Theorem jm2.26a

Description: Lemma for jm2.26 . Reverse direction is required to prove forward direction, so do it separately. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014)

	Ref	Expression
Assertion	jm2.26a	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		simplr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
3		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ )
4	1 2 3	sylancr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 2 · 𝑁 ) ∈ ℤ )
5		zsubcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℤ )
6	5	adantl	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝐾 − 𝑀 ) ∈ ℤ )
7		divides	⊢ ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ ( 𝐾 − 𝑀 ) ∈ ℤ ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) )
8	4 6 7	syl2anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) )
9		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
10		simplrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → 𝑀 ∈ ℤ )
11		simpllr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → 𝑁 ∈ ℤ )
12		simpr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℤ )
13		jm2.25	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
14	9 10 11 12 13	syl121anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
15	14	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
16		oveq2	⊢ ( ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) → ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) = ( 𝑀 + ( 𝐾 − 𝑀 ) ) )
17	16	oveq2d	⊢ ( ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) → ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Yrm ( 𝑀 + ( 𝐾 − 𝑀 ) ) ) )
18		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
19		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
20		pncan3	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑀 + ( 𝐾 − 𝑀 ) ) = 𝐾 )
21	18 19 20	syl2anr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 + ( 𝐾 − 𝑀 ) ) = 𝐾 )
22	21	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝑀 + ( 𝐾 − 𝑀 ) ) = 𝐾 )
23	22	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑀 + ( 𝐾 − 𝑀 ) ) ) = ( 𝐴 Yrm 𝐾 ) )
24	17 23	sylan9eqr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) → ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Yrm 𝐾 ) )
25		eqidd	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) → ( 𝐴 Yrm 𝑀 ) = ( 𝐴 Yrm 𝑀 ) )
26	24 25	acongeq12d	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) → ( ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm 𝑀 ) ) ) ↔ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
27	15 26	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
28	27	rexlimdva2	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ∃ 𝑎 ∈ ℤ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − 𝑀 ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
29	8 28	sylbid	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
30		simprl	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
31		znegcl	⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
32	31	ad2antll	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → - 𝑀 ∈ ℤ )
33	30 32	zsubcld	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝐾 − - 𝑀 ) ∈ ℤ )
34		divides	⊢ ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ ( 𝐾 − - 𝑀 ) ∈ ℤ ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) )
35	4 33 34	syl2anc	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) )
36		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
37	36	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
38	37	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
39	9 11 38	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
40		simplrl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → 𝐾 ∈ ℤ )
41		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
42	41	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐴 Yrm 𝐾 ) ∈ ℤ )
43	9 40 42	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝐾 ) ∈ ℤ )
44	41	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
45	9 10 44	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
46	39 43 45	3jca	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝐾 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ) )
47	46	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝐾 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ) )
48	32	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → - 𝑀 ∈ ℤ )
49		jm2.25	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( - 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm - 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm - 𝑀 ) ) ) )
50	9 48 11 12 49	syl121anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm - 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm - 𝑀 ) ) ) )
51	50	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm - 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm - 𝑀 ) ) ) )
52		oveq2	⊢ ( ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) → ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) = ( - 𝑀 + ( 𝐾 − - 𝑀 ) ) )
53	52	oveq2d	⊢ ( ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) → ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Yrm ( - 𝑀 + ( 𝐾 − - 𝑀 ) ) ) )
54	18	negcld	⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℂ )
55		pncan3	⊢ ( ( - 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( - 𝑀 + ( 𝐾 − - 𝑀 ) ) = 𝐾 )
56	54 19 55	syl2anr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( - 𝑀 + ( 𝐾 − - 𝑀 ) ) = 𝐾 )
57	56	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( - 𝑀 + ( 𝐾 − - 𝑀 ) ) = 𝐾 )
58	57	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm ( - 𝑀 + ( 𝐾 − - 𝑀 ) ) ) = ( 𝐴 Yrm 𝐾 ) )
59	53 58	sylan9eqr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) = ( 𝐴 Yrm 𝐾 ) )
60		rmyneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm - 𝑀 ) = - ( 𝐴 Yrm 𝑀 ) )
61	9 10 60	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) → ( 𝐴 Yrm - 𝑀 ) = - ( 𝐴 Yrm 𝑀 ) )
62	61	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( 𝐴 Yrm - 𝑀 ) = - ( 𝐴 Yrm 𝑀 ) )
63	59 62	acongeq12d	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − ( 𝐴 Yrm - 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm ( - 𝑀 + ( 𝑎 · ( 2 · 𝑁 ) ) ) ) − - ( 𝐴 Yrm - 𝑀 ) ) ) ↔ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - - ( 𝐴 Yrm 𝑀 ) ) ) ) )
64	51 63	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - - ( 𝐴 Yrm 𝑀 ) ) ) )
65		acongneg2	⊢ ( ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝐾 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℤ ) ∧ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - - ( 𝐴 Yrm 𝑀 ) ) ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
66	47 64 65	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
67	66	rexlimdva2	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ∃ 𝑎 ∈ ℤ ( 𝑎 · ( 2 · 𝑁 ) ) = ( 𝐾 − - 𝑀 ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
68	35 67	sylbid	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
69	29 68	jaod	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )