| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simprl 771 | . . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐴 ∈
(ℤ≥‘2)) | 
| 2 |  | simprrr 782 | . . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑁 ∈ ℤ) | 
| 3 |  | frmx 42925 | . . . . . . . . . . 11
⊢ 
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 | 
| 4 | 3 | fovcl 7561 | . . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈
ℕ0) | 
| 5 | 4 | nn0zd 12639 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℤ) | 
| 6 | 1, 2, 5 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℤ) | 
| 7 |  | simprrl 781 | . . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℤ) | 
| 8 |  | frmy 42926 | . . . . . . . . . 10
⊢ 
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ | 
| 9 | 8 | fovcl 7561 | . . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ) | 
| 10 | 1, 7, 9 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑀) ∈ ℤ) | 
| 11 |  | congid 42983 | . . . . . . . 8
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀))) | 
| 12 | 6, 10, 11 | syl2anc 584 | . . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀))) | 
| 13 |  | 2cnd 12344 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 2 ∈
ℂ) | 
| 14 |  | zcn 12618 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 15 | 13, 14 | mulcld 11281 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (2
· 𝑁) ∈
ℂ) | 
| 16 | 15 | mul02d 11459 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (0
· (2 · 𝑁)) =
0) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0
· (2 · 𝑁)) =
0) | 
| 18 | 17 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + (0 · (2 · 𝑁))) = (𝑀 + 0)) | 
| 19 |  | zcn 12618 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) | 
| 20 | 19 | addridd 11461 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 + 0) = 𝑀) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 0) = 𝑀) | 
| 22 | 18, 21 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + (0 · (2 · 𝑁))) = 𝑀) | 
| 23 | 22 | ad2antll 729 | . . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + (0 · (2 · 𝑁))) = 𝑀) | 
| 24 | 23 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) = (𝐴 Yrm 𝑀)) | 
| 25 | 24 | oveq1d 7446 | . . . . . . 7
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀))) | 
| 26 | 12, 25 | breqtrrd 5171 | . . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) | 
| 27 | 26 | orcd 874 | . . . . 5
⊢ ((𝐼 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | 
| 28 | 27 | ex 412 | . . . 4
⊢ (𝐼 ∈ ℤ → ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 29 |  | simprl 771 | . . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐴 ∈
(ℤ≥‘2)) | 
| 30 |  | simprrr 782 | . . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑁 ∈ ℤ) | 
| 31 | 29, 30, 5 | syl2anc 584 | . . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℤ) | 
| 32 |  | simprrl 781 | . . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℤ) | 
| 33 | 29, 32, 9 | syl2anc 584 | . . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑀) ∈ ℤ) | 
| 34 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑏 ∈ ℤ) | 
| 35 | 34 | peano2zd 12725 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 + 1) ∈
ℤ) | 
| 36 |  | eluzel2 12883 | . . . . . . . . . . . 12
⊢ (𝐴 ∈
(ℤ≥‘2) → 2 ∈ ℤ) | 
| 37 | 36 | ad2antrl 728 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 2 ∈
ℤ) | 
| 38 | 37, 30 | zmulcld 12728 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · 𝑁) ∈
ℤ) | 
| 39 | 35, 38 | zmulcld 12728 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑏 + 1) · (2 · 𝑁)) ∈
ℤ) | 
| 40 | 32, 39 | zaddcld 12726 | . . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) ∈ ℤ) | 
| 41 | 8 | fovcl 7561 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) ∈ ℤ) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ) | 
| 42 | 29, 40, 41 | syl2anc 584 | . . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ) | 
| 43 | 34, 38 | zmulcld 12728 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 · (2 · 𝑁)) ∈
ℤ) | 
| 44 | 32, 43 | zaddcld 12726 | . . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) | 
| 45 | 8 | fovcl 7561 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) | 
| 46 | 29, 44, 45 | syl2anc 584 | . . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) | 
| 47 | 3 | fovcl 7561 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) ∈
ℕ0) | 
| 48 | 47 | nn0zd 12639 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) ∈
ℤ) | 
| 49 | 29, 38, 48 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) ∈
ℤ) | 
| 50 | 46, 49 | zmulcld 12728 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) ∈
ℤ) | 
| 51 | 46 | znegcld 12724 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) | 
| 52 | 50, 51 | zsubcld 12727 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ) | 
| 53 | 3 | fovcl 7561 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈
ℕ0) | 
| 54 | 53 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) | 
| 55 | 29, 44, 54 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) | 
| 56 | 8 | fovcl 7561 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) ∈
ℤ) | 
| 57 | 29, 38, 56 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) ∈
ℤ) | 
| 58 | 55, 57 | zmulcld 12728 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈
ℤ) | 
| 59 | 37, 31 | zmulcld 12728 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · (𝐴 Xrm 𝑁)) ∈
ℤ) | 
| 60 |  | dvdsmul2 16316 | . . . . . . . . . . . . . 14
⊢ (((2
· (𝐴 Xrm
𝑁)) ∈ ℤ ∧
(𝐴 Xrm 𝑁) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 61 | 59, 31, 60 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 62 |  | rmxdbl 42951 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) −
1)) | 
| 63 | 29, 30, 62 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) −
1)) | 
| 64 | 63 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 ·
𝑁)) + 1) = (((2 ·
((𝐴 Xrm 𝑁)↑2)) − 1) +
1)) | 
| 65 |  | 2cnd 12344 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 2 ∈
ℂ) | 
| 66 | 29, 30, 4 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈
ℕ0) | 
| 67 | 66 | nn0cnd 12589 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℂ) | 
| 68 | 67 | sqcld 14184 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁)↑2) ∈
ℂ) | 
| 69 | 65, 68 | mulcld 11281 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁)↑2)) ∈
ℂ) | 
| 70 |  | 1cnd 11256 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 1 ∈
ℂ) | 
| 71 | 69, 70 | npcand 11624 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((2 ·
((𝐴 Xrm 𝑁)↑2)) − 1) + 1) = (2
· ((𝐴 Xrm
𝑁)↑2))) | 
| 72 | 67 | sqvald 14183 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁)↑2) = ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) | 
| 73 | 72 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁)↑2)) = (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁)))) | 
| 74 |  | mulass 11243 | . . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ) → ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)) = (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁)))) | 
| 75 | 74 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ ∧ (𝐴
Xrm 𝑁) ∈
ℂ) → (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 76 | 65, 67, 67, 75 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 77 | 73, 76 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 ·
((𝐴 Xrm 𝑁)↑2)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 78 | 64, 71, 77 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 ·
𝑁)) + 1) = ((2 ·
(𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 79 | 61, 78 | breqtrrd 5171 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1)) | 
| 80 | 49 | peano2zd 12725 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 ·
𝑁)) + 1) ∈
ℤ) | 
| 81 |  | dvdsmultr2 16335 | . . . . . . . . . . . . 13
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ ∧ ((𝐴 Xrm (2 ·
𝑁)) + 1) ∈ ℤ)
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Xrm (2 ·
𝑁)) + 1) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)))) | 
| 82 | 31, 46, 80, 81 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)))) | 
| 83 | 79, 82 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1))) | 
| 84 | 46 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℂ) | 
| 85 | 84 | mulridd 11278 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1) = (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) | 
| 86 | 85 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) | 
| 87 | 49 | zcnd 12723 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) ∈
ℂ) | 
| 88 | 84, 87, 70 | adddid 11285 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1))) | 
| 89 | 50 | zcnd 12723 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) ∈
ℂ) | 
| 90 | 89, 84 | subnegd 11627 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) | 
| 91 | 86, 88, 90 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) | 
| 92 | 83, 91 | breqtrd 5169 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) | 
| 93 | 8 | fovcl 7561 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ) | 
| 94 | 29, 30, 93 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑁) ∈ ℤ) | 
| 95 | 37, 94 | zmulcld 12728 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · (𝐴 Yrm 𝑁)) ∈
ℤ) | 
| 96 |  | dvdsmul2 16316 | . . . . . . . . . . . . 13
⊢ (((2
· (𝐴 Yrm
𝑁)) ∈ ℤ ∧
(𝐴 Xrm 𝑁) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 97 | 95, 31, 96 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 98 |  | rmydbl 42952 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁))) | 
| 99 | 29, 30, 98 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁))) | 
| 100 | 94 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑁) ∈ ℂ) | 
| 101 | 65, 67, 100 | mul32d 11471 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((2 ·
(𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁)) = ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 102 | 99, 101 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁))) | 
| 103 | 97, 102 | breqtrrd 5171 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁))) | 
| 104 |  | dvdsmultr2 16335 | . . . . . . . . . . . 12
⊢ (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ ∧ (𝐴 Yrm (2 · 𝑁)) ∈ ℤ) →
((𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 105 | 31, 55, 57, 104 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 106 | 103, 105 | mpd 15 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) | 
| 107 | 31, 52, 58, 92, 106 | dvds2addd 16329 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 108 | 34 | zcnd 12723 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑏 ∈ ℂ) | 
| 109 | 38 | zcnd 12723 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · 𝑁) ∈
ℂ) | 
| 110 | 108, 70, 109 | adddird 11286 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑏 + 1) · (2 · 𝑁)) = ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁)))) | 
| 111 | 110 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) = (𝑀 + ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁))))) | 
| 112 | 32 | zcnd 12723 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℂ) | 
| 113 | 43 | zcnd 12723 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 · (2 · 𝑁)) ∈
ℂ) | 
| 114 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 1 ∈
ℤ) | 
| 115 | 114, 38 | zmulcld 12728 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2
· 𝑁)) ∈
ℤ) | 
| 116 | 115 | zcnd 12723 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2
· 𝑁)) ∈
ℂ) | 
| 117 | 112, 113,
116 | addassd 11283 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑀 + (𝑏 · (2 · 𝑁))) + (1 · (2 · 𝑁))) = (𝑀 + ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁))))) | 
| 118 | 109 | mullidd 11279 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2
· 𝑁)) = (2 ·
𝑁)) | 
| 119 | 118 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑀 + (𝑏 · (2 · 𝑁))) + (1 · (2 · 𝑁))) = ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) | 
| 120 | 111, 117,
119 | 3eqtr2d 2783 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) = ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) | 
| 121 | 120 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) = (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁)))) | 
| 122 |  | rmyadd 42943 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 123 | 29, 44, 38, 122 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 124 | 121, 123 | eqtrd 2777 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 125 | 124 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) | 
| 126 | 58 | zcnd 12723 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈
ℂ) | 
| 127 | 51 | zcnd 12723 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℂ) | 
| 128 | 89, 126, 127 | addsubd 11641 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 129 | 125, 128 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) | 
| 130 | 107, 129 | breqtrrd 5171 | . . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))) | 
| 131 | 130 | olcd 875 | . . . . . . 7
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))) | 
| 132 |  | jm2.25lem1 43010 | . . . . . . 7
⊢ ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) ∧ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ ∧ (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 133 | 31, 33, 42, 46, 131, 132 | syl221anc 1383 | . . . . . 6
⊢ ((𝑏 ∈ ℤ ∧ (𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 134 | 133 | pm5.74da 804 | . . . . 5
⊢ (𝑏 ∈ ℤ → (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) | 
| 135 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑎 · (2 · 𝑁)) = (𝑏 · (2 · 𝑁))) | 
| 136 | 135 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝑏 · (2 · 𝑁)))) | 
| 137 | 136 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) | 
| 138 | 137 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) | 
| 139 | 138 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) | 
| 140 | 137 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) | 
| 141 | 140 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = 𝑏 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | 
| 142 | 139, 141 | orbi12d 919 | . . . . . 6
⊢ (𝑎 = 𝑏 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 143 | 142 | imbi2d 340 | . . . . 5
⊢ (𝑎 = 𝑏 → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) | 
| 144 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑎 = (𝑏 + 1) → (𝑎 · (2 · 𝑁)) = ((𝑏 + 1) · (2 · 𝑁))) | 
| 145 | 144 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑎 = (𝑏 + 1) → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) | 
| 146 | 145 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁))))) | 
| 147 | 146 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) | 
| 148 | 147 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) | 
| 149 | 146 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) | 
| 150 | 149 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | 
| 151 | 148, 150 | orbi12d 919 | . . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 152 | 151 | imbi2d 340 | . . . . 5
⊢ (𝑎 = (𝑏 + 1) → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) | 
| 153 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑎 = 0 → (𝑎 · (2 · 𝑁)) = (0 · (2 · 𝑁))) | 
| 154 | 153 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑎 = 0 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (0 · (2 · 𝑁)))) | 
| 155 | 154 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑎 = 0 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (0 · (2 · 𝑁))))) | 
| 156 | 155 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = 0 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) | 
| 157 | 156 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = 0 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) | 
| 158 | 155 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = 0 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) | 
| 159 | 158 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = 0 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | 
| 160 | 157, 159 | orbi12d 919 | . . . . . 6
⊢ (𝑎 = 0 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 161 | 160 | imbi2d 340 | . . . . 5
⊢ (𝑎 = 0 → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) | 
| 162 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑎 = 𝐼 → (𝑎 · (2 · 𝑁)) = (𝐼 · (2 · 𝑁))) | 
| 163 | 162 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑎 = 𝐼 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝐼 · (2 · 𝑁)))) | 
| 164 | 163 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑎 = 𝐼 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁))))) | 
| 165 | 164 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = 𝐼 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))) | 
| 166 | 165 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = 𝐼 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))) | 
| 167 | 164 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑎 = 𝐼 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) | 
| 168 | 167 | breq2d 5155 | . . . . . . 7
⊢ (𝑎 = 𝐼 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | 
| 169 | 166, 168 | orbi12d 919 | . . . . . 6
⊢ (𝑎 = 𝐼 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 170 | 169 | imbi2d 340 | . . . . 5
⊢ (𝑎 = 𝐼 → (((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) | 
| 171 | 134, 143,
152, 161, 170 | zindbi 42958 | . . . 4
⊢ (𝐼 ∈ ℤ → (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ≥‘2)
∧ (𝑀 ∈ ℤ
∧ 𝑁 ∈ ℤ))
→ ((𝐴 Xrm
𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))) | 
| 172 | 28, 171 | mpbid 232 | . . 3
⊢ (𝐼 ∈ ℤ → ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))) | 
| 173 | 172 | impcom 407 | . 2
⊢ (((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | 
| 174 | 173 | 3impa 1110 | 1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) |