ruclem15 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem ruclem15 7525

Description: Lemma for ruc 7550. A helper lemma showing the successor value of the recursive sequence builder used for our construction.

**Hypotheses**
Ref	Expression
ruclem.0	⊢ F:ℕ–→ℝ
ruclem.1	⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))
ruclem.2	⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ⋀ y ∈ ℝ) ⋀ z = if(((1^st ‘x) < y ⋀ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))}
ruclem.3	⊢ G = (1^st ∘ (Dseq₁C))
ruclem.4	⊢ H = (2^nd ∘ (Dseq₁C))
ruclem15.a	⊢ A ∈ ℕ

**Assertion**
Ref	Expression
ruclem15	⊢ ((Dseq₁C) ‘(A + 1)) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩, ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩)

Distinct variable groups: x,y,z z,F

**Proof of Theorem ruclem15**
Step	Hyp	Ref	Expression
1		ruclem15.a	. . 3 ⊢ A ∈ ℕ
2		ruclem.2	. . . . 5 ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ⋀ y ∈ ℝ) ⋀ z = if(((1^st ‘x) < y ⋀ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))}
3	2	ruclem9 7519	. . . 4 ⊢ D ∈ V
4		ruclem.0	. . . . 5 ⊢ F:ℕ–→ℝ
5		ruclem.1	. . . . 5 ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))
6	4, 5	ruclem5 7515	. . . 4 ⊢ C ∈ V
7	3, 6	seq1p1 6319	. . 3 ⊢ (A ∈ ℕ → ((Dseq₁C) ‘(A + 1)) = (((Dseq₁C) ‘A)D(C ‘(A + 1))))
8	1, 7	ax-mp 7	. 2 ⊢ ((Dseq₁C) ‘(A + 1)) = (((Dseq₁C) ‘A)D(C ‘(A + 1)))
9	4, 5, 2	ruclem13 7523	. . . 4 ⊢ (Dseq₁C):ℕ–→(ℝ × ℝ)
10		ffvelrn 3820	. . . 4 ⊢ (((Dseq₁C):ℕ–→(ℝ × ℝ) ⋀ A ∈ ℕ) → ((Dseq₁C) ‘A) ∈ (ℝ × ℝ))
11	9, 1, 10	mp2an 699	. . 3 ⊢ ((Dseq₁C) ‘A) ∈ (ℝ × ℝ)
12	4, 5, 1	ruclem8 7518	. . . 4 ⊢ (C ‘(A + 1)) = (F ‘(A + 1))
13		peano2nn 5937	. . . . . 6 ⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)
14	1, 13	ax-mp 7	. . . . 5 ⊢ (A + 1) ∈ ℕ
15		ffvelrn 3820	. . . . 5 ⊢ ((F:ℕ–→ℝ ⋀ (A + 1) ∈ ℕ) → (F ‘(A + 1)) ∈ ℝ)
16	4, 14, 15	mp2an 699	. . . 4 ⊢ (F ‘(A + 1)) ∈ ℝ
17	12, 16	eqeltr 1547	. . 3 ⊢ (C ‘(A + 1)) ∈ ℝ
18		opex 2788	. . . . 5 ⊢ ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩ ∈ V
19		opex 2788	. . . . 5 ⊢ ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩ ∈ V
20	18, 19	ifex 2404	. . . 4 ⊢ if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) ∈ V
21		eqid 1478	. . . . 5 ⊢ v = v
22		ruclem4 7514	. . . . 5 ⊢ ((w = ((Dseq₁C) ‘A) ⋀ v = v) → if(((1^st ‘w) < v ⋀ v < (2^nd ‘w)), ⟨(((2 · v) + (2^nd ‘w)) / 3), ((v + (2 · (2^nd ‘w))) / 3)⟩, ⟨(((2 · (1^st ‘w)) + (2^nd ‘w)) / 3), (((1^st ‘w) + (2 · (2^nd ‘w))) / 3)⟩) = if(((1^st ‘((Dseq₁C) ‘A)) < v ⋀ v < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · v) + (2^nd ‘((Dseq₁C) ‘A))) / 3), ((v + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩))
23	21, 22	mpan2 698	. . . 4 ⊢ (w = ((Dseq₁C) ‘A) → if(((1^st ‘w) < v ⋀ v < (2^nd ‘w)), ⟨(((2 · v) + (2^nd ‘w)) / 3), ((v + (2 · (2^nd ‘w))) / 3)⟩, ⟨(((2 · (1^st ‘w)) + (2^nd ‘w)) / 3), (((1^st ‘w) + (2 · (2^nd ‘w))) / 3)⟩) = if(((1^st ‘((Dseq₁C) ‘A)) < v ⋀ v < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · v) + (2^nd ‘((Dseq₁C) ‘A))) / 3), ((v + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩))
24		eqid 1478	. . . . 5 ⊢ ((Dseq₁C) ‘A) = ((Dseq₁C) ‘A)
25		ruclem4 7514	. . . . 5 ⊢ ((((Dseq₁C) ‘A) = ((Dseq₁C) ‘A) ⋀ v = (C ‘(A + 1))) → if(((1^st ‘((Dseq₁C) ‘A)) < v ⋀ v < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · v) + (2^nd ‘((Dseq₁C) ‘A))) / 3), ((v + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩))
26	24, 25	mpan 697	. . . 4 ⊢ (v = (C ‘(A + 1)) → if(((1^st ‘((Dseq₁C) ‘A)) < v ⋀ v < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · v) + (2^nd ‘((Dseq₁C) ‘A))) / 3), ((v + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩))
27	2	ruclem12 7522	. . . 4 ⊢ D = {⟨⟨w, v⟩, u⟩∣((w ∈ (ℝ × ℝ) ⋀ v ∈ ℝ) ⋀ u = if(((1^st ‘w) < v ⋀ v < (2^nd ‘w)), ⟨(((2 · v) + (2^nd ‘w)) / 3), ((v + (2 · (2^nd ‘w))) / 3)⟩, ⟨(((2 · (1^st ‘w)) + (2^nd ‘w)) / 3), (((1^st ‘w) + (2 · (2^nd ‘w))) / 3)⟩))}
28	20, 23, 26, 27	oprabval2 4034	. . 3 ⊢ ((((Dseq₁C) ‘A) ∈ (ℝ × ℝ) ⋀ (C ‘(A + 1)) ∈ ℝ) → (((Dseq₁C) ‘A)D(C ‘(A + 1))) = if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩))
29	11, 17, 28	mp2an 699	. 2 ⊢ (((Dseq₁C) ‘A)D(C ‘(A + 1))) = if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩)
30		ruclem.3	. . . . . . 7 ⊢ G = (1^st ∘ (Dseq₁C))
31	1, 3, 6, 30	ruclem10 7520	. . . . . 6 ⊢ (1^st ‘((Dseq₁C) ‘A)) = (G ‘A)
32	31, 12	breq12i 2633	. . . . 5 ⊢ ((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ↔ (G ‘A) < (F ‘(A + 1)))
33		ruclem.4	. . . . . . 7 ⊢ H = (2^nd ∘ (Dseq₁C))
34	1, 3, 6, 33	ruclem11 7521	. . . . . 6 ⊢ (2^nd ‘((Dseq₁C) ‘A)) = (H ‘A)
35	12, 34	breq12i 2633	. . . . 5 ⊢ ((C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A)) ↔ (F ‘(A + 1)) < (H ‘A))
36	32, 35	anbi12i 484	. . . 4 ⊢ (((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))) ↔ ((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)))
37		ifbi 2375	. . . 4 ⊢ ((((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))) ↔ ((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A))) → if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩))
38	36, 37	ax-mp 7	. . 3 ⊢ if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩)
39	12	opreq2i 3978	. . . . . . 7 ⊢ (2 · (C ‘(A + 1))) = (2 · (F ‘(A + 1)))
40	39, 34	opreq12i 3979	. . . . . 6 ⊢ ((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) = ((2 · (F ‘(A + 1))) + (H ‘A))
41	40	opreq1i 3977	. . . . 5 ⊢ (((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3) = (((2 · (F ‘(A + 1))) + (H ‘A)) / 3)
42	34	opreq2i 3978	. . . . . . 7 ⊢ (2 · (2^nd ‘((Dseq₁C) ‘A))) = (2 · (H ‘A))
43	12, 42	opreq12i 3979	. . . . . 6 ⊢ ((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) = ((F ‘(A + 1)) + (2 · (H ‘A)))
44	43	opreq1i 3977	. . . . 5 ⊢ (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3) = (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)
45	41, 44	opeq12i 2496	. . . 4 ⊢ ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩ = ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩
46	31	opreq2i 3978	. . . . . . 7 ⊢ (2 · (1^st ‘((Dseq₁C) ‘A))) = (2 · (G ‘A))
47	46, 34	opreq12i 3979	. . . . . 6 ⊢ ((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) = ((2 · (G ‘A)) + (H ‘A))
48	47	opreq1i 3977	. . . . 5 ⊢ (((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3) = (((2 · (G ‘A)) + (H ‘A)) / 3)
49	31, 42	opreq12i 3979	. . . . . 6 ⊢ ((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) = ((G ‘A) + (2 · (H ‘A)))
50	49	opreq1i 3977	. . . . 5 ⊢ (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3) = (((G ‘A) + (2 · (H ‘A))) / 3)
51	48, 50	opeq12i 2496	. . . 4 ⊢ ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩ = ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩
52		ifeq12 2372	. . . 4 ⊢ ((⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩ = ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩ ⋀ ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩ = ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩) → if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩, ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩))
53	45, 51, 52	mp2an 699	. . 3 ⊢ if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩, ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩)
54	38, 53	eqtr 1498	. 2 ⊢ if(((1^st ‘((Dseq₁C) ‘A)) < (C ‘(A + 1)) ⋀ (C ‘(A + 1)) < (2^nd ‘((Dseq₁C) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((Dseq₁C) ‘A))) + (2^nd ‘((Dseq₁C) ‘A))) / 3), (((1^st ‘((Dseq₁C) ‘A)) + (2 · (2^nd ‘((Dseq₁C) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩, ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩)
55	8, 29, 54	3eqtr 1502	1 ⊢ ((Dseq₁C) ‘(A + 1)) = if(((G ‘A) < (F ‘(A + 1)) ⋀ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩, ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩)

Colors of variables: wff set class

Syntax hints: ↔ wb 146 ⋀ wa 223 = wceq 958 ∈ wcel 960 ∖ cdif 2047 ∪ cun 2048 ifcif 2365 {csn 2413 ⟨cop 2415 class class class wbr 2624 × cxp 3174 ↾ cres 3178 ∘ ccom 3180 –→wf 3184 ‘cfv 3188 (class class class)co 3969 {copab2 3970 1^st c1st 4083 2^nd c2nd 4084 ℝcr 5245 1c1 5247 + caddc 5249 · cmul 5251 / cdiv 5306 ℕcn 5308 < clt 5498 2c2 5963 3c3 5964 seq₁cseq1 6308

This theorem is referenced by: ruclem18 7528 ruclem19 7529 ruclem20 7530 ruclem21 7531

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-nel 1591 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2005 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-f1 3201 df-fo 3202 df-f1o 3203 df-fv 3204 df-rdg 3938 df-opr 3971 df-oprab 3972 df-1st 4085 df-2nd 4086 df-1o 4139 df-oadd 4141 df-omul 4142 df-er 4267 df-ec 4269 df-qs 4272 df-en 4374 df-dom 4375 df-sdom 4376 df-ni 5012 df-pli 5013 df-mi 5014 df-lti 5015 df-plpq 5047 df-mpq 5048 df-enq 5049 df-nq 5050 df-plq 5051 df-mq 5052 df-rq 5053 df-ltq 5054 df-1q 5055 df-np 5098 df-1p 5099 df-plp 5100 df-mp 5101 df-ltp 5102 df-plpr 5176 df-mpr 5177 df-enr 5178 df-nr 5179 df-plr 5180 df-mr 5181 df-ltr 5182 df-0r 5183 df-1r 5184 df-m1r 5185 df-c 5252 df-0 5253 df-1 5254 df-i 5255 df-r 5256 df-plus 5257 df-mul 5258 df-lt 5259 df-sub 5368 df-neg 5370 df-pnf 5499 df-mnf 5500 df-xr 5501 df-ltxr 5502 df-le 5503 df-div 5715 df-n 5927 df-2 5972 df-3 5973 df-n0 6102 df-z 6138 df-seq1 6309