Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.25 Structured version   Visualization version   GIF version

Theorem jm2.25 37067
Description: Lemma for jm2.26 37070. Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014.)
Assertion
Ref Expression
jm2.25 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))

Proof of Theorem jm2.25
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 793 . . . . . . . . 9 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐴 ∈ (ℤ‘2))
2 simprrr 804 . . . . . . . . 9 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑁 ∈ ℤ)
3 frmx 36979 . . . . . . . . . . 11 Xrm :((ℤ‘2) × ℤ)⟶ℕ0
43fovcl 6721 . . . . . . . . . 10 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
54nn0zd 11427 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℤ)
61, 2, 5syl2anc 692 . . . . . . . 8 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℤ)
7 simprrl 803 . . . . . . . . 9 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℤ)
8 frmy 36980 . . . . . . . . . 10 Yrm :((ℤ‘2) × ℤ)⟶ℤ
98fovcl 6721 . . . . . . . . 9 ((𝐴 ∈ (ℤ‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
101, 7, 9syl2anc 692 . . . . . . . 8 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑀) ∈ ℤ)
11 congid 37039 . . . . . . . 8 (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀)))
126, 10, 11syl2anc 692 . . . . . . 7 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀)))
13 2cnd 11040 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℤ → 2 ∈ ℂ)
14 zcn 11329 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
1513, 14mulcld 10007 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (2 · 𝑁) ∈ ℂ)
1615mul02d 10181 . . . . . . . . . . . . 13 (𝑁 ∈ ℤ → (0 · (2 · 𝑁)) = 0)
1716adantl 482 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 · (2 · 𝑁)) = 0)
1817oveq2d 6623 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + (0 · (2 · 𝑁))) = (𝑀 + 0))
19 zcn 11329 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
2019addid1d 10183 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → (𝑀 + 0) = 𝑀)
2120adantr 481 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 0) = 𝑀)
2218, 21eqtrd 2655 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + (0 · (2 · 𝑁))) = 𝑀)
2322ad2antll 764 . . . . . . . . 9 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + (0 · (2 · 𝑁))) = 𝑀)
2423oveq2d 6623 . . . . . . . 8 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) = (𝐴 Yrm 𝑀))
2524oveq1d 6622 . . . . . . 7 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑀)))
2612, 25breqtrrd 4643 . . . . . 6 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))
2726orcd 407 . . . . 5 ((𝐼 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
2827ex 450 . . . 4 (𝐼 ∈ ℤ → ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
29 simprl 793 . . . . . . . 8 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝐴 ∈ (ℤ‘2))
30 simprrr 804 . . . . . . . 8 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑁 ∈ ℤ)
3129, 30, 5syl2anc 692 . . . . . . 7 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℤ)
32 simprrl 803 . . . . . . . 8 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℤ)
3329, 32, 9syl2anc 692 . . . . . . 7 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑀) ∈ ℤ)
34 simpl 473 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑏 ∈ ℤ)
3534peano2zd 11432 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 + 1) ∈ ℤ)
36 eluzel2 11639 . . . . . . . . . . . 12 (𝐴 ∈ (ℤ‘2) → 2 ∈ ℤ)
3736ad2antrl 763 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 2 ∈ ℤ)
3837, 30zmulcld 11435 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · 𝑁) ∈ ℤ)
3935, 38zmulcld 11435 . . . . . . . . 9 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑏 + 1) · (2 · 𝑁)) ∈ ℤ)
4032, 39zaddcld 11433 . . . . . . . 8 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) ∈ ℤ)
418fovcl 6721 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) ∈ ℤ) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ)
4229, 40, 41syl2anc 692 . . . . . . 7 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) ∈ ℤ)
4334, 38zmulcld 11435 . . . . . . . . 9 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 · (2 · 𝑁)) ∈ ℤ)
4432, 43zaddcld 11433 . . . . . . . 8 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ)
458fovcl 6721 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ)
4629, 44, 45syl2anc 692 . . . . . . 7 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ)
473fovcl 6721 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) ∈ ℕ0)
4847nn0zd 11427 . . . . . . . . . . . . 13 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) ∈ ℤ)
4929, 38, 48syl2anc 692 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) ∈ ℤ)
5046, 49zmulcld 11435 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) ∈ ℤ)
5146znegcld 11431 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ)
5250, 51zsubcld 11434 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ)
533fovcl 6721 . . . . . . . . . . . . 13 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℕ0)
5453nn0zd 11427 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ)
5529, 44, 54syl2anc 692 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ)
568fovcl 6721 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) ∈ ℤ)
5729, 38, 56syl2anc 692 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) ∈ ℤ)
5855, 57zmulcld 11435 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈ ℤ)
5937, 31zmulcld 11435 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · (𝐴 Xrm 𝑁)) ∈ ℤ)
60 dvdsmul2 14931 . . . . . . . . . . . . . 14 (((2 · (𝐴 Xrm 𝑁)) ∈ ℤ ∧ (𝐴 Xrm 𝑁) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)))
6159, 31, 60syl2anc 692 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)))
62 rmxdbl 37005 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) − 1))
6329, 30, 62syl2anc 692 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) − 1))
6463oveq1d 6622 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 · 𝑁)) + 1) = (((2 · ((𝐴 Xrm 𝑁)↑2)) − 1) + 1))
65 2cnd 11040 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 2 ∈ ℂ)
6629, 30, 4syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℕ0)
6766nn0cnd 11300 . . . . . . . . . . . . . . . . 17 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∈ ℂ)
6867sqcld 12949 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁)↑2) ∈ ℂ)
6965, 68mulcld 10007 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · ((𝐴 Xrm 𝑁)↑2)) ∈ ℂ)
70 1cnd 10003 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 1 ∈ ℂ)
7169, 70npcand 10343 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((2 · ((𝐴 Xrm 𝑁)↑2)) − 1) + 1) = (2 · ((𝐴 Xrm 𝑁)↑2)))
7267sqvald 12948 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁)↑2) = ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁)))
7372oveq2d 6623 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · ((𝐴 Xrm 𝑁)↑2)) = (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))))
74 mulass 9971 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ (𝐴 Xrm 𝑁) ∈ ℂ ∧ (𝐴 Xrm 𝑁) ∈ ℂ) → ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)) = (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))))
7574eqcomd 2627 . . . . . . . . . . . . . . . 16 ((2 ∈ ℂ ∧ (𝐴 Xrm 𝑁) ∈ ℂ ∧ (𝐴 Xrm 𝑁) ∈ ℂ) → (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)))
7665, 67, 67, 75syl3anc 1323 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · ((𝐴 Xrm 𝑁) · (𝐴 Xrm 𝑁))) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)))
7773, 76eqtrd 2655 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · ((𝐴 Xrm 𝑁)↑2)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)))
7864, 71, 773eqtrd 2659 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 · 𝑁)) + 1) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Xrm 𝑁)))
7961, 78breqtrrd 4643 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1))
8049peano2zd 11432 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (2 · 𝑁)) + 1) ∈ ℤ)
81 dvdsmultr2 14948 . . . . . . . . . . . . 13 (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ ∧ ((𝐴 Xrm (2 · 𝑁)) + 1) ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1))))
8231, 46, 80, 81syl3anc 1323 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (2 · 𝑁)) + 1) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1))))
8379, 82mpd 15 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)))
8446zcnd 11430 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℂ)
8584mulid1d 10004 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1) = (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))
8685oveq2d 6623 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))
8749zcnd 11430 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm (2 · 𝑁)) ∈ ℂ)
8884, 87, 70adddid 10011 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · 1)))
8950zcnd 11430 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) ∈ ℂ)
9089, 84subnegd 10346 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))
9186, 88, 903eqtr4d 2665 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · ((𝐴 Xrm (2 · 𝑁)) + 1)) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))
9283, 91breqtrd 4641 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))
938fovcl 6721 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ)
9429, 30, 93syl2anc 692 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑁) ∈ ℤ)
9537, 94zmulcld 11435 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · (𝐴 Yrm 𝑁)) ∈ ℤ)
96 dvdsmul2 14931 . . . . . . . . . . . . 13 (((2 · (𝐴 Yrm 𝑁)) ∈ ℤ ∧ (𝐴 Xrm 𝑁) ∈ ℤ) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁)))
9795, 31, 96syl2anc 692 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁)))
98 rmydbl 37006 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁)))
9929, 30, 98syl2anc 692 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁)))
10094zcnd 11430 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm 𝑁) ∈ ℂ)
10165, 67, 100mul32d 10193 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁)) = ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁)))
10299, 101eqtrd 2655 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Yrm 𝑁)) · (𝐴 Xrm 𝑁)))
10397, 102breqtrrd 4643 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)))
104 dvdsmultr2 14948 . . . . . . . . . . . 12 (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℤ ∧ (𝐴 Yrm (2 · 𝑁)) ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
10531, 55, 57, 104syl3anc 1323 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ (𝐴 Yrm (2 · 𝑁)) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
106103, 105mpd 15 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))
107 dvds2add 14942 . . . . . . . . . . 11 (((𝐴 Xrm 𝑁) ∈ ℤ ∧ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ ∧ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈ ℤ) → (((𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∧ (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))))
108107imp 445 . . . . . . . . . 10 ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∈ ℤ ∧ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈ ℤ) ∧ ((𝐴 Xrm 𝑁) ∥ (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∧ (𝐴 Xrm 𝑁) ∥ ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
10931, 52, 58, 92, 106, 108syl32anc 1331 . . . . . . . . 9 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
11034zcnd 11430 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑏 ∈ ℂ)
11138zcnd 11430 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (2 · 𝑁) ∈ ℂ)
112110, 70, 111adddird 10012 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑏 + 1) · (2 · 𝑁)) = ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁))))
113112oveq2d 6623 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) = (𝑀 + ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁)))))
11432zcnd 11430 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 𝑀 ∈ ℂ)
11543zcnd 11430 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑏 · (2 · 𝑁)) ∈ ℂ)
116 1zzd 11355 . . . . . . . . . . . . . . . . 17 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → 1 ∈ ℤ)
117116, 38zmulcld 11435 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2 · 𝑁)) ∈ ℤ)
118117zcnd 11430 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2 · 𝑁)) ∈ ℂ)
119114, 115, 118addassd 10009 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑀 + (𝑏 · (2 · 𝑁))) + (1 · (2 · 𝑁))) = (𝑀 + ((𝑏 · (2 · 𝑁)) + (1 · (2 · 𝑁)))))
120111mulid2d 10005 . . . . . . . . . . . . . . 15 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (1 · (2 · 𝑁)) = (2 · 𝑁))
121120oveq2d 6623 . . . . . . . . . . . . . 14 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝑀 + (𝑏 · (2 · 𝑁))) + (1 · (2 · 𝑁))) = ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁)))
122113, 119, 1213eqtr2d 2661 . . . . . . . . . . . . 13 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝑀 + ((𝑏 + 1) · (2 · 𝑁))) = ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁)))
123122oveq2d 6623 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) = (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))))
124 rmyadd 36997 . . . . . . . . . . . . 13 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 + (𝑏 · (2 · 𝑁))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) → (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
12529, 44, 38, 124syl3anc 1323 . . . . . . . . . . . 12 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm ((𝑀 + (𝑏 · (2 · 𝑁))) + (2 · 𝑁))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
126123, 125eqtrd 2655 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) = (((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
127126oveq1d 6622 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))
12858zcnd 11430 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁))) ∈ ℂ)
12951zcnd 11430 . . . . . . . . . . 11 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) ∈ ℂ)
13089, 128, 129addsubd 10360 . . . . . . . . . 10 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
131127, 130eqtrd 2655 . . . . . . . . 9 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) = ((((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Xrm (2 · 𝑁))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) + ((𝐴 Xrm (𝑀 + (𝑏 · (2 · 𝑁)))) · (𝐴 Yrm (2 · 𝑁)))))
132109, 131breqtrrd 4643 . . . . . . . 8 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))))
133132olcd 408 . . . . . . 7 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁))))) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))))
134 jm2.25lem1 37066 . . . . . . 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 𝑀)))))
13531, 33, 42, 46, 133, 134syl221anc 1334 . . . . . 6 ((𝑏 ∈ ℤ ∧ (𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
136135pm5.74da 722 . . . . 5 (𝑏 ∈ ℤ → (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))))
137 oveq1 6614 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎 · (2 · 𝑁)) = (𝑏 · (2 · 𝑁)))
138137oveq2d 6623 . . . . . . . . . 10 (𝑎 = 𝑏 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝑏 · (2 · 𝑁))))
139138oveq2d 6623 . . . . . . . . 9 (𝑎 = 𝑏 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))))
140139oveq1d 6622 . . . . . . . 8 (𝑎 = 𝑏 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))
141140breq2d 4627 . . . . . . 7 (𝑎 = 𝑏 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))))
142139oveq1d 6622 . . . . . . . 8 (𝑎 = 𝑏 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))
143142breq2d 4627 . . . . . . 7 (𝑎 = 𝑏 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
144141, 143orbi12d 745 . . . . . 6 (𝑎 = 𝑏 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
145144imbi2d 330 . . . . 5 (𝑎 = 𝑏 → (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑏 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))))
146 oveq1 6614 . . . . . . . . . . 11 (𝑎 = (𝑏 + 1) → (𝑎 · (2 · 𝑁)) = ((𝑏 + 1) · (2 · 𝑁)))
147146oveq2d 6623 . . . . . . . . . 10 (𝑎 = (𝑏 + 1) → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + ((𝑏 + 1) · (2 · 𝑁))))
148147oveq2d 6623 . . . . . . . . 9 (𝑎 = (𝑏 + 1) → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))))
149148oveq1d 6622 . . . . . . . 8 (𝑎 = (𝑏 + 1) → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))
150149breq2d 4627 . . . . . . 7 (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))))
151148oveq1d 6622 . . . . . . . 8 (𝑎 = (𝑏 + 1) → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))
152151breq2d 4627 . . . . . . 7 (𝑎 = (𝑏 + 1) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
153150, 152orbi12d 745 . . . . . 6 (𝑎 = (𝑏 + 1) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
154153imbi2d 330 . . . . 5 (𝑎 = (𝑏 + 1) → (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + ((𝑏 + 1) · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))))
155 oveq1 6614 . . . . . . . . . . 11 (𝑎 = 0 → (𝑎 · (2 · 𝑁)) = (0 · (2 · 𝑁)))
156155oveq2d 6623 . . . . . . . . . 10 (𝑎 = 0 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (0 · (2 · 𝑁))))
157156oveq2d 6623 . . . . . . . . 9 (𝑎 = 0 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))))
158157oveq1d 6622 . . . . . . . 8 (𝑎 = 0 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))
159158breq2d 4627 . . . . . . 7 (𝑎 = 0 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))))
160157oveq1d 6622 . . . . . . . 8 (𝑎 = 0 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))
161160breq2d 4627 . . . . . . 7 (𝑎 = 0 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
162159, 161orbi12d 745 . . . . . 6 (𝑎 = 0 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
163162imbi2d 330 . . . . 5 (𝑎 = 0 → (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))))
164 oveq1 6614 . . . . . . . . . . 11 (𝑎 = 𝐼 → (𝑎 · (2 · 𝑁)) = (𝐼 · (2 · 𝑁)))
165164oveq2d 6623 . . . . . . . . . 10 (𝑎 = 𝐼 → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝐼 · (2 · 𝑁))))
166165oveq2d 6623 . . . . . . . . 9 (𝑎 = 𝐼 → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))))
167166oveq1d 6622 . . . . . . . 8 (𝑎 = 𝐼 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)))
168167breq2d 4627 . . . . . . 7 (𝑎 = 𝐼 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀))))
169166oveq1d 6622 . . . . . . . 8 (𝑎 = 𝐼 → ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) = ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))
170169breq2d 4627 . . . . . . 7 (𝑎 = 𝐼 → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)) ↔ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
171168, 170orbi12d 745 . . . . . 6 (𝑎 = 𝐼 → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
172171imbi2d 330 . . . . 5 (𝑎 = 𝐼 → (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))))
173136, 145, 154, 163, 172zindbi 37012 . . . 4 (𝐼 ∈ ℤ → (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (0 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) ↔ ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))))
17428, 173mpbid 222 . . 3 (𝐼 ∈ ℤ → ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))))
175174impcom 446 . 2 (((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
1761753impa 1256 1 ((𝐴 ∈ (ℤ‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987   class class class wbr 4615  cfv 5849  (class class class)co 6607  cc 9881  0cc0 9883  1c1 9884   + caddc 9886   · cmul 9888  cmin 10213  -cneg 10214  2c2 11017  0cn0 11239  cz 11324  cuz 11634  cexp 12803  cdvds 14910   Xrm crmx 36965   Yrm crmy 36966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961  ax-addf 9962  ax-mulf 9963
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-of 6853  df-om 7016  df-1st 7116  df-2nd 7117  df-supp 7244  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-omul 7513  df-er 7690  df-map 7807  df-pm 7808  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fsupp 8223  df-fi 8264  df-sup 8295  df-inf 8296  df-oi 8362  df-card 8712  df-acn 8715  df-cda 8937  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-xnn0 11311  df-z 11325  df-dec 11441  df-uz 11635  df-q 11736  df-rp 11780  df-xneg 11893  df-xadd 11894  df-xmul 11895  df-ioo 12124  df-ioc 12125  df-ico 12126  df-icc 12127  df-fz 12272  df-fzo 12410  df-fl 12536  df-mod 12612  df-seq 12745  df-exp 12804  df-fac 13004  df-bc 13033  df-hash 13061  df-shft 13744  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-limsup 14139  df-clim 14156  df-rlim 14157  df-sum 14354  df-ef 14726  df-sin 14728  df-cos 14729  df-pi 14731  df-dvds 14911  df-gcd 15144  df-numer 15370  df-denom 15371  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-mulr 15879  df-starv 15880  df-sca 15881  df-vsca 15882  df-ip 15883  df-tset 15884  df-ple 15885  df-ds 15888  df-unif 15889  df-hom 15890  df-cco 15891  df-rest 16007  df-topn 16008  df-0g 16026  df-gsum 16027  df-topgen 16028  df-pt 16029  df-prds 16032  df-xrs 16086  df-qtop 16091  df-imas 16092  df-xps 16094  df-mre 16170  df-mrc 16171  df-acs 16173  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-submnd 17260  df-mulg 17465  df-cntz 17674  df-cmn 18119  df-psmet 19660  df-xmet 19661  df-met 19662  df-bl 19663  df-mopn 19664  df-fbas 19665  df-fg 19666  df-cnfld 19669  df-top 20621  df-topon 20638  df-topsp 20651  df-bases 20664  df-cld 20736  df-ntr 20737  df-cls 20738  df-nei 20815  df-lp 20853  df-perf 20854  df-cn 20944  df-cnp 20945  df-haus 21032  df-tx 21278  df-hmeo 21471  df-fil 21563  df-fm 21655  df-flim 21656  df-flf 21657  df-xms 22038  df-ms 22039  df-tms 22040  df-cncf 22594  df-limc 23543  df-dv 23544  df-log 24214  df-squarenn 36906  df-pell1qr 36907  df-pell14qr 36908  df-pell1234qr 36909  df-pellfund 36910  df-rmx 36967  df-rmy 36968
This theorem is referenced by:  jm2.26a  37068
  Copyright terms: Public domain W3C validator