jm2.25

Description: Lemma for jm2.26 . Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014)

		Ref	Expression
	Assertion	jm2.25	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℤ ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
2		simprrr	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑁 ∈ ℤ )
3		frmx	⊢ X_rm : ( ( ℤ_≥ ‘ 2 ) × ℤ ) ⟶ ℕ₀
4	3	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∈ ℕ₀ )
5	4	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∈ ℤ )
6	1 2 5	syl2anc	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∈ ℤ )
7		simprrl	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑀 ∈ ℤ )
8		frmy	⊢ Y_rm : ( ( ℤ_≥ ‘ 2 ) × ℤ ) ⟶ ℤ
9	8	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Y_rm 𝑀 ) ∈ ℤ )
10	1 7 9	syl2anc	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm 𝑀 ) ∈ ℤ )
11		congid	⊢ ( ( ( 𝐴 X_rm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Y_rm 𝑀 ) ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑀 ) ) )
12	6 10 11	syl2anc	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑀 ) ) )
13		2cnd	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
14		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
15	13 14	mulcld	⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℂ )
16	15	mul02d	⊢ ( 𝑁 ∈ ℤ → ( 0 · ( 2 · 𝑁 ) ) = 0 )
17	16	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 · ( 2 · 𝑁 ) ) = 0 )
18	17	oveq2d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + 0 ) )
19		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
20	19	addid1d	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 0 ) = 𝑀 )
21	20	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 0 ) = 𝑀 )
22	18 21	eqtrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) = 𝑀 )
23	22	ad2antll	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) = 𝑀 )
24	23	oveq2d	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Y_rm 𝑀 ) )
25	24	oveq1d	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑀 ) ) )
26	12 25	breqtrrd	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) )
27	26	orcd	⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
28	27	ex	⊢ ( 𝐼 ∈ ℤ → ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
29		simprl	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
30		simprrr	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑁 ∈ ℤ )
31	29 30 5	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∈ ℤ )
32		simprrl	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑀 ∈ ℤ )
33	29 32 9	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm 𝑀 ) ∈ ℤ )
34		simpl	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑏 ∈ ℤ )
35	34	peano2zd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑏 + 1 ) ∈ ℤ )
36		eluzel2	⊢ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) → 2 ∈ ℤ )
37	36	ad2antrl	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 2 ∈ ℤ )
38	37 30	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · 𝑁 ) ∈ ℤ )
39	35 38	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ∈ ℤ )
40	32 39	zaddcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ∈ ℤ )
41	8	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ∈ ℤ ) → ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
42	29 40 41	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
43	34 38	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑏 · ( 2 · 𝑁 ) ) ∈ ℤ )
44	32 43	zaddcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ∈ ℤ )
45	8	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ∈ ℤ ) → ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
46	29 44 45	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
47	3	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 2 · 𝑁 ) ∈ ℤ ) → ( 𝐴 X_rm ( 2 · 𝑁 ) ) ∈ ℕ₀ )
48	47	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 2 · 𝑁 ) ∈ ℤ ) → ( 𝐴 X_rm ( 2 · 𝑁 ) ) ∈ ℤ )
49	29 38 48	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm ( 2 · 𝑁 ) ) ∈ ℤ )
50	46 49	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) ∈ ℤ )
51	46	znegcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
52	50 51	zsubcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) ∈ ℤ )
53	3	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ∈ ℤ ) → ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℕ₀ )
54	53	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ∈ ℤ ) → ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
55	29 44 54	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ )
56	8	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 2 · 𝑁 ) ∈ ℤ ) → ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ∈ ℤ )
57	29 38 56	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ∈ ℤ )
58	55 57	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ∈ ℤ )
59	37 31	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · ( 𝐴 X_rm 𝑁 ) ) ∈ ℤ )
60		dvdsmul2	⊢ ( ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 X_rm 𝑁 ) ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
61	59 31 60	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
62		rmxdbl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 X_rm ( 2 · 𝑁 ) ) = ( ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) − 1 ) )
63	29 30 62	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm ( 2 · 𝑁 ) ) = ( ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) − 1 ) )
64	63	oveq1d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) = ( ( ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) − 1 ) + 1 ) )
65		2cnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 2 ∈ ℂ )
66	29 30 4	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∈ ℕ₀ )
67	66	nn0cnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∈ ℂ )
68	67	sqcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ∈ ℂ )
69	65 68	mulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) ∈ ℂ )
70		1cnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 1 ∈ ℂ )
71	69 70	npcand	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) − 1 ) + 1 ) = ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) )
72	67	sqvald	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) = ( ( 𝐴 X_rm 𝑁 ) · ( 𝐴 X_rm 𝑁 ) ) )
73	72	oveq2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) = ( 2 · ( ( 𝐴 X_rm 𝑁 ) · ( 𝐴 X_rm 𝑁 ) ) ) )
74		mulass	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐴 X_rm 𝑁 ) ∈ ℂ ∧ ( 𝐴 X_rm 𝑁 ) ∈ ℂ ) → ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) = ( 2 · ( ( 𝐴 X_rm 𝑁 ) · ( 𝐴 X_rm 𝑁 ) ) ) )
75	74	eqcomd	⊢ ( ( 2 ∈ ℂ ∧ ( 𝐴 X_rm 𝑁 ) ∈ ℂ ∧ ( 𝐴 X_rm 𝑁 ) ∈ ℂ ) → ( 2 · ( ( 𝐴 X_rm 𝑁 ) · ( 𝐴 X_rm 𝑁 ) ) ) = ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
76	65 67 67 75	syl3anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · ( ( 𝐴 X_rm 𝑁 ) · ( 𝐴 X_rm 𝑁 ) ) ) = ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
77	73 76	eqtrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · ( ( 𝐴 X_rm 𝑁 ) ↑ 2 ) ) = ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
78	64 71 77	3eqtrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) = ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
79	61 78	breqtrrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) )
80	49	peano2zd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ∈ ℤ )
81		dvdsmultr2	⊢ ( ( ( 𝐴 X_rm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ ∧ ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ∈ ℤ ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ) ) )
82	31 46 80 81	syl3anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ) ) )
83	79 82	mpd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ) )
84	46	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℂ )
85	84	mulid1d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · 1 ) = ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) )
86	85	oveq2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · 1 ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) )
87	49	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm ( 2 · 𝑁 ) ) ∈ ℂ )
88	84 87 70	adddid	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · 1 ) ) )
89	50	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) ∈ ℂ )
90	89 84	subnegd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) )
91	86 88 90	3eqtr4d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( ( 𝐴 X_rm ( 2 · 𝑁 ) ) + 1 ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) )
92	83 91	breqtrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) )
93	8	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Y_rm 𝑁 ) ∈ ℤ )
94	29 30 93	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm 𝑁 ) ∈ ℤ )
95	37 94	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · ( 𝐴 Y_rm 𝑁 ) ) ∈ ℤ )
96		dvdsmul2	⊢ ( ( ( 2 · ( 𝐴 Y_rm 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 X_rm 𝑁 ) ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 2 · ( 𝐴 Y_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
97	95 31 96	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 2 · ( 𝐴 Y_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
98		rmydbl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Y_rm ( 2 · 𝑁 ) ) = ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 Y_rm 𝑁 ) ) )
99	29 30 98	syl2anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 2 · 𝑁 ) ) = ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 Y_rm 𝑁 ) ) )
100	94	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm 𝑁 ) ∈ ℂ )
101	65 67 100	mul32d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 2 · ( 𝐴 X_rm 𝑁 ) ) · ( 𝐴 Y_rm 𝑁 ) ) = ( ( 2 · ( 𝐴 Y_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
102	99 101	eqtrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 2 · 𝑁 ) ) = ( ( 2 · ( 𝐴 Y_rm 𝑁 ) ) · ( 𝐴 X_rm 𝑁 ) ) )
103	97 102	breqtrrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( 𝐴 Y_rm ( 2 · 𝑁 ) ) )
104		dvdsmultr2	⊢ ( ( ( 𝐴 X_rm 𝑁 ) ∈ ℤ ∧ ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ ∧ ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ∈ ℤ ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( 𝐴 Y_rm ( 2 · 𝑁 ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
105	31 55 57 104	syl3anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( 𝐴 Y_rm ( 2 · 𝑁 ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
106	103 105	mpd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) )
107	31 52 58 92 106	dvds2addd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
108	34	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑏 ∈ ℂ )
109	38	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 2 · 𝑁 ) ∈ ℂ )
110	108 70 109	adddird	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) = ( ( 𝑏 · ( 2 · 𝑁 ) ) + ( 1 · ( 2 · 𝑁 ) ) ) )
111	110	oveq2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( ( 𝑏 · ( 2 · 𝑁 ) ) + ( 1 · ( 2 · 𝑁 ) ) ) ) )
112	32	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 𝑀 ∈ ℂ )
113	43	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑏 · ( 2 · 𝑁 ) ) ∈ ℂ )
114		1zzd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → 1 ∈ ℤ )
115	114 38	zmulcld	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 1 · ( 2 · 𝑁 ) ) ∈ ℤ )
116	115	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 1 · ( 2 · 𝑁 ) ) ∈ ℂ )
117	112 113 116	addassd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 1 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( ( 𝑏 · ( 2 · 𝑁 ) ) + ( 1 · ( 2 · 𝑁 ) ) ) ) )
118	109	mulid2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 1 · ( 2 · 𝑁 ) ) = ( 2 · 𝑁 ) )
119	118	oveq2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 1 · ( 2 · 𝑁 ) ) ) = ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 2 · 𝑁 ) ) )
120	111 117 119	3eqtr2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) = ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 2 · 𝑁 ) ) )
121	120	oveq2d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Y_rm ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 2 · 𝑁 ) ) ) )
122		rmyadd	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ ( 2 · 𝑁 ) ∈ ℤ ) → ( 𝐴 Y_rm ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 2 · 𝑁 ) ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
123	29 44 38 122	syl3anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) + ( 2 · 𝑁 ) ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
124	121 123	eqtrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) = ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
125	124	oveq1d	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) = ( ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) )
126	58	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ∈ ℂ )
127	51	zcnd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℂ )
128	89 126 127	addsubd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) = ( ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
129	125 128	eqtrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) = ( ( ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 X_rm ( 2 · 𝑁 ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) + ( ( 𝐴 X_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) · ( 𝐴 Y_rm ( 2 · 𝑁 ) ) ) ) )
130	107 129	breqtrrd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) )
131	130	olcd	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) ) )
132		jm2.25lem1	⊢ ( ( ( ( 𝐴 X_rm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Y_rm 𝑀 ) ∈ ℤ ) ∧ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) ∈ ℤ ∧ ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ∈ ℤ ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) ) ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
133	31 33 42 46 131 132	syl221anc	⊢ ( ( 𝑏 ∈ ℤ ∧ ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
134	133	pm5.74da	⊢ ( 𝑏 ∈ ℤ → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) )
135		oveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝑏 · ( 2 · 𝑁 ) ) )
136	135	oveq2d	⊢ ( 𝑎 = 𝑏 → ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) )
137	136	oveq2d	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) )
138	137	oveq1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) )
139	138	breq2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ) )
140	137	oveq1d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) )
141	140	breq2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
142	139 141	orbi12d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
143	142	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑏 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) )
144		oveq1	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 · ( 2 · 𝑁 ) ) = ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) )
145	144	oveq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) )
146	145	oveq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) )
147	146	oveq1d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) )
148	147	breq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ) )
149	146	oveq1d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) )
150	149	breq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
151	148 150	orbi12d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
152	151	imbi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( ( 𝑏 + 1 ) · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) )
153		oveq1	⊢ ( 𝑎 = 0 → ( 𝑎 · ( 2 · 𝑁 ) ) = ( 0 · ( 2 · 𝑁 ) ) )
154	153	oveq2d	⊢ ( 𝑎 = 0 → ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) )
155	154	oveq2d	⊢ ( 𝑎 = 0 → ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) )
156	155	oveq1d	⊢ ( 𝑎 = 0 → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) )
157	156	breq2d	⊢ ( 𝑎 = 0 → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ) )
158	155	oveq1d	⊢ ( 𝑎 = 0 → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) )
159	158	breq2d	⊢ ( 𝑎 = 0 → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
160	157 159	orbi12d	⊢ ( 𝑎 = 0 → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
161	160	imbi2d	⊢ ( 𝑎 = 0 → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) )
162		oveq1	⊢ ( 𝑎 = 𝐼 → ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐼 · ( 2 · 𝑁 ) ) )
163	162	oveq2d	⊢ ( 𝑎 = 𝐼 → ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) )
164	163	oveq2d	⊢ ( 𝑎 = 𝐼 → ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) )
165	164	oveq1d	⊢ ( 𝑎 = 𝐼 → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) )
166	165	breq2d	⊢ ( 𝑎 = 𝐼 → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ) )
167	164	oveq1d	⊢ ( 𝑎 = 𝐼 → ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) = ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) )
168	167	breq2d	⊢ ( 𝑎 = 𝐼 → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ↔ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
169	166 168	orbi12d	⊢ ( 𝑎 = 𝐼 → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
170	169	imbi2d	⊢ ( 𝑎 = 𝐼 → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) )
171	134 143 152 161 170	zindbi	⊢ ( 𝐼 ∈ ℤ → ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 0 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) )
172	28 171	mpbid	⊢ ( 𝐼 ∈ ℤ → ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
173	172	impcom	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) ∧ 𝐼 ∈ ℤ ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
174	173	3impa	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℤ ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm ( 𝑀 + ( 𝐼 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )

Metamath Proof Explorer

Theorem jm2.25

Proof