Step | Hyp | Ref
| Expression |
1 | | ruclem9.7 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → (𝐺‘𝑘) = (𝐺‘𝑀)) |
3 | 2 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑀 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑀))) |
4 | 3 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = 𝑀 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑀)))) |
5 | 2 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑀 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑀))) |
6 | 5 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝑀 → ((2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)) ↔ (2nd ‘(𝐺‘𝑀)) ≤ (2nd ‘(𝐺‘𝑀)))) |
7 | 4, 6 | anbi12d 743 |
. . . 4
⊢ (𝑘 = 𝑀 → (((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀))) ↔ ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑀)) ∧ (2nd ‘(𝐺‘𝑀)) ≤ (2nd ‘(𝐺‘𝑀))))) |
8 | 7 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑀 → ((𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)))) ↔ (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑀)) ∧ (2nd ‘(𝐺‘𝑀)) ≤ (2nd ‘(𝐺‘𝑀)))))) |
9 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝐺‘𝑘) = (𝐺‘𝑛)) |
10 | 9 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑛))) |
11 | 10 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑛)))) |
12 | 9 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑛))) |
13 | 12 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)) ↔ (2nd ‘(𝐺‘𝑛)) ≤ (2nd ‘(𝐺‘𝑀)))) |
14 | 11, 13 | anbi12d 743 |
. . . 4
⊢ (𝑘 = 𝑛 → (((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀))) ↔ ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑛)) ∧ (2nd ‘(𝐺‘𝑛)) ≤ (2nd ‘(𝐺‘𝑀))))) |
15 | 14 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑛 → ((𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)))) ↔ (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑛)) ∧ (2nd ‘(𝐺‘𝑛)) ≤ (2nd ‘(𝐺‘𝑀)))))) |
16 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) |
17 | 16 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘(𝑛 + 1)))) |
18 | 17 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘(𝑛 + 1))))) |
19 | 16 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = (𝑛 + 1) → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘(𝑛 + 1)))) |
20 | 19 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = (𝑛 + 1) → ((2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)) ↔ (2nd ‘(𝐺‘(𝑛 + 1))) ≤ (2nd ‘(𝐺‘𝑀)))) |
21 | 18, 20 | anbi12d 743 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → (((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀))) ↔ ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘(𝑛 + 1))) ∧ (2nd ‘(𝐺‘(𝑛 + 1))) ≤ (2nd ‘(𝐺‘𝑀))))) |
22 | 21 | imbi2d 329 |
. . 3
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)))) ↔ (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘(𝑛 + 1))) ∧ (2nd ‘(𝐺‘(𝑛 + 1))) ≤ (2nd ‘(𝐺‘𝑀)))))) |
23 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (𝐺‘𝑘) = (𝐺‘𝑁)) |
24 | 23 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (1st ‘(𝐺‘𝑘)) = (1st ‘(𝐺‘𝑁))) |
25 | 24 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ↔ (1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑁)))) |
26 | 23 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (2nd ‘(𝐺‘𝑘)) = (2nd ‘(𝐺‘𝑁))) |
27 | 26 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)) ↔ (2nd ‘(𝐺‘𝑁)) ≤ (2nd ‘(𝐺‘𝑀)))) |
28 | 25, 27 | anbi12d 743 |
. . . 4
⊢ (𝑘 = 𝑁 → (((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀))) ↔ ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑁)) ∧ (2nd ‘(𝐺‘𝑁)) ≤ (2nd ‘(𝐺‘𝑀))))) |
29 | 28 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑁 → ((𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑘)) ∧ (2nd ‘(𝐺‘𝑘)) ≤ (2nd ‘(𝐺‘𝑀)))) ↔ (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑁)) ∧ (2nd ‘(𝐺‘𝑁)) ≤ (2nd ‘(𝐺‘𝑀)))))) |
30 | | ruc.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) |
31 | | ruc.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
32 | | ruc.4 |
. . . . . . . . 9
⊢ 𝐶 = ({〈0, 〈0,
1〉〉} ∪ 𝐹) |
33 | | ruc.5 |
. . . . . . . . 9
⊢ 𝐺 = seq0(𝐷, 𝐶) |
34 | 30, 31, 32, 33 | ruclem6 14803 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
35 | | ruclem9.6 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
36 | 34, 35 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝑀) ∈ (ℝ ×
ℝ)) |
37 | | xp1st 7089 |
. . . . . . 7
⊢ ((𝐺‘𝑀) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑀)) ∈ ℝ) |
38 | 36, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1st
‘(𝐺‘𝑀)) ∈
ℝ) |
39 | 38 | leidd 10473 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑀))) |
40 | | xp2nd 7090 |
. . . . . . 7
⊢ ((𝐺‘𝑀) ∈ (ℝ × ℝ) →
(2nd ‘(𝐺‘𝑀)) ∈ ℝ) |
41 | 36, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2nd
‘(𝐺‘𝑀)) ∈
ℝ) |
42 | 41 | leidd 10473 |
. . . . 5
⊢ (𝜑 → (2nd
‘(𝐺‘𝑀)) ≤ (2nd
‘(𝐺‘𝑀))) |
43 | 39, 42 | jca 553 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑀)) ∧ (2nd
‘(𝐺‘𝑀)) ≤ (2nd
‘(𝐺‘𝑀)))) |
44 | 43 | a1i 11 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝜑 → ((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑀)) ∧ (2nd
‘(𝐺‘𝑀)) ≤ (2nd
‘(𝐺‘𝑀))))) |
45 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝐹:ℕ⟶ℝ) |
46 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦
⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) |
47 | 34 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝐺:ℕ0⟶(ℝ ×
ℝ)) |
48 | | eluznn0 11633 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑀)) → 𝑛 ∈ ℕ0) |
49 | 35, 48 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → 𝑛 ∈ ℕ0) |
50 | 47, 49 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) ∈ (ℝ ×
ℝ)) |
51 | | xp1st 7089 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(1st ‘(𝐺‘𝑛)) ∈ ℝ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘𝑛)) ∈
ℝ) |
53 | | xp2nd 7090 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(2nd ‘(𝐺‘𝑛)) ∈ ℝ) |
54 | 50, 53 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (2nd
‘(𝐺‘𝑛)) ∈
ℝ) |
55 | | nn0p1nn 11209 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝑛 + 1) ∈ ℕ) |
57 | 45, 56 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
58 | | eqid 2610 |
. . . . . . . . . 10
⊢
(1st ‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) = (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
59 | | eqid 2610 |
. . . . . . . . . 10
⊢
(2nd ‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) = (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
60 | 30, 31, 32, 33 | ruclem8 14805 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(1st ‘(𝐺‘𝑛)) < (2nd ‘(𝐺‘𝑛))) |
61 | 49, 60 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘𝑛)) < (2nd
‘(𝐺‘𝑛))) |
62 | 45, 46, 52, 54, 57, 58, 59, 61 | ruclem2 14800 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((1st
‘(𝐺‘𝑛)) ≤ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ∧ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) < (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ∧ (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ≤ (2nd ‘(𝐺‘𝑛)))) |
63 | 62 | simp1d 1066 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘𝑛)) ≤ (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
64 | 30, 31, 32, 33 | ruclem7 14804 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐺‘(𝑛 + 1)) = ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
65 | 49, 64 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘(𝑛 + 1)) = ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1)))) |
66 | | 1st2nd2 7096 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑛) ∈ (ℝ × ℝ) →
(𝐺‘𝑛) = 〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉) |
67 | 50, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑛) = 〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉) |
68 | 67 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝐺‘𝑛)𝐷(𝐹‘(𝑛 + 1))) = (〈(1st
‘(𝐺‘𝑛)), (2nd
‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
69 | 65, 68 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘(𝑛 + 1)) = (〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) |
70 | 69 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘(𝑛 + 1))) = (1st
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
71 | 63, 70 | breqtrrd 4611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘𝑛)) ≤ (1st
‘(𝐺‘(𝑛 + 1)))) |
72 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘𝑀)) ∈
ℝ) |
73 | | peano2nn0 11210 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ0) |
74 | 49, 73 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝑛 + 1) ∈
ℕ0) |
75 | 47, 74 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (𝐺‘(𝑛 + 1)) ∈ (ℝ ×
ℝ)) |
76 | | xp1st 7089 |
. . . . . . . . 9
⊢ ((𝐺‘(𝑛 + 1)) ∈ (ℝ × ℝ)
→ (1st ‘(𝐺‘(𝑛 + 1))) ∈ ℝ) |
77 | 75, 76 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (1st
‘(𝐺‘(𝑛 + 1))) ∈
ℝ) |
78 | | letr 10010 |
. . . . . . . 8
⊢
(((1st ‘(𝐺‘𝑀)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑛)) ∈ ℝ ∧
(1st ‘(𝐺‘(𝑛 + 1))) ∈ ℝ) →
(((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑛)) ∧ (1st ‘(𝐺‘𝑛)) ≤ (1st ‘(𝐺‘(𝑛 + 1)))) → (1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘(𝑛 + 1))))) |
79 | 72, 52, 77, 78 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑛)) ∧ (1st
‘(𝐺‘𝑛)) ≤ (1st
‘(𝐺‘(𝑛 + 1)))) → (1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘(𝑛 + 1))))) |
80 | 71, 79 | mpan2d 706 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑛)) → (1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘(𝑛 + 1))))) |
81 | 69 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (2nd
‘(𝐺‘(𝑛 + 1))) = (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1))))) |
82 | 62 | simp3d 1068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (2nd
‘(〈(1st ‘(𝐺‘𝑛)), (2nd ‘(𝐺‘𝑛))〉𝐷(𝐹‘(𝑛 + 1)))) ≤ (2nd ‘(𝐺‘𝑛))) |
83 | 81, 82 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑛))) |
84 | | xp2nd 7090 |
. . . . . . . . 9
⊢ ((𝐺‘(𝑛 + 1)) ∈ (ℝ × ℝ)
→ (2nd ‘(𝐺‘(𝑛 + 1))) ∈ ℝ) |
85 | 75, 84 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (2nd
‘(𝐺‘(𝑛 + 1))) ∈
ℝ) |
86 | 41 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (2nd
‘(𝐺‘𝑀)) ∈
ℝ) |
87 | | letr 10010 |
. . . . . . . 8
⊢
(((2nd ‘(𝐺‘(𝑛 + 1))) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑀)) ∈ ℝ) → (((2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑛)) ∧ (2nd
‘(𝐺‘𝑛)) ≤ (2nd
‘(𝐺‘𝑀))) → (2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑀)))) |
88 | 85, 54, 86, 87 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (((2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑛)) ∧ (2nd
‘(𝐺‘𝑛)) ≤ (2nd
‘(𝐺‘𝑀))) → (2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑀)))) |
89 | 83, 88 | mpand 707 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((2nd
‘(𝐺‘𝑛)) ≤ (2nd
‘(𝐺‘𝑀)) → (2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑀)))) |
90 | 80, 89 | anim12d 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → (((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑛)) ∧ (2nd
‘(𝐺‘𝑛)) ≤ (2nd
‘(𝐺‘𝑀))) → ((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘(𝑛 + 1))) ∧ (2nd
‘(𝐺‘(𝑛 + 1))) ≤ (2nd
‘(𝐺‘𝑀))))) |
91 | 90 | expcom 450 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝜑 → (((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑛)) ∧ (2nd ‘(𝐺‘𝑛)) ≤ (2nd ‘(𝐺‘𝑀))) → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘(𝑛 + 1))) ∧ (2nd ‘(𝐺‘(𝑛 + 1))) ≤ (2nd ‘(𝐺‘𝑀)))))) |
92 | 91 | a2d 29 |
. . 3
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑛)) ∧ (2nd ‘(𝐺‘𝑛)) ≤ (2nd ‘(𝐺‘𝑀)))) → (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘(𝑛 + 1))) ∧ (2nd ‘(𝐺‘(𝑛 + 1))) ≤ (2nd ‘(𝐺‘𝑀)))))) |
93 | 8, 15, 22, 29, 44, 92 | uzind4 11622 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑁)) ∧ (2nd ‘(𝐺‘𝑁)) ≤ (2nd ‘(𝐺‘𝑀))))) |
94 | 1, 93 | mpcom 37 |
1
⊢ (𝜑 → ((1st
‘(𝐺‘𝑀)) ≤ (1st
‘(𝐺‘𝑁)) ∧ (2nd
‘(𝐺‘𝑁)) ≤ (2nd
‘(𝐺‘𝑀)))) |