| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2z 12651 | . . . . . . . . . 10
⊢ 2 ∈
ℤ | 
| 2 |  | eluzelz 12889 | . . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) | 
| 3 | 2 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → 𝐴 ∈
ℤ) | 
| 4 |  | zmulcl 12668 | . . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ 𝐴
∈ ℤ) → (2 · 𝐴) ∈ ℤ) | 
| 5 | 1, 3, 4 | sylancr 587 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (2
· 𝐴) ∈
ℤ) | 
| 6 |  | nn0z 12640 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) | 
| 7 | 6 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℤ) | 
| 8 | 5, 7 | zmulcld 12730 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((2
· 𝐴) · 𝐾) ∈
ℤ) | 
| 9 |  | zsqcl 14170 | . . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (𝐾↑2) ∈
ℤ) | 
| 10 | 7, 9 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾↑2) ∈
ℤ) | 
| 11 | 8, 10 | zsubcld 12729 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((2
· 𝐴) · 𝐾) − (𝐾↑2)) ∈ ℤ) | 
| 12 |  | peano2zm 12662 | . . . . . . 7
⊢ ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) ∈ ℤ → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈
ℤ) | 
| 13 | 11, 12 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈
ℤ) | 
| 14 |  | dvds0 16310 | . . . . . 6
⊢ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ →
((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) − 1) ∥
0) | 
| 15 | 13, 14 | syl 17 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥
0) | 
| 16 |  | rmx0 42942 | . . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Xrm 0) = 1) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 Xrm 0) =
1) | 
| 18 |  | rmy0 42946 | . . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) | 
| 19 | 18 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 Yrm 0) =
0) | 
| 20 | 19 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 − 𝐾) · (𝐴 Yrm 0)) = ((𝐴 − 𝐾) · 0)) | 
| 21 | 3, 7 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 − 𝐾) ∈ ℤ) | 
| 22 | 21 | zcnd 12725 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 − 𝐾) ∈ ℂ) | 
| 23 | 22 | mul01d 11461 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 − 𝐾) · 0) = 0) | 
| 24 | 20, 23 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 − 𝐾) · (𝐴 Yrm 0)) = 0) | 
| 25 | 17, 24 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) = (1 −
0)) | 
| 26 |  | 1m0e1 12388 | . . . . . . . 8
⊢ (1
− 0) = 1 | 
| 27 | 25, 26 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) = 1) | 
| 28 |  | nn0cn 12538 | . . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) | 
| 29 | 28 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℂ) | 
| 30 | 29 | exp0d 14181 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾↑0) = 1) | 
| 31 | 27, 30 | oveq12d 7450 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) − (𝐾↑0)) = (1 −
1)) | 
| 32 |  | 1m1e0 12339 | . . . . . 6
⊢ (1
− 1) = 0 | 
| 33 | 31, 32 | eqtrdi 2792 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) − (𝐾↑0)) = 0) | 
| 34 | 15, 33 | breqtrrd 5170 | . . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) − (𝐾↑0))) | 
| 35 |  | rmx1 42943 | . . . . . . . . . 10
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Xrm 1) = 𝐴) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 Xrm 1) = 𝐴) | 
| 37 |  | rmy1 42947 | . . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 1) = 1) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 Yrm 1) =
1) | 
| 39 | 38 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 − 𝐾) · (𝐴 Yrm 1)) = ((𝐴 − 𝐾) · 1)) | 
| 40 | 22 | mulridd 11279 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 − 𝐾) · 1) = (𝐴 − 𝐾)) | 
| 41 | 39, 40 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 − 𝐾) · (𝐴 Yrm 1)) = (𝐴 − 𝐾)) | 
| 42 | 36, 41 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) = (𝐴 − (𝐴 − 𝐾))) | 
| 43 | 3 | zcnd 12725 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → 𝐴 ∈
ℂ) | 
| 44 | 43, 29 | nncand 11626 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐴 − (𝐴 − 𝐾)) = 𝐾) | 
| 45 | 42, 44 | eqtrd 2776 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) = 𝐾) | 
| 46 | 29 | exp1d 14182 | . . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾↑1) = 𝐾) | 
| 47 | 45, 46 | oveq12d 7450 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) − (𝐾↑1)) = (𝐾 − 𝐾)) | 
| 48 | 29 | subidd 11609 | . . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾 − 𝐾) = 0) | 
| 49 | 47, 48 | eqtrd 2776 | . . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) − (𝐾↑1)) = 0) | 
| 50 | 15, 49 | breqtrrd 5170 | . . . 4
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) − (𝐾↑1))) | 
| 51 |  | pm3.43 473 | . . . . 5
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1)))) ∧ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))))) | 
| 52 | 13 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈
ℤ) | 
| 53 | 5 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (2
· 𝐴) ∈
ℤ) | 
| 54 |  | simpll 766 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝐴 ∈
(ℤ≥‘2)) | 
| 55 |  | nnz 12636 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℤ) | 
| 56 | 55 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝑏 ∈
ℤ) | 
| 57 |  | frmx 42930 | . . . . . . . . . . . . . . . . . 18
⊢ 
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 | 
| 58 | 57 | fovcl 7562 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm 𝑏) ∈
ℕ0) | 
| 59 | 54, 56, 58 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm 𝑏) ∈
ℕ0) | 
| 60 | 59 | nn0zd 12641 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm 𝑏) ∈
ℤ) | 
| 61 | 21 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 − 𝐾) ∈ ℤ) | 
| 62 |  | frmy 42931 | . . . . . . . . . . . . . . . . . 18
⊢ 
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ | 
| 63 | 62 | fovcl 7562 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) | 
| 64 | 54, 56, 63 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Yrm 𝑏) ∈
ℤ) | 
| 65 | 61, 64 | zmulcld 12730 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)) ∈ ℤ) | 
| 66 | 60, 65 | zsubcld 12729 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) ∈ ℤ) | 
| 67 | 53, 66 | zmulcld 12730 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) ∈ ℤ) | 
| 68 |  | peano2zm 12662 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ ℤ → (𝑏 − 1) ∈
ℤ) | 
| 69 | 56, 68 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝑏 − 1) ∈
ℤ) | 
| 70 | 57 | fovcl 7562 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Xrm (𝑏 − 1)) ∈
ℕ0) | 
| 71 | 54, 69, 70 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm (𝑏 − 1)) ∈
ℕ0) | 
| 72 | 71 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm (𝑏 − 1)) ∈
ℤ) | 
| 73 | 62 | fovcl 7562 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℤ) | 
| 74 | 54, 69, 73 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℤ) | 
| 75 | 61, 74 | zmulcld 12730 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))) ∈
ℤ) | 
| 76 | 72, 75 | zsubcld 12729 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) ∈
ℤ) | 
| 77 | 67, 76 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((2
· 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) ∈
ℤ) | 
| 78 | 52, 77 | jca 511 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
(((2 · 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) ∈
ℤ)) | 
| 79 | 78 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
(((2 · 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) ∈
ℤ)) | 
| 80 | 7 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝐾 ∈
ℤ) | 
| 81 |  | nnnn0 12535 | . . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℕ0) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝑏 ∈
ℕ0) | 
| 83 |  | zexpcl 14118 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑏 ∈ ℕ0)
→ (𝐾↑𝑏) ∈
ℤ) | 
| 84 | 80, 82, 83 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑𝑏) ∈ ℤ) | 
| 85 | 53, 84 | zmulcld 12730 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) · (𝐾↑𝑏)) ∈ ℤ) | 
| 86 |  | nnm1nn0 12569 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℕ → (𝑏 − 1) ∈
ℕ0) | 
| 87 | 86 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝑏 − 1) ∈
ℕ0) | 
| 88 |  | zexpcl 14118 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ (𝑏 − 1) ∈
ℕ0) → (𝐾↑(𝑏 − 1)) ∈ ℤ) | 
| 89 | 80, 87, 88 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑(𝑏 − 1)) ∈ ℤ) | 
| 90 | 85, 89 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((2
· 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) ∈
ℤ) | 
| 91 |  | 0z 12626 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ | 
| 92 |  | zaddcl 12659 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℤ ∧ (𝐾↑2) ∈ ℤ) → (0 + (𝐾↑2)) ∈
ℤ) | 
| 93 | 91, 10, 92 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (0 +
(𝐾↑2)) ∈
ℤ) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (0 +
(𝐾↑2)) ∈
ℤ) | 
| 95 | 89, 94 | zmulcld 12730 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))) ∈ ℤ) | 
| 96 | 90, 95 | jca 511 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) ∈ ℤ ∧ ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))) ∈ ℤ)) | 
| 97 | 96 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) ∈ ℤ ∧ ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))) ∈ ℤ)) | 
| 98 | 52, 67, 85 | 3jca 1128 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
((2 · 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) ∈ ℤ ∧ ((2 · 𝐴) · (𝐾↑𝑏)) ∈ ℤ)) | 
| 99 | 98 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
((2 · 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) ∈ ℤ ∧ ((2 · 𝐴) · (𝐾↑𝑏)) ∈ ℤ)) | 
| 100 | 76, 89 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) ∈ ℤ ∧ (𝐾↑(𝑏 − 1)) ∈
ℤ)) | 
| 101 | 100 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) ∈ ℤ ∧ (𝐾↑(𝑏 − 1)) ∈
ℤ)) | 
| 102 | 13, 5, 5 | 3jca 1128 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧ (2
· 𝐴) ∈ ℤ
∧ (2 · 𝐴) ∈
ℤ)) | 
| 103 | 102 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧ (2
· 𝐴) ∈ ℤ
∧ (2 · 𝐴) ∈
ℤ)) | 
| 104 | 66, 84 | jca 511 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) ∈ ℤ ∧ (𝐾↑𝑏) ∈ ℤ)) | 
| 105 | 104 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) ∈ ℤ ∧ (𝐾↑𝑏) ∈ ℤ)) | 
| 106 |  | congid 42988 | . . . . . . . . . . . . . . 15
⊢ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧ (2
· 𝐴) ∈ ℤ)
→ ((((2 · 𝐴)
· 𝐾) − (𝐾↑2)) − 1) ∥ ((2
· 𝐴) − (2
· 𝐴))) | 
| 107 | 13, 5, 106 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((2 ·
𝐴) − (2 ·
𝐴))) | 
| 108 | 107 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((2 ·
𝐴) − (2 ·
𝐴))) | 
| 109 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) | 
| 110 |  | congmul 42984 | . . . . . . . . . . . . 13
⊢ (((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧ (2
· 𝐴) ∈ ℤ
∧ (2 · 𝐴) ∈
ℤ) ∧ (((𝐴
Xrm 𝑏) −
((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) ∈ ℤ ∧ (𝐾↑𝑏) ∈ ℤ) ∧ (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((2 ·
𝐴) − (2 ·
𝐴)) ∧ ((((2 ·
𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((2 · 𝐴) · (𝐾↑𝑏)))) | 
| 111 | 103, 105,
108, 109, 110 | syl112anc 1375 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((2 · 𝐴) · (𝐾↑𝑏)))) | 
| 112 | 111 | adantrl 716 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((2 · 𝐴) · (𝐾↑𝑏)))) | 
| 113 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1)))) | 
| 114 |  | congsub 42987 | . . . . . . . . . . 11
⊢ (((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
((2 · 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) ∈ ℤ ∧ ((2 · 𝐴) · (𝐾↑𝑏)) ∈ ℤ) ∧ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) ∈ ℤ ∧ (𝐾↑(𝑏 − 1)) ∈ ℤ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((2 · 𝐴) · (𝐾↑𝑏))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − (((2 · 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))))) | 
| 115 | 99, 101, 112, 113, 114 | syl112anc 1375 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − (((2 · 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))))) | 
| 116 | 13, 10 | zaddcld 12728 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) ∈ ℤ) | 
| 117 | 116 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) ∈ ℤ) | 
| 118 |  | congid 42988 | . . . . . . . . . . . . . 14
⊢ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
(𝐾↑(𝑏 − 1)) ∈ ℤ) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((𝐾↑(𝑏 − 1)) − (𝐾↑(𝑏 − 1)))) | 
| 119 | 52, 89, 118 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((𝐾↑(𝑏 − 1)) − (𝐾↑(𝑏 − 1)))) | 
| 120 |  | 0zd 12627 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → 0 ∈
ℤ) | 
| 121 |  | iddvds 16308 | . . . . . . . . . . . . . . . . 17
⊢ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ →
((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) − 1) ∥
((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) −
1)) | 
| 122 | 13, 121 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · 𝐾) − (𝐾↑2)) − 1)) | 
| 123 | 13 | zcnd 12725 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈
ℂ) | 
| 124 | 123 | subid1d 11610 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) − 0) = ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1)) | 
| 125 | 122, 124 | breqtrrd 5170 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((((2 ·
𝐴) · 𝐾) − (𝐾↑2)) − 1) −
0)) | 
| 126 |  | congid 42988 | . . . . . . . . . . . . . . . 16
⊢ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
(𝐾↑2) ∈ ℤ)
→ ((((2 · 𝐴)
· 𝐾) − (𝐾↑2)) − 1) ∥
((𝐾↑2) − (𝐾↑2))) | 
| 127 | 13, 10, 126 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((𝐾↑2) − (𝐾↑2))) | 
| 128 |  | congadd 42983 | . . . . . . . . . . . . . . 15
⊢ (((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) − 1) ∈
ℤ ∧ 0 ∈ ℤ) ∧ ((𝐾↑2) ∈ ℤ ∧ (𝐾↑2) ∈ ℤ) ∧
(((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) − 1) ∥
(((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) − 1) − 0)
∧ ((((2 · 𝐴)
· 𝐾) − (𝐾↑2)) − 1) ∥
((𝐾↑2) − (𝐾↑2)))) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) − (0 + (𝐾↑2)))) | 
| 129 | 13, 13, 120, 10, 10, 125, 127, 128 | syl322anc 1399 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) − (0 + (𝐾↑2)))) | 
| 130 | 129 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) − (0 + (𝐾↑2)))) | 
| 131 |  | congmul 42984 | . . . . . . . . . . . . 13
⊢ (((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
(𝐾↑(𝑏 − 1)) ∈ ℤ ∧ (𝐾↑(𝑏 − 1)) ∈ ℤ) ∧ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) ∈ ℤ ∧ (0 + (𝐾↑2)) ∈ ℤ) ∧
(((((2 · 𝐴) ·
𝐾) − (𝐾↑2)) − 1) ∥
((𝐾↑(𝑏 − 1)) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) − (0 + (𝐾↑2))))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐾↑(𝑏 − 1)) · (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 132 | 52, 89, 89, 117, 94, 119, 130, 131 | syl322anc 1399 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐾↑(𝑏 − 1)) · (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 133 | 11 | zcnd 12725 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((2
· 𝐴) · 𝐾) − (𝐾↑2)) ∈ ℂ) | 
| 134 | 29 | sqcld 14185 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾↑2) ∈
ℂ) | 
| 135 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → 1 ∈
ℂ) | 
| 136 | 133, 134,
135 | addsubd 11642 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) + (𝐾↑2)) − 1) = (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2))) | 
| 137 | 8 | zcnd 12725 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((2
· 𝐴) · 𝐾) ∈
ℂ) | 
| 138 | 137, 134 | npcand 11625 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) + (𝐾↑2)) = ((2 · 𝐴) · 𝐾)) | 
| 139 | 138 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) + (𝐾↑2)) − 1) = (((2 · 𝐴) · 𝐾) − 1)) | 
| 140 | 136, 139 | eqtr3d 2778 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) = (((2 · 𝐴) · 𝐾) − 1)) | 
| 141 | 140 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)) = (((2 · 𝐴) · 𝐾) − 1)) | 
| 142 | 141 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2))) = ((𝐾↑(𝑏 − 1)) · (((2 · 𝐴) · 𝐾) − 1))) | 
| 143 | 28 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝐾 ∈
ℂ) | 
| 144 | 143, 87 | expcld 14187 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑(𝑏 − 1)) ∈ ℂ) | 
| 145 | 137 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) · 𝐾) ∈
ℂ) | 
| 146 |  | 1cnd 11257 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 1 ∈
ℂ) | 
| 147 | 144, 145,
146 | subdid 11720 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · (((2 · 𝐴) · 𝐾) − 1)) = (((𝐾↑(𝑏 − 1)) · ((2 · 𝐴) · 𝐾)) − ((𝐾↑(𝑏 − 1)) · 1))) | 
| 148 | 5 | zcnd 12725 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (2
· 𝐴) ∈
ℂ) | 
| 149 | 148 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (2
· 𝐴) ∈
ℂ) | 
| 150 | 144, 149,
143 | mul12d 11471 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · ((2 · 𝐴) · 𝐾)) = ((2 · 𝐴) · ((𝐾↑(𝑏 − 1)) · 𝐾))) | 
| 151 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝑏 ∈
ℕ) | 
| 152 |  | expm1t 14132 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℂ ∧ 𝑏 ∈ ℕ) → (𝐾↑𝑏) = ((𝐾↑(𝑏 − 1)) · 𝐾)) | 
| 153 | 143, 151,
152 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑𝑏) = ((𝐾↑(𝑏 − 1)) · 𝐾)) | 
| 154 | 153 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) · (𝐾↑𝑏)) = ((2 · 𝐴) · ((𝐾↑(𝑏 − 1)) · 𝐾))) | 
| 155 | 150, 154 | eqtr4d 2779 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · ((2 · 𝐴) · 𝐾)) = ((2 · 𝐴) · (𝐾↑𝑏))) | 
| 156 | 144 | mulridd 11279 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · 1) = (𝐾↑(𝑏 − 1))) | 
| 157 | 155, 156 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐾↑(𝑏 − 1)) · ((2 · 𝐴) · 𝐾)) − ((𝐾↑(𝑏 − 1)) · 1)) = (((2 ·
𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1)))) | 
| 158 | 142, 147,
157 | 3eqtrrd 2781 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((2
· 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) = ((𝐾↑(𝑏 − 1)) · (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2)))) | 
| 159 | 158 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2)))) = (((𝐾↑(𝑏 − 1)) · (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) + (𝐾↑2))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 160 | 132, 159 | breqtrrd 5170 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 161 | 160 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 162 |  | congtr 42982 | . . . . . . . . . 10
⊢ (((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℤ ∧
(((2 · 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) ∈ ℤ) ∧ ((((2
· 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) ∈ ℤ ∧ ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))) ∈ ℤ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − (((2 · 𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1)))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · (𝐾↑𝑏)) − (𝐾↑(𝑏 − 1))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2)))))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 163 | 79, 97, 115, 161, 162 | syl112anc 1375 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ ((((2 ·
𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 164 |  | rmxluc 42953 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm (𝑏 + 1)) = (((2 · 𝐴) · (𝐴 Xrm 𝑏)) − (𝐴 Xrm (𝑏 − 1)))) | 
| 165 | 54, 56, 164 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm (𝑏 + 1)) = (((2 · 𝐴) · (𝐴 Xrm 𝑏)) − (𝐴 Xrm (𝑏 − 1)))) | 
| 166 |  | rmyluc 42954 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) | 
| 167 | 54, 56, 166 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Yrm (𝑏 + 1)) = ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) | 
| 168 | 167 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1))) = ((𝐴 − 𝐾) · ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1))))) | 
| 169 | 2 | zcnd 12725 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℂ) | 
| 170 | 169 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝐴 ∈
ℂ) | 
| 171 | 170, 143 | subcld 11621 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 − 𝐾) ∈ ℂ) | 
| 172 |  | 2cn 12342 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ | 
| 173 | 63 | zcnd 12725 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℂ) | 
| 174 | 54, 56, 173 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Yrm 𝑏) ∈
ℂ) | 
| 175 | 174, 170 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 Yrm 𝑏) · 𝐴) ∈ ℂ) | 
| 176 |  | mulcl 11240 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ ((𝐴
Yrm 𝑏) ·
𝐴) ∈ ℂ) →
(2 · ((𝐴
Yrm 𝑏) ·
𝐴)) ∈
ℂ) | 
| 177 | 172, 175,
176 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (2
· ((𝐴 Yrm
𝑏) · 𝐴)) ∈
ℂ) | 
| 178 | 73 | zcnd 12725 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℂ) | 
| 179 | 54, 69, 178 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Yrm (𝑏 − 1)) ∈
ℂ) | 
| 180 | 171, 177,
179 | subdid 11720 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · ((2 · ((𝐴 Yrm 𝑏) · 𝐴)) − (𝐴 Yrm (𝑏 − 1)))) = (((𝐴 − 𝐾) · (2 · ((𝐴 Yrm 𝑏) · 𝐴))) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) | 
| 181 |  | 2cnd 12345 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 2 ∈
ℂ) | 
| 182 | 181, 174,
170 | mul12d 11471 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (2
· ((𝐴 Yrm
𝑏) · 𝐴)) = ((𝐴 Yrm 𝑏) · (2 · 𝐴))) | 
| 183 | 174, 149 | mulcomd 11283 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 Yrm 𝑏) · (2 · 𝐴)) = ((2 · 𝐴) · (𝐴 Yrm 𝑏))) | 
| 184 | 182, 183 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (2
· ((𝐴 Yrm
𝑏) · 𝐴)) = ((2 · 𝐴) · (𝐴 Yrm 𝑏))) | 
| 185 | 184 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (2 · ((𝐴 Yrm 𝑏) · 𝐴))) = ((𝐴 − 𝐾) · ((2 · 𝐴) · (𝐴 Yrm 𝑏)))) | 
| 186 | 171, 149,
174 | mul12d 11471 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · ((2 · 𝐴) · (𝐴 Yrm 𝑏))) = ((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) | 
| 187 | 185, 186 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (2 · ((𝐴 Yrm 𝑏) · 𝐴))) = ((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) | 
| 188 | 187 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐴 − 𝐾) · (2 · ((𝐴 Yrm 𝑏) · 𝐴))) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) = (((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) | 
| 189 | 168, 180,
188 | 3eqtrd 2780 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1))) = (((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) | 
| 190 | 165, 189 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) = ((((2 · 𝐴) · (𝐴 Xrm 𝑏)) − (𝐴 Xrm (𝑏 − 1))) − (((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))))) | 
| 191 | 58 | nn0cnd 12591 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Xrm 𝑏) ∈ ℂ) | 
| 192 | 54, 56, 191 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm 𝑏) ∈
ℂ) | 
| 193 | 149, 192 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) · (𝐴 Xrm 𝑏)) ∈
ℂ) | 
| 194 | 70 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 − 1) ∈ ℤ) → (𝐴 Xrm (𝑏 − 1)) ∈
ℂ) | 
| 195 | 54, 69, 194 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐴 Xrm (𝑏 − 1)) ∈
ℂ) | 
| 196 | 171, 174 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)) ∈ ℂ) | 
| 197 | 149, 196 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) ·
((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) ∈ ℂ) | 
| 198 | 171, 179 | mulcld 11282 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))) ∈
ℂ) | 
| 199 | 193, 195,
197, 198 | sub4d 11670 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · (𝐴 Xrm 𝑏)) − (𝐴 Xrm (𝑏 − 1))) − (((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) = ((((2 · 𝐴) · (𝐴 Xrm 𝑏)) − ((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))))) | 
| 200 | 149, 192,
196 | subdid 11720 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((2
· 𝐴) ·
((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) = (((2 · 𝐴) · (𝐴 Xrm 𝑏)) − ((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))))) | 
| 201 | 200 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((2
· 𝐴) · (𝐴 Xrm 𝑏)) − ((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) = ((2 · 𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))))) | 
| 202 | 201 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((2
· 𝐴) · (𝐴 Xrm 𝑏)) − ((2 · 𝐴) · ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) = (((2 · 𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))))) | 
| 203 | 190, 199,
202 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) = (((2 · 𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))))) | 
| 204 | 143, 82 | expp1d 14188 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑(𝑏 + 1)) = ((𝐾↑𝑏) · 𝐾)) | 
| 205 |  | nncn 12275 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ ℕ → 𝑏 ∈
ℂ) | 
| 206 | 205 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → 𝑏 ∈
ℂ) | 
| 207 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ | 
| 208 |  | npcan 11518 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑏 −
1) + 1) = 𝑏) | 
| 209 | 206, 207,
208 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝑏 − 1) + 1) = 𝑏) | 
| 210 | 209 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑((𝑏 − 1) + 1)) = (𝐾↑𝑏)) | 
| 211 | 143, 87 | expp1d 14188 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑((𝑏 − 1) + 1)) = ((𝐾↑(𝑏 − 1)) · 𝐾)) | 
| 212 | 210, 211 | eqtr3d 2778 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑𝑏) = ((𝐾↑(𝑏 − 1)) · 𝐾)) | 
| 213 | 212 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑𝑏) · 𝐾) = (((𝐾↑(𝑏 − 1)) · 𝐾) · 𝐾)) | 
| 214 | 144, 143,
143 | mulassd 11285 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐾↑(𝑏 − 1)) · 𝐾) · 𝐾) = ((𝐾↑(𝑏 − 1)) · (𝐾 · 𝐾))) | 
| 215 | 134 | addlidd 11463 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (0 +
(𝐾↑2)) = (𝐾↑2)) | 
| 216 | 29 | sqvald 14184 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾↑2) = (𝐾 · 𝐾)) | 
| 217 | 215, 216 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (𝐾 · 𝐾) = (0 + (𝐾↑2))) | 
| 218 | 217 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾 · 𝐾) = (0 + (𝐾↑2))) | 
| 219 | 218 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((𝐾↑(𝑏 − 1)) · (𝐾 · 𝐾)) = ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2)))) | 
| 220 | 214, 219 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐾↑(𝑏 − 1)) · 𝐾) · 𝐾) = ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2)))) | 
| 221 | 204, 213,
220 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (𝐾↑(𝑏 + 1)) = ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2)))) | 
| 222 | 203, 221 | oveq12d 7450 | . . . . . . . . . 10
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1))) = ((((2 · 𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 223 | 222 | adantr 480 | . . . . . . . . 9
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1))) = ((((2 · 𝐴) · ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) − ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) − ((𝐾↑(𝑏 − 1)) · (0 + (𝐾↑2))))) | 
| 224 | 163, 223 | breqtrrd 5170 | . . . . . . . 8
⊢ ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) ∧ (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1)))) | 
| 225 | 224 | ex 412 | . . . . . . 7
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑏 ∈ ℕ) → ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1))))) | 
| 226 | 225 | expcom 413 | . . . . . 6
⊢ (𝑏 ∈ ℕ → ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1)))))) | 
| 227 | 226 | a2d 29 | . . . . 5
⊢ (𝑏 ∈ ℕ → (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → (((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))) ∧ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1)))))) | 
| 228 | 51, 227 | syl5 34 | . . . 4
⊢ (𝑏 ∈ ℕ → ((((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1)))) ∧ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) → ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1)))))) | 
| 229 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑎 = 0 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 0)) | 
| 230 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑎 = 0 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 0)) | 
| 231 | 230 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = 0 → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎)) = ((𝐴 − 𝐾) · (𝐴 Yrm 0))) | 
| 232 | 229, 231 | oveq12d 7450 | . . . . . . 7
⊢ (𝑎 = 0 → ((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) = ((𝐴 Xrm 0) − ((𝐴 − 𝐾) · (𝐴 Yrm 0)))) | 
| 233 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 0 → (𝐾↑𝑎) = (𝐾↑0)) | 
| 234 | 232, 233 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 0 → (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) = (((𝐴 Xrm 0) − ((𝐴 − 𝐾) · (𝐴 Yrm 0))) − (𝐾↑0))) | 
| 235 | 234 | breq2d 5154 | . . . . 5
⊢ (𝑎 = 0 → (((((2 ·
𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) ↔ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) − (𝐾↑0)))) | 
| 236 | 235 | imbi2d 340 | . . . 4
⊢ (𝑎 = 0 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 0) −
((𝐴 − 𝐾) · (𝐴 Yrm 0))) − (𝐾↑0))))) | 
| 237 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑎 = 1 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 1)) | 
| 238 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑎 = 1 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 1)) | 
| 239 | 238 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = 1 → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎)) = ((𝐴 − 𝐾) · (𝐴 Yrm 1))) | 
| 240 | 237, 239 | oveq12d 7450 | . . . . . . 7
⊢ (𝑎 = 1 → ((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) = ((𝐴 Xrm 1) − ((𝐴 − 𝐾) · (𝐴 Yrm 1)))) | 
| 241 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 1 → (𝐾↑𝑎) = (𝐾↑1)) | 
| 242 | 240, 241 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 1 → (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) = (((𝐴 Xrm 1) − ((𝐴 − 𝐾) · (𝐴 Yrm 1))) − (𝐾↑1))) | 
| 243 | 242 | breq2d 5154 | . . . . 5
⊢ (𝑎 = 1 → (((((2 ·
𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) ↔ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) − (𝐾↑1)))) | 
| 244 | 243 | imbi2d 340 | . . . 4
⊢ (𝑎 = 1 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 1) −
((𝐴 − 𝐾) · (𝐴 Yrm 1))) − (𝐾↑1))))) | 
| 245 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑎 = (𝑏 − 1) → (𝐴 Xrm 𝑎) = (𝐴 Xrm (𝑏 − 1))) | 
| 246 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑎 = (𝑏 − 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 − 1))) | 
| 247 | 246 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎)) = ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) | 
| 248 | 245, 247 | oveq12d 7450 | . . . . . . 7
⊢ (𝑎 = (𝑏 − 1) → ((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) = ((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1))))) | 
| 249 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = (𝑏 − 1) → (𝐾↑𝑎) = (𝐾↑(𝑏 − 1))) | 
| 250 | 248, 249 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = (𝑏 − 1) → (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) = (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1)))) | 
| 251 | 250 | breq2d 5154 | . . . . 5
⊢ (𝑎 = (𝑏 − 1) → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) ↔ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1))))) | 
| 252 | 251 | imbi2d 340 | . . . 4
⊢ (𝑎 = (𝑏 − 1) → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 − 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 − 1)))) − (𝐾↑(𝑏 − 1)))))) | 
| 253 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑎 = 𝑏 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 𝑏)) | 
| 254 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑏)) | 
| 255 | 254 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎)) = ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) | 
| 256 | 253, 255 | oveq12d 7450 | . . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) = ((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏)))) | 
| 257 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 𝑏 → (𝐾↑𝑎) = (𝐾↑𝑏)) | 
| 258 | 256, 257 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 𝑏 → (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) = (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))) | 
| 259 | 258 | breq2d 5154 | . . . . 5
⊢ (𝑎 = 𝑏 → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) ↔ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏)))) | 
| 260 | 259 | imbi2d 340 | . . . 4
⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑏) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑏))) − (𝐾↑𝑏))))) | 
| 261 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Xrm 𝑎) = (𝐴 Xrm (𝑏 + 1))) | 
| 262 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm 𝑎) = (𝐴 Yrm (𝑏 + 1))) | 
| 263 | 262 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎)) = ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) | 
| 264 | 261, 263 | oveq12d 7450 | . . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) = ((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1))))) | 
| 265 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → (𝐾↑𝑎) = (𝐾↑(𝑏 + 1))) | 
| 266 | 264, 265 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) = (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1)))) | 
| 267 | 266 | breq2d 5154 | . . . . 5
⊢ (𝑎 = (𝑏 + 1) → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) ↔ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1))))) | 
| 268 | 267 | imbi2d 340 | . . . 4
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm (𝑏 + 1)) − ((𝐴 − 𝐾) · (𝐴 Yrm (𝑏 + 1)))) − (𝐾↑(𝑏 + 1)))))) | 
| 269 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑎 = 𝑁 → (𝐴 Xrm 𝑎) = (𝐴 Xrm 𝑁)) | 
| 270 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑎 = 𝑁 → (𝐴 Yrm 𝑎) = (𝐴 Yrm 𝑁)) | 
| 271 | 270 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑎 = 𝑁 → ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎)) = ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) | 
| 272 | 269, 271 | oveq12d 7450 | . . . . . . 7
⊢ (𝑎 = 𝑁 → ((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) = ((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁)))) | 
| 273 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑎 = 𝑁 → (𝐾↑𝑎) = (𝐾↑𝑁)) | 
| 274 | 272, 273 | oveq12d 7450 | . . . . . 6
⊢ (𝑎 = 𝑁 → (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) = (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁))) | 
| 275 | 274 | breq2d 5154 | . . . . 5
⊢ (𝑎 = 𝑁 → (((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎)) ↔ ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁)))) | 
| 276 | 275 | imbi2d 340 | . . . 4
⊢ (𝑎 = 𝑁 → (((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑎) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑎))) − (𝐾↑𝑎))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁))))) | 
| 277 | 34, 50, 228, 236, 244, 252, 260, 268, 276 | 2nn0ind 42962 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) → ((((2
· 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁)))) | 
| 278 | 277 | impcom 407 | . 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0)
→ ((((2 · 𝐴)
· 𝐾) − (𝐾↑2)) − 1) ∥
(((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁))) | 
| 279 | 278 | 3impa 1109 | 1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((((2 · 𝐴)
· 𝐾) − (𝐾↑2)) − 1) ∥
(((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁))) |