Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem ruclem15 4899

Description: Lemma for ruc 4924. A helper lemma showing the successor value of the 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 ∘ (DseqC))
ruclem.4	⊢ H = (2^nd ∘ (DseqC))
ruclem15.a	⊢ A ∈ ℕ

**Assertion**
Ref	Expression
ruclem15	⊢ ((DseqC) ‘(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 group(s): 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 4893	. . . 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 4889	. . . 4 ⊢ C ∈ V
7	3, 6	seqsuc 4671	. . 3 ⊢ (A ∈ ℕ → ((DseqC) ‘(A + 1)) = (((DseqC) ‘A)D(C ‘(A + 1))))
8	1, 7	ax-mp 6	. 2 ⊢ ((DseqC) ‘(A + 1)) = (((DseqC) ‘A)D(C ‘(A + 1)))
9	4, 5, 2	ruclem13 4897	. . . 4 ⊢ (DseqC):ℕ–→(ℝ × ℝ)
10		ffvrn 2890	. . . 4 ⊢ (((DseqC):ℕ–→(ℝ × ℝ) ∧ A ∈ ℕ) → ((DseqC) ‘A) ∈ (ℝ × ℝ))
11	9, 1, 10	mp2an 520	. . 3 ⊢ ((DseqC) ‘A) ∈ (ℝ × ℝ)
12	4, 5, 1	ruclem8 4892	. . . 4 ⊢ (C ‘(A + 1)) = (F ‘(A + 1))
13		peano2nn 4433	. . . . . 6 ⊢ (A ∈ ℕ → (A + 1) ∈ ℕ)
14	1, 13	ax-mp 6	. . . . 5 ⊢ (A + 1) ∈ ℕ
15		ffvrn 2890	. . . . 5 ⊢ ((F:ℕ–→ℝ ∧ (A + 1) ∈ ℕ) → (F ‘(A + 1)) ∈ ℝ)
16	4, 14, 15	mp2an 520	. . . 4 ⊢ (F ‘(A + 1)) ∈ ℝ
17	12, 16	eqeltr 1159	. . 3 ⊢ (C ‘(A + 1)) ∈ ℝ
18		opex 1893	. . . . 5 ⊢ ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ ∈ V
19		opex 1893	. . . . 5 ⊢ ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ ∈ V
20	18, 19	ifex 1797	. . . 4 ⊢ if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩) ∈ V
21		cleqid 1102	. . . . 5 ⊢ v = v
22		ruclem4 4888	. . . . 5 ⊢ ((w = ((DseqC) ‘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 ‘((DseqC) ‘A)) < v ∧ v < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · v) + (2^nd ‘((DseqC) ‘A))) / 3), ((v + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩))
23	21, 22	mpan2 519	. . . 4 ⊢ (w = ((DseqC) ‘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 ‘((DseqC) ‘A)) < v ∧ v < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · v) + (2^nd ‘((DseqC) ‘A))) / 3), ((v + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩))
24		cleqid 1102	. . . . 5 ⊢ ((DseqC) ‘A) = ((DseqC) ‘A)
25		ruclem4 4888	. . . . 5 ⊢ ((((DseqC) ‘A) = ((DseqC) ‘A) ∧ v = (C ‘(A + 1))) → if(((1^st ‘((DseqC) ‘A)) < v ∧ v < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · v) + (2^nd ‘((DseqC) ‘A))) / 3), ((v + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩) = if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩))
26	24, 25	mpan 518	. . . 4 ⊢ (v = (C ‘(A + 1)) → if(((1^st ‘((DseqC) ‘A)) < v ∧ v < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · v) + (2^nd ‘((DseqC) ‘A))) / 3), ((v + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩) = if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩))
27	2	ruclem12 4896	. . . 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 3051	. . 3 ⊢ ((((DseqC) ‘A) ∈ (ℝ × ℝ) ∧ (C ‘(A + 1)) ∈ ℝ) → (((DseqC) ‘A)D(C ‘(A + 1))) = if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩))
29	11, 17, 28	mp2an 520	. 2 ⊢ (((DseqC) ‘A)D(C ‘(A + 1))) = if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩)
30		ruclem.3	. . . . . . 7 ⊢ G = (1^st ∘ (DseqC))
31	1, 3, 6, 30	ruclem10 4894	. . . . . 6 ⊢ (1^st ‘((DseqC) ‘A)) = (G ‘A)
32	31, 12	breq12i 2070	. . . . 5 ⊢ ((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ↔ (G ‘A) < (F ‘(A + 1)))
33		ruclem.4	. . . . . . 7 ⊢ H = (2^nd ∘ (DseqC))
34	1, 3, 6, 33	ruclem11 4895	. . . . . 6 ⊢ (2^nd ‘((DseqC) ‘A)) = (H ‘A)
35	12, 34	breq12i 2070	. . . . 5 ⊢ ((C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A)) ↔ (F ‘(A + 1)) < (H ‘A))
36	32, 35	anbi12i 369	. . . 4 ⊢ (((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))) ↔ ((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)))
37		ifbi 1783	. . . 4 ⊢ ((((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))) ↔ ((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A))) → if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩))
38	36, 37	ax-mp 6	. . 3 ⊢ if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩) = if(((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩)
39	12	opreq2i 3010	. . . . . . 7 ⊢ (2 · (C ‘(A + 1))) = (2 · (F ‘(A + 1)))
40	39, 34	opreq12i 3011	. . . . . 6 ⊢ ((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) = ((2 · (F ‘(A + 1))) + (H ‘A))
41	40	opreq1i 3009	. . . . 5 ⊢ (((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3) = (((2 · (F ‘(A + 1))) + (H ‘A)) / 3)
42	34	opreq2i 3010	. . . . . . 7 ⊢ (2 · (2^nd ‘((DseqC) ‘A))) = (2 · (H ‘A))
43	12, 42	opreq12i 3011	. . . . . 6 ⊢ ((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) = ((F ‘(A + 1)) + (2 · (H ‘A)))
44	43	opreq1i 3009	. . . . 5 ⊢ (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3) = (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)
45		opeq12 1878	. . . . 5 ⊢ (((((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3) = (((2 · (F ‘(A + 1))) + (H ‘A)) / 3) ∧ (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3) = (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)) → ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ = ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩)
46	41, 44, 45	mp2an 520	. . . 4 ⊢ ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ = ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩
47	31	opreq2i 3010	. . . . . . 7 ⊢ (2 · (1^st ‘((DseqC) ‘A))) = (2 · (G ‘A))
48	47, 34	opreq12i 3011	. . . . . 6 ⊢ ((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) = ((2 · (G ‘A)) + (H ‘A))
49	48	opreq1i 3009	. . . . 5 ⊢ (((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3) = (((2 · (G ‘A)) + (H ‘A)) / 3)
50	31, 42	opreq12i 3011	. . . . . 6 ⊢ ((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) = ((G ‘A) + (2 · (H ‘A)))
51	50	opreq1i 3009	. . . . 5 ⊢ (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3) = (((G ‘A) + (2 · (H ‘A))) / 3)
52		opeq12 1878	. . . . 5 ⊢ (((((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3) = (((2 · (G ‘A)) + (H ‘A)) / 3) ∧ (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3) = (((G ‘A) + (2 · (H ‘A))) / 3)) → ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ = ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩)
53	49, 51, 52	mp2an 520	. . . 4 ⊢ ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ = ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩
54		ifeq12 1782	. . . 4 ⊢ ((⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩ = ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩ ∧ ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘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 ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘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	46, 53, 54	mp2an 520	. . 3 ⊢ if(((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘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)⟩)
56	38, 55	eqtr 1119	. 2 ⊢ if(((1^st ‘((DseqC) ‘A)) < (C ‘(A + 1)) ∧ (C ‘(A + 1)) < (2^nd ‘((DseqC) ‘A))), ⟨(((2 · (C ‘(A + 1))) + (2^nd ‘((DseqC) ‘A))) / 3), (((C ‘(A + 1)) + (2 · (2^nd ‘((DseqC) ‘A)))) / 3)⟩, ⟨(((2 · (1^st ‘((DseqC) ‘A))) + (2^nd ‘((DseqC) ‘A))) / 3), (((1^st ‘((DseqC) ‘A)) + (2 · (2^nd ‘((DseqC) ‘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)⟩)
57	8, 29, 56	3eqtr 1123	1 ⊢ ((DseqC) ‘(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 127 ∧ wa 196 = weq 797 = wceq 1091 ∈ wcel 1092 ∖ cdif 1484 ∪ cun 1485 ifcif 1776 {csn 1808 ⟨cop 1810 class class class wbr 2054 × cxp 2408 ↾ cres 2412 ∘ ccom 2414 –→wf 2418 ‘cfv 2422 (class class class)co 3001 {copab2 3002 1^st c1st 3085 2^nd c2nd 3086 ℝcr 4027 1c1 4029 + caddc 4031 · cmulc 4032 < clt 4033 / cdiv 4091 ℕcn 4093 2c2 4454 3c3 4455 seqcseq 4660

This theorem is referenced by: ruclem18 4902 ruclem19 4903 ruclem20 4904 ruclem21 4905

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-n0 4535 df-z 4564 df-seq 4661

metamath.org