| Step | Hyp | Ref
| Expression |
| 1 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = 0 → (1st
‘(𝐺‘𝑘)) = (1st
‘(𝐺‘0))) |
| 2 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = 0 → (2nd
‘(𝐺‘𝑘)) = (2nd
‘(𝐺‘0))) |
| 3 | 1, 2 | breq12d 5156 |
. . . 4
⊢ (𝑘 = 0 → ((1st
‘(𝐺‘𝑘)) < (2nd
‘(𝐺‘𝑘)) ↔ (1st
‘(𝐺‘0)) <
(2nd ‘(𝐺‘0)))) |
| 4 | 3 | imbi2d 340 |
. . 3
⊢ (𝑘 = 0 → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘0)) < (2nd
‘(𝐺‘0))))) |
| 5 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = 𝑛 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑛))) |
| 6 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = 𝑛 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑛))) |
| 7 | 5, 6 | breq12d 5156 |
. . . 4
⊢ (𝑘 = 𝑛 → ((1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) |
| 8 | 7 | imbi2d 340 |
. . 3
⊢ (𝑘 = 𝑛 → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))))) |
| 9 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘(𝑛 + 1)))) |
| 10 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘(𝑛 + 1)))) |
| 11 | 9, 10 | breq12d 5156 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → ((1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1))))) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))))) |
| 13 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = 𝑁 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑁))) |
| 14 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑘 = 𝑁 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑁))) |
| 15 | 13, 14 | breq12d 5156 |
. . . 4
⊢ (𝑘 = 𝑁 → ((1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁)))) |
| 16 | 15 | imbi2d 340 |
. . 3
⊢ (𝑘 = 𝑁 → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁))))) |
| 17 | | 0lt1 11785 |
. . . . 5
⊢ 0 <
1 |
| 18 | 17 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 < 1) |
| 19 | | ruc.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
| 20 | | ruc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
| 21 | | ruc.4 |
. . . . . . 7
⊢ 𝐶 = ({〈0, 〈0,
1〉〉} ∪ 𝐹) |
| 22 | | ruc.5 |
. . . . . . 7
⊢ 𝐺 = seq0(𝐷, 𝐶) |
| 23 | 19, 20, 21, 22 | ruclem4 16270 |
. . . . . 6
⊢ (𝜑 → (𝐺‘0) = 〈0,
1〉) |
| 24 | 23 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐺‘0)) =
(1st ‘〈0, 1〉)) |
| 25 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 26 | | 1ex 11257 |
. . . . . 6
⊢ 1 ∈
V |
| 27 | 25, 26 | op1st 8022 |
. . . . 5
⊢
(1st ‘〈0, 1〉) = 0 |
| 28 | 24, 27 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (1st
‘(𝐺‘0)) =
0) |
| 29 | 23 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
(2nd ‘〈0, 1〉)) |
| 30 | 25, 26 | op2nd 8023 |
. . . . 5
⊢
(2nd ‘〈0, 1〉) = 1 |
| 31 | 29, 30 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
1) |
| 32 | 18, 28, 31 | 3brtr4d 5175 |
. . 3
⊢ (𝜑 → (1st
‘(𝐺‘0)) <
(2nd ‘(𝐺‘0))) |
| 33 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → 𝐹:ℕ⟶ℝ) |
| 34 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
| 35 | 19, 20, 21, 22 | ruclem6 16271 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
| 36 | 35 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
| 37 | 36 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
| 38 | | xp1st 8046 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘𝑛)) ∈ ℝ) |
| 40 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
| 41 | 37, 40 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
| 42 | | nn0p1nn 12565 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
| 43 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶ℝ ∧
(𝑛 + 1) ∈ ℕ)
→ (𝐹‘(𝑛 + 1)) ∈
ℝ) |
| 44 | 19, 42, 43 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
| 45 | 44 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
| 46 | | eqid 2737 |
. . . . . . . . 9
⊢
(1st ‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) = (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
| 47 | | eqid 2737 |
. . . . . . . . 9
⊢
(2nd ‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) = (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
| 48 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))) |
| 49 | 33, 34, 39, 41, 45, 46, 47, 48 | ruclem2 16268 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → ((1st ‘(𝐺‘𝑛)) ≤ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ∧ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) < (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ∧ (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ≤ (2nd ‘(𝐺‘𝑛)))) |
| 50 | 49 | simp2d 1144 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) < (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
| 51 | 19, 20, 21, 22 | ruclem7 16272 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘(𝑛 + 1)) = ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
| 52 | 51 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘(𝑛 + 1)) = ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
| 53 | | 1st2nd2 8053 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(𝐺‘𝑛) = 〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉) |
| 54 | 37, 53 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘𝑛) = 〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉) |
| 55 | 54 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1))) = (〈(1st
‘(𝐺‘𝑛)), (2nd
‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
| 56 | 52, 55 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘(𝑛 + 1)) = (〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
| 57 | 56 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘(𝑛 + 1))) = (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
| 58 | 56 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (2nd ‘(𝐺‘(𝑛 + 1))) = (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
| 59 | 50, 57, 58 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))) |
| 60 | 59 | expr 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)) → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1))))) |
| 61 | 60 | expcom 413 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ (𝜑 →
((1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)) → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))))) |
| 62 | 61 | a2d 29 |
. . 3
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 →
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))) → (𝜑 → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))))) |
| 63 | 4, 8, 12, 16, 32, 62 | nn0ind 12713 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 →
(1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁)))) |
| 64 | 63 | impcom 407 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) →
(1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁))) |