| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 0)) |
| 2 | 1 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = 0 → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm
0))) |
| 3 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 0 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 0)) |
| 4 | 3 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = 0 → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm
0))) |
| 5 | 2, 4 | anbi12d 632 |
. . . 4
⊢ (𝑎 = 0 → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm 0) ∧ 0 ≤
(𝐴 Yrm
0)))) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑎 = 0 → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 0) ∧ 0 ≤ (𝐴 Yrm
0))))) |
| 7 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 𝑏)) |
| 8 | 7 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = 𝑏 → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm 𝑏))) |
| 9 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑏)) |
| 10 | 9 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = 𝑏 → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm 𝑏))) |
| 11 | 8, 10 | anbi12d 632 |
. . . 4
⊢ (𝑎 = 𝑏 → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏)))) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))))) |
| 13 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Xrm 𝑎) = (𝐴 Xrm (𝑏 + 1))) |
| 14 | 13 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm (𝑏 + 1)))) |
| 15 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 + 1))) |
| 16 | 15 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm (𝑏 + 1)))) |
| 17 | 14, 16 | anbi12d 632 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1))))) |
| 18 | 17 | imbi2d 340 |
. . 3
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1)))))) |
| 19 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 𝑁)) |
| 20 | 19 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = 𝑁 → (0 < (𝐴 Xrm 𝑎) ↔ 0 < (𝐴 Xrm 𝑁))) |
| 21 | | oveq2 7439 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑁)) |
| 22 | 21 | breq2d 5155 |
. . . . 5
⊢ (𝑎 = 𝑁 → (0 ≤ (𝐴 Yrm 𝑎) ↔ 0 ≤ (𝐴 Yrm 𝑁))) |
| 23 | 20, 22 | anbi12d 632 |
. . . 4
⊢ (𝑎 = 𝑁 → ((0 < (𝐴 Xrm 𝑎) ∧ 0 ≤ (𝐴 Yrm 𝑎)) ↔ (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁)))) |
| 24 | 23 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑁 → ((𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm 𝑎) ∧ 0
≤ (𝐴 Yrm
𝑎))) ↔ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁))))) |
| 25 | | 0lt1 11785 |
. . . . 5
⊢ 0 <
1 |
| 26 | | rmx0 42937 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Xrm 0) = 1) |
| 27 | 25, 26 | breqtrrid 5181 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 < (𝐴 Xrm 0)) |
| 28 | | 0le0 12367 |
. . . . 5
⊢ 0 ≤
0 |
| 29 | | rmy0 42941 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
| 30 | 28, 29 | breqtrrid 5181 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 ≤ (𝐴 Yrm 0)) |
| 31 | 27, 30 | jca 511 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 0) ∧ 0 ≤ (𝐴 Yrm
0))) |
| 32 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 𝐴 ∈
(ℤ≥‘2)) |
| 33 | | nn0z 12638 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℤ) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 𝑏 ∈ ℤ) |
| 35 | | frmx 42925 |
. . . . . . . . . . . 12
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
| 36 | 35 | fovcl 7561 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm 𝑏) ∈
ℕ0) |
| 37 | 32, 34, 36 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Xrm 𝑏) ∈
ℕ0) |
| 38 | 37 | nn0red 12588 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Xrm 𝑏) ∈ ℝ) |
| 39 | | eluzelre 12889 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℝ) |
| 40 | 39 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 𝐴 ∈ ℝ) |
| 41 | 38, 40 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → ((𝐴 Xrm 𝑏) · 𝐴) ∈ ℝ) |
| 42 | | rmspecpos 42928 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ+) |
| 43 | 42 | rpred 13077 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → ((𝐴↑2) − 1) ∈
ℝ) |
| 44 | 43 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → ((𝐴↑2) − 1) ∈
ℝ) |
| 45 | | frmy 42926 |
. . . . . . . . . . . 12
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 46 | 45 | fovcl 7561 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) |
| 47 | 32, 34, 46 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Yrm 𝑏) ∈ ℤ) |
| 48 | 47 | zred 12722 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Yrm 𝑏) ∈ ℝ) |
| 49 | 44, 48 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)) ∈
ℝ) |
| 50 | | simp3l 1202 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < (𝐴 Xrm 𝑏)) |
| 51 | | eluz2nn 12924 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
| 52 | 51 | nngt0d 12315 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 < 𝐴) |
| 53 | 52 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < 𝐴) |
| 54 | 38, 40, 50, 53 | mulgt0d 11416 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < ((𝐴 Xrm 𝑏) · 𝐴)) |
| 55 | 42 | rpge0d 13081 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 ≤ ((𝐴↑2) − 1)) |
| 56 | 55 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ ((𝐴↑2) − 1)) |
| 57 | | simp3r 1203 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (𝐴 Yrm 𝑏)) |
| 58 | 44, 48, 56, 57 | mulge0d 11840 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏))) |
| 59 | 41, 49, 54, 58 | addgtge0d 11837 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
| 60 | | rmxp1 42944 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm (𝑏 + 1)) = (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
| 61 | 32, 34, 60 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Xrm (𝑏 + 1)) = (((𝐴 Xrm 𝑏) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑏)))) |
| 62 | 59, 61 | breqtrrd 5171 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 < (𝐴 Xrm (𝑏 + 1))) |
| 63 | 48, 40 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → ((𝐴 Yrm 𝑏) · 𝐴) ∈ ℝ) |
| 64 | | eluzge2nn0 12929 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈
ℕ0) |
| 65 | 64 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → 0 ≤ 𝐴) |
| 66 | 65 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ 𝐴) |
| 67 | 48, 40, 57, 66 | mulge0d 11840 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ ((𝐴 Yrm 𝑏) · 𝐴)) |
| 68 | 37 | nn0ge0d 12590 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (𝐴 Xrm 𝑏)) |
| 69 | 63, 38, 67, 68 | addge0d 11839 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (((𝐴 Yrm 𝑏) · 𝐴) + (𝐴 Xrm 𝑏))) |
| 70 | | rmyp1 42945 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) = (((𝐴 Yrm 𝑏) · 𝐴) + (𝐴 Xrm 𝑏))) |
| 71 | 32, 34, 70 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 Yrm (𝑏 + 1)) = (((𝐴 Yrm 𝑏) · 𝐴) + (𝐴 Xrm 𝑏))) |
| 72 | 69, 71 | breqtrrd 5171 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → 0 ≤ (𝐴 Yrm (𝑏 + 1))) |
| 73 | 62, 72 | jca 511 |
. . . . 5
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1)))) |
| 74 | 73 | 3exp 1120 |
. . . 4
⊢ (𝑏 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → ((0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏)) → (0 < (𝐴 Xrm (𝑏 + 1)) ∧ 0 ≤ (𝐴 Yrm (𝑏 + 1)))))) |
| 75 | 74 | a2d 29 |
. . 3
⊢ (𝑏 ∈ ℕ0
→ ((𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑏) ∧ 0 ≤ (𝐴 Yrm 𝑏))) → (𝐴 ∈ (ℤ≥‘2)
→ (0 < (𝐴
Xrm (𝑏 + 1))
∧ 0 ≤ (𝐴
Yrm (𝑏 +
1)))))) |
| 76 | 6, 12, 18, 24, 31, 75 | nn0ind 12713 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁)))) |
| 77 | 76 | impcom 407 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (0 <
(𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁))) |