| Step | Hyp | Ref
| Expression |
| 1 | | ruc.5 |
. . . . . . 7
⊢ 𝐺 = seq0(𝐷, 𝐶) |
| 2 | 1 | fveq1i 6907 |
. . . . . 6
⊢ (𝐺‘0) = (seq0(𝐷, 𝐶)‘0) |
| 3 | | 0z 12624 |
. . . . . . 7
⊢ 0 ∈
ℤ |
| 4 | | seq1 14055 |
. . . . . . 7
⊢ (0 ∈
ℤ → (seq0(𝐷,
𝐶)‘0) = (𝐶‘0)) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢
(seq0(𝐷, 𝐶)‘0) = (𝐶‘0) |
| 6 | 2, 5 | eqtri 2765 |
. . . . 5
⊢ (𝐺‘0) = (𝐶‘0) |
| 7 | | ruc.1 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
| 8 | | ruc.2 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
| 9 | | ruc.4 |
. . . . . 6
⊢ 𝐶 = ({〈0, 〈0,
1〉〉} ∪ 𝐹) |
| 10 | 7, 8, 9, 1 | ruclem4 16270 |
. . . . 5
⊢ (𝜑 → (𝐺‘0) = 〈0,
1〉) |
| 11 | 6, 10 | eqtr3id 2791 |
. . . 4
⊢ (𝜑 → (𝐶‘0) = 〈0,
1〉) |
| 12 | | 0re 11263 |
. . . . 5
⊢ 0 ∈
ℝ |
| 13 | | 1re 11261 |
. . . . 5
⊢ 1 ∈
ℝ |
| 14 | | opelxpi 5722 |
. . . . 5
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → 〈0, 1〉 ∈ (ℝ
× ℝ)) |
| 15 | 12, 13, 14 | mp2an 692 |
. . . 4
⊢ 〈0,
1〉 ∈ (ℝ × ℝ) |
| 16 | 11, 15 | eqeltrdi 2849 |
. . 3
⊢ (𝜑 → (𝐶‘0) ∈ (ℝ ×
ℝ)) |
| 17 | | 1st2nd2 8053 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 =
〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 18 | 17 | ad2antrl 728 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) → 𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
| 19 | 18 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) → (𝑧𝐷𝑤) = (〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) |
| 20 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) → 𝐹:ℕ⟶ℝ) |
| 21 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
| 22 | | xp1st 8046 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
| 23 | 22 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) →
(1st ‘𝑧)
∈ ℝ) |
| 24 | | xp2nd 8047 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (2nd ‘𝑧) ∈ ℝ) |
| 25 | 24 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) →
(2nd ‘𝑧)
∈ ℝ) |
| 26 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) → 𝑤 ∈
ℝ) |
| 27 | | eqid 2737 |
. . . . . 6
⊢
(1st ‘(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) = (1st
‘(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) |
| 28 | | eqid 2737 |
. . . . . 6
⊢
(2nd ‘(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) = (2nd
‘(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) |
| 29 | 20, 21, 23, 25, 26, 27, 28 | ruclem1 16267 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) →
((〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤) ∈ (ℝ × ℝ) ∧
(1st ‘(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) = if((((1st ‘𝑧) + (2nd ‘𝑧)) / 2) < 𝑤, (1st ‘𝑧), (((((1st ‘𝑧) + (2nd ‘𝑧)) / 2) + (2nd
‘𝑧)) / 2)) ∧
(2nd ‘(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤)) = if((((1st ‘𝑧) + (2nd ‘𝑧)) / 2) < 𝑤, (((1st ‘𝑧) + (2nd ‘𝑧)) / 2), (2nd ‘𝑧)))) |
| 30 | 29 | simp1d 1143 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) →
(〈(1st ‘𝑧), (2nd ‘𝑧)〉𝐷𝑤) ∈ (ℝ ×
ℝ)) |
| 31 | 19, 30 | eqeltrd 2841 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ ℝ)) → (𝑧𝐷𝑤) ∈ (ℝ ×
ℝ)) |
| 32 | | nn0uz 12920 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
| 33 | | 0zd 12625 |
. . 3
⊢ (𝜑 → 0 ∈
ℤ) |
| 34 | | 0p1e1 12388 |
. . . . . . 7
⊢ (0 + 1) =
1 |
| 35 | 34 | fveq2i 6909 |
. . . . . 6
⊢
(ℤ≥‘(0 + 1)) =
(ℤ≥‘1) |
| 36 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 37 | 35, 36 | eqtr4i 2768 |
. . . . 5
⊢
(ℤ≥‘(0 + 1)) = ℕ |
| 38 | 37 | eleq2i 2833 |
. . . 4
⊢ (𝑧 ∈
(ℤ≥‘(0 + 1)) ↔ 𝑧 ∈ ℕ) |
| 39 | 9 | equncomi 4160 |
. . . . . . . 8
⊢ 𝐶 = (𝐹 ∪ {〈0, 〈0,
1〉〉}) |
| 40 | 39 | fveq1i 6907 |
. . . . . . 7
⊢ (𝐶‘𝑧) = ((𝐹 ∪ {〈0, 〈0,
1〉〉})‘𝑧) |
| 41 | | nnne0 12300 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℕ → 𝑧 ≠ 0) |
| 42 | 41 | necomd 2996 |
. . . . . . . 8
⊢ (𝑧 ∈ ℕ → 0 ≠
𝑧) |
| 43 | | fvunsn 7199 |
. . . . . . . 8
⊢ (0 ≠
𝑧 → ((𝐹 ∪ {〈0, 〈0,
1〉〉})‘𝑧) =
(𝐹‘𝑧)) |
| 44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ ℕ → ((𝐹 ∪ {〈0, 〈0,
1〉〉})‘𝑧) =
(𝐹‘𝑧)) |
| 45 | 40, 44 | eqtrid 2789 |
. . . . . 6
⊢ (𝑧 ∈ ℕ → (𝐶‘𝑧) = (𝐹‘𝑧)) |
| 46 | 45 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐶‘𝑧) = (𝐹‘𝑧)) |
| 47 | 7 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐹‘𝑧) ∈ ℝ) |
| 48 | 46, 47 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐶‘𝑧) ∈ ℝ) |
| 49 | 38, 48 | sylan2b 594 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘(0 +
1))) → (𝐶‘𝑧) ∈
ℝ) |
| 50 | 16, 31, 32, 33, 49 | seqf2 14062 |
. 2
⊢ (𝜑 → seq0(𝐷, 𝐶):ℕ0⟶(ℝ
× ℝ)) |
| 51 | 1 | feq1i 6727 |
. 2
⊢ (𝐺:ℕ0⟶(ℝ ×
ℝ) ↔ seq0(𝐷,
𝐶):ℕ0⟶(ℝ
× ℝ)) |
| 52 | 50, 51 | sylibr 234 |
1
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |