Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐺‘𝑘) = (𝐺‘0)) |
2 | 1 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = 0 → (1st
‘(𝐺‘𝑘)) = (1st
‘(𝐺‘0))) |
3 | 1 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = 0 → (2nd
‘(𝐺‘𝑘)) = (2nd
‘(𝐺‘0))) |
4 | 2, 3 | breq12d 4666 |
. . . 4
⊢ (𝑘 = 0 → ((1st
‘(𝐺‘𝑘)) < (2nd
‘(𝐺‘𝑘)) ↔ (1st
‘(𝐺‘0)) <
(2nd ‘(𝐺‘0)))) |
5 | 4 | imbi2d 330 |
. . 3
⊢ (𝑘 = 0 → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘0)) < (2nd
‘(𝐺‘0))))) |
6 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝐺‘𝑘) = (𝐺‘𝑛)) |
7 | 6 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = 𝑛 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑛))) |
8 | 6 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = 𝑛 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑛))) |
9 | 7, 8 | breq12d 4666 |
. . . 4
⊢ (𝑘 = 𝑛 → ((1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) |
10 | 9 | imbi2d 330 |
. . 3
⊢ (𝑘 = 𝑛 → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))))) |
11 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) |
12 | 11 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘(𝑛 + 1)))) |
13 | 11 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘(𝑛 + 1)))) |
14 | 12, 13 | breq12d 4666 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → ((1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1))))) |
15 | 14 | imbi2d 330 |
. . 3
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))))) |
16 | | fveq2 6191 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝐺‘𝑘) = (𝐺‘𝑁)) |
17 | 16 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = 𝑁 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑁))) |
18 | 16 | fveq2d 6195 |
. . . . 5
⊢ (𝑘 = 𝑁 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑁))) |
19 | 17, 18 | breq12d 4666 |
. . . 4
⊢ (𝑘 = 𝑁 → ((1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁)))) |
20 | 19 | imbi2d 330 |
. . 3
⊢ (𝑘 = 𝑁 → ((𝜑 → (1st ‘(𝐺‘𝑘)) < (2nd ‘(𝐺‘𝑘))) ↔ (𝜑 → (1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁))))) |
21 | | 0lt1 10550 |
. . . . 5
⊢ 0 <
1 |
22 | 21 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 < 1) |
23 | | ruc.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
24 | | ruc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
25 | | ruc.4 |
. . . . . . 7
⊢ 𝐶 = ({〈0, 〈0,
1〉〉} ∪ 𝐹) |
26 | | ruc.5 |
. . . . . . 7
⊢ 𝐺 = seq0(𝐷, 𝐶) |
27 | 23, 24, 25, 26 | ruclem4 14963 |
. . . . . 6
⊢ (𝜑 → (𝐺‘0) = 〈0,
1〉) |
28 | 27 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐺‘0)) =
(1st ‘〈0, 1〉)) |
29 | | c0ex 10034 |
. . . . . 6
⊢ 0 ∈
V |
30 | | 1ex 10035 |
. . . . . 6
⊢ 1 ∈
V |
31 | 29, 30 | op1st 7176 |
. . . . 5
⊢
(1st ‘〈0, 1〉) = 0 |
32 | 28, 31 | syl6eq 2672 |
. . . 4
⊢ (𝜑 → (1st
‘(𝐺‘0)) =
0) |
33 | 27 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
(2nd ‘〈0, 1〉)) |
34 | 29, 30 | op2nd 7177 |
. . . . 5
⊢
(2nd ‘〈0, 1〉) = 1 |
35 | 33, 34 | syl6eq 2672 |
. . . 4
⊢ (𝜑 → (2nd
‘(𝐺‘0)) =
1) |
36 | 22, 32, 35 | 3brtr4d 4685 |
. . 3
⊢ (𝜑 → (1st
‘(𝐺‘0)) <
(2nd ‘(𝐺‘0))) |
37 | 23 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → 𝐹:ℕ⟶ℝ) |
38 | 24 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
39 | 23, 24, 25, 26 | ruclem6 14964 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
40 | 39 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
41 | 40 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
42 | | xp1st 7198 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘𝑛)) ∈ ℝ) |
44 | | xp2nd 7199 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
45 | 41, 44 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
46 | | nn0p1nn 11332 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
47 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶ℝ ∧
(𝑛 + 1) ∈ ℕ)
→ (𝐹‘(𝑛 + 1)) ∈
ℝ) |
48 | 23, 46, 47 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
49 | 48 | adantrr 753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
50 | | eqid 2622 |
. . . . . . . . 9
⊢
(1st ‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) = (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
51 | | eqid 2622 |
. . . . . . . . 9
⊢
(2nd ‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) = (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
52 | | simprr 796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))) |
53 | 37, 38, 43, 45, 49, 50, 51, 52 | ruclem2 14961 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → ((1st ‘(𝐺‘𝑛)) ≤ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ∧ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) < (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ∧ (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ≤ (2nd ‘(𝐺‘𝑛)))) |
54 | 53 | simp2d 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) < (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
55 | 23, 24, 25, 26 | ruclem7 14965 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘(𝑛 + 1)) = ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
56 | 55 | adantrr 753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘(𝑛 + 1)) = ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
57 | | 1st2nd2 7205 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(𝐺‘𝑛) = 〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉) |
58 | 41, 57 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘𝑛) = 〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉) |
59 | 58 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1))) = (〈(1st
‘(𝐺‘𝑛)), (2nd
‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
60 | 56, 59 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (𝐺‘(𝑛 + 1)) = (〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
61 | 60 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘(𝑛 + 1))) = (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
62 | 60 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (2nd ‘(𝐺‘(𝑛 + 1))) = (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
63 | 54, 61, 62 | 3brtr4d 4685 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℕ0 ∧
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)))) → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))) |
64 | 63 | expr 643 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)) → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1))))) |
65 | 64 | expcom 451 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ (𝜑 →
((1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛)) → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))))) |
66 | 65 | a2d 29 |
. . 3
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 →
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))) → (𝜑 → (1st ‘(𝐺‘(𝑛 + 1))) < (2nd ‘(𝐺‘(𝑛 + 1)))))) |
67 | 5, 10, 15, 20, 36, 66 | nn0ind 11472 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 →
(1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁)))) |
68 | 67 | impcom 446 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) →
(1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁))) |