Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 0)) |
2 | 1 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = 0 → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm
0))) |
3 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 0)) |
4 | 3 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = 0 → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm
0))) |
5 | 2, 4 | anbi12d 743 |
. . . 4
⊢ (𝑎 = 0 → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm 0) ∧ 0 ≤
(𝐴 Yrm
0)))) |
6 | 5 | imbi2d 329 |
. . 3
⊢ (𝑎 = 0 → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 0) ∧ 0 ≤ (𝐴 Yrm
0))))) |
7 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 𝑏)) |
8 | 7 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = 𝑏 → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm 𝑏))) |
9 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑏)) |
10 | 9 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = 𝑏 → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm 𝑏))) |
11 | 8, 10 | anbi12d 743 |
. . . 4
⊢ (𝑎 = 𝑏 → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏)))) |
12 | 11 | imbi2d 329 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))))) |
13 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Xrm 𝑎) = (𝐴 Xrm (𝑏 + 1))) |
14 | 13 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm (𝑏 + 1)))) |
15 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 + 1))) |
16 | 15 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm (𝑏 + 1)))) |
17 | 14, 16 | anbi12d 743 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1))))) |
18 | 17 | imbi2d 329 |
. . 3
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1)))))) |
19 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 𝑁)) |
20 | 19 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = 𝑁 → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm 𝑁))) |
21 | | oveq2 6557 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑁)) |
22 | 21 | breq2d 4595 |
. . . . 5
⊢ (𝑎 = 𝑁 → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm 𝑁))) |
23 | 20, 22 | anbi12d 743 |
. . . 4
⊢ (𝑎 = 𝑁 → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁)))) |
24 | 23 | imbi2d 329 |
. . 3
⊢ (𝑎 = 𝑁 → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁))))) |
25 | | 0lt1 10429 |
. . . . 5
⊢ 0 <
1 |
26 | | rmx0 36508 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Xrm 0) = 1) |
27 | 25, 26 | syl5breqr 4621 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 < (𝐴 Xrm 0)) |
28 | | 0le0 10987 |
. . . . 5
⊢ 0 ≤
0 |
29 | | rmy0 36512 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
30 | 28, 29 | syl5breqr 4621 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 ≤ (𝐴 Yrm 0)) |
31 | 27, 30 | jca 553 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 0) ∧ 0 ≤ (𝐴 Yrm
0))) |
32 | | simp2 1055 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 𝐴 ∈
(ℤ≥‘2)) |
33 | | nn0z 11277 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℤ) |
34 | 33 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 𝑏 ∈ ℤ) |
35 | | frmx 36496 |
. . . . . . . . . . . 12
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
36 | 35 | fovcl 6663 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm 𝑏) ∈
ℕ0) |
37 | 32, 34, 36 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Xrm 𝑏) ∈
ℕ0) |
38 | 37 | nn0red 11229 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Xrm 𝑏) ∈ ℝ) |
39 | | eluzelre 11574 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℝ) |
40 | 39 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 𝐴 ∈ ℝ) |
41 | 38, 40 | remulcld 9949 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → ((𝐴 Xrm 𝑏) · 𝐴) ∈ ℝ) |
42 | | rmspecpos 36499 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ+) |
43 | 42 | rpred 11748 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ) |
44 | 43 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → ((𝐴↑2) − 1) ∈
ℝ) |
45 | | frmy 36497 |
. . . . . . . . . . . 12
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
46 | 45 | fovcl 6663 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) |
47 | 32, 34, 46 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Yrm 𝑏) ∈ ℤ) |
48 | 47 | zred 11358 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Yrm 𝑏) ∈ ℝ) |
49 | 44, 48 | remulcld 9949 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)) ∈
ℝ) |
50 | | simp3l 1082 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < (𝐴 Xrm 𝑏)) |
51 | | eluz2nn 11602 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
52 | 51 | nngt0d 10941 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 < 𝐴) |
53 | 52 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < 𝐴) |
54 | 38, 40, 50, 53 | mulgt0d 10071 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < ((𝐴 Xrm 𝑏) · 𝐴)) |
55 | 42 | rpge0d 11752 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 ≤ ((𝐴↑2) − 1)) |
56 | 55 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ ((𝐴↑2) − 1)) |
57 | | simp3r 1083 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (𝐴 Yrm 𝑏)) |
58 | 44, 48, 56, 57 | mulge0d 10483 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏))) |
59 | | addgtge0 10395 |
. . . . . . . 8
⊢
(((((𝐴
Xrm 𝑏) ·
𝐴) ∈ ℝ ∧
(((𝐴↑2) − 1)
· (𝐴 Yrm
𝑏)) ∈ ℝ) ∧
(0 < ((𝐴 Xrm
𝑏) · 𝐴) ∧ 0 ≤ (((𝐴↑2) − 1) ·
(𝐴 Yrm 𝑏)))) → 0 < (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
60 | 41, 49, 54, 58, 59 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
61 | | rmxp1 36515 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm (𝑏 + 1)) = (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
62 | 32, 34, 61 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Xrm (𝑏 + 1)) = (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
63 | 60, 62 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < (𝐴 Xrm (𝑏 + 1))) |
64 | 48, 40 | remulcld 9949 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → ((𝐴 Yrm 𝑏) · 𝐴) ∈ ℝ) |
65 | | eluzge2nn0 11603 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈
ℕ0) |
66 | 65 | nn0ge0d 11231 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 ≤ 𝐴) |
67 | 66 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ 𝐴) |
68 | 48, 40, 57, 67 | mulge0d 10483 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ ((𝐴 Yrm 𝑏) · 𝐴)) |
69 | 37 | nn0ge0d 11231 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (𝐴 Xrm 𝑏)) |
70 | 64, 38, 68, 69 | addge0d 10482 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (((𝐴 Yrm 𝑏) · 𝐴) + (𝐴 Xrm 𝑏))) |
71 | | rmyp1 36516 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) = (((𝐴 Yrm 𝑏) · 𝐴) + (𝐴 Xrm 𝑏))) |
72 | 32, 34, 71 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Yrm (𝑏 + 1)) = (((𝐴 Yrm 𝑏) · 𝐴) + (𝐴 Xrm 𝑏))) |
73 | 70, 72 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (𝐴 Yrm (𝑏 + 1))) |
74 | 63, 73 | jca 553 |
. . . . 5
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1)))) |
75 | 74 | 3exp 1256 |
. . . 4
⊢ (𝑏 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → ((0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏)) → (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1)))))) |
76 | 75 | a2d 29 |
. . 3
⊢ (𝑏 ∈ ℕ0
→ ((𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm (𝑏 + 1))
∧ 0 ≤ (𝐴
Yrm (𝑏 +
1)))))) |
77 | 6, 12, 18, 24, 31, 76 | nn0ind 11348 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁)))) |
78 | 77 | impcom 445 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (0 <
(𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁))) |