Theorem jm2.26a 44200

Description: Lemma for jm2.26 44202. 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.)

Assertion

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

Proof of Theorem jm2.26a

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2z 12755	. . . . 5 ⊢ 2 ∈ ℤ
2		simplr 781	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑁 ∈ ℤ)
3		zmulcl 12772	. . . . 5 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
4	1, 2, 3	sylancr 599	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (2 · 𝑁) ∈ ℤ)
5		zsubcl 12765	. . . . 5 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 − 𝑀) ∈ ℤ)
6	5	adantl 487	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝐾 − 𝑀) ∈ ℤ)
7		divides 16453	. . . 4 ⊢ (((2 · 𝑁) ∈ ℤ ∧ (𝐾 − 𝑀) ∈ ℤ) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ↔ ∃𝑎 ∈ ℤ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)))
8	4, 6, 7	syl2anc 596	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ↔ ∃𝑎 ∈ ℤ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)))
9		simplll 787	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → 𝐴 ∈ (ℤ≥‘2))
10		simplrr 790	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → 𝑀 ∈ ℤ)
11		simpllr 788	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → 𝑁 ∈ ℤ)
12		simpr 490	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → 𝑎 ∈ ℤ)
13		jm2.25 44199	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
14	9, 10, 11, 12, 13	syl121anc 1403	. . . . . 6 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
15	14	adantr 486	. . . . 5 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
16		oveq2 7451	. . . . . . . 8 ⊢ ((𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀) → (𝑀 + (𝑎 · (2 · 𝑁))) = (𝑀 + (𝐾 − 𝑀)))
17	16	oveq2d 7459	. . . . . . 7 ⊢ ((𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀) → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm (𝑀 + (𝐾 − 𝑀))))
18		zcn 12725	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
19		zcn 12725	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
20		pncan3 11592	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑀 + (𝐾 − 𝑀)) = 𝐾)
21	18, 19, 20	syl2anr 609	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 + (𝐾 − 𝑀)) = 𝐾)
22	21	ad2antlr 740	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝑀 + (𝐾 − 𝑀)) = 𝐾)
23	22	oveq2d 7459	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝐴 Yrm (𝑀 + (𝐾 − 𝑀))) = (𝐴 Yrm 𝐾))
24	17, 23	sylan9eqr 2820	. . . . . 6 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)) → (𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm 𝐾))
25		eqidd 2764	. . . . . 6 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)) → (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑀))
26	24, 25	acongeq12d 44179	. . . . 5 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
27	15, 26	mpbid 235	. . . 4 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))))
28	27	rexlimdva2 3169	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (∃𝑎 ∈ ℤ (𝑎 · (2 · 𝑁)) = (𝐾 − 𝑀) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
29	8, 28	sylbid 243	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
30		simprl 783	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝐾 ∈ ℤ)
31		znegcl 12758	. . . . . 6 ⊢ (𝑀 ∈ ℤ → -𝑀 ∈ ℤ)
32	31	ad2antll 742	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → -𝑀 ∈ ℤ)
33	30, 32	zsubcld 12835	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝐾 − -𝑀) ∈ ℤ)
34		divides 16453	. . . 4 ⊢ (((2 · 𝑁) ∈ ℤ ∧ (𝐾 − -𝑀) ∈ ℤ) → ((2 · 𝑁) ∥ (𝐾 − -𝑀) ↔ ∃𝑎 ∈ ℤ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)))
35	4, 33, 34	syl2anc 596	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((2 · 𝑁) ∥ (𝐾 − -𝑀) ↔ ∃𝑎 ∈ ℤ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)))
36		frmx 44113	. . . . . . . . . 10 ⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0
37	36	fovcl 7571	. . . . . . . . 9 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
38	37	nn0zd 12745	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℤ)
39	9, 11, 38	syl2anc 596	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℤ)
40		simplrl 789	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → 𝐾 ∈ ℤ)
41		frmy 44114	. . . . . . . . 9 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
42	41	fovcl 7571	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐴 Yrm 𝐾) ∈ ℤ)
43	9, 40, 42	syl2anc 596	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝐴 Yrm 𝐾) ∈ ℤ)
44	41	fovcl 7571	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
45	9, 10, 44	syl2anc 596	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
46	39, 43, 45	3jca 1146	. . . . . 6 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝐾) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ))
47	46	adantr 486	. . . . 5 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝐾) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ))
48	32	adantr 486	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → -𝑀 ∈ ℤ)
49		jm2.25 44199	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ ( -𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm -𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm -𝑀))))
50	9, 48, 11, 12, 49	syl121anc 1403	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm -𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm -𝑀))))
51	50	adantr 486	. . . . . 6 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm -𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm -𝑀))))
52		oveq2 7451	. . . . . . . . 9 ⊢ ((𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀) → ( -𝑀 + (𝑎 · (2 · 𝑁))) = ( -𝑀 + (𝐾 − -𝑀)))
53	52	oveq2d 7459	. . . . . . . 8 ⊢ ((𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀) → (𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm ( -𝑀 + (𝐾 − -𝑀))))
54	18	negcld 11683	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → -𝑀 ∈ ℂ)
55		pncan3 11592	. . . . . . . . . . 11 ⊢ (( -𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ( -𝑀 + (𝐾 − -𝑀)) = 𝐾)
56	54, 19, 55	syl2anr 609	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ( -𝑀 + (𝐾 − -𝑀)) = 𝐾)
57	56	ad2antlr 740	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → ( -𝑀 + (𝐾 − -𝑀)) = 𝐾)
58	57	oveq2d 7459	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝐴 Yrm ( -𝑀 + (𝐾 − -𝑀))) = (𝐴 Yrm 𝐾))
59	53, 58	sylan9eqr 2820	. . . . . . 7 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → (𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) = (𝐴 Yrm 𝐾))
60		rmyneg 44128	. . . . . . . . 9 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm -𝑀) = -(𝐴 Yrm 𝑀))
61	9, 10, 60	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) → (𝐴 Yrm -𝑀) = -(𝐴 Yrm 𝑀))
62	61	adantr 486	. . . . . . 7 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → (𝐴 Yrm -𝑀) = -(𝐴 Yrm 𝑀))
63	59, 62	acongeq12d 44179	. . . . . 6 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − (𝐴 Yrm -𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm ( -𝑀 + (𝑎 · (2 · 𝑁)))) − -(𝐴 Yrm -𝑀))) ↔ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − - -(𝐴 Yrm 𝑀)))))
64	51, 63	mpbid 235	. . . . 5 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − - -(𝐴 Yrm 𝑀))))
65		acongneg2 44177	. . . . 5 ⊢ ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝐾) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − - -(𝐴 Yrm 𝑀)))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))))
66	47, 64, 65	syl2anc 596	. . . 4 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ 𝑎 ∈ ℤ) ∧ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))))
67	66	rexlimdva2 3169	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (∃𝑎 ∈ ℤ (𝑎 · (2 · 𝑁)) = (𝐾 − -𝑀) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
68	35, 67	sylbid 243	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((2 · 𝑁) ∥ (𝐾 − -𝑀) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
69	29, 68	jaod 873	1 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∃wrex 3090   class class class wbr 5106  ‘cfv 6558  (class class class)co 7443  ℂcc 11225   + caddc 11230   · cmul 11232   − cmin 11568   -cneg 11569  2c2 12424  ℕ₀cn0 12633  ℤcz 12720  ℤ_≥cuz 12992   ∥ cdvds 16451   X_rm crmx 44100   Y_rm crmy 44101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-inf2 9669  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304  ax-pre-sup 11305  ax-addf 11306

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-isom 6567  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-of 7717  df-om 7902  df-1st 8025  df-2nd 8026  df-supp 8205  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-1o 8504  df-2o 8505  df-oadd 8508  df-omul 8509  df-er 8745  df-map 8877  df-pm 8878  df-ixp 8954  df-en 9002  df-dom 9003  df-sdom 9004  df-fin 9005  df-fsupp 9382  df-fi 9430  df-sup 9461  df-inf 9462  df-oi 9531  df-card 10047  df-acn 10050  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001  df-nn 12363  df-2 12432  df-3 12433  df-4 12434  df-5 12435  df-6 12436  df-7 12437  df-8 12438  df-9 12439  df-n0 12634  df-xnn0 12707  df-z 12721  df-dec 12842  df-uz 12993  df-q 13103  df-rp 13148  df-xneg 13268  df-xadd 13269  df-xmul 13270  df-ioo 13507  df-ioc 13508  df-ico 13509  df-icc 13510  df-fz 13667  df-fzo 13816  df-fl 13959  df-mod 14037  df-seq 14172  df-exp 14232  df-fac 14445  df-bc 14474  df-hash 14502  df-shft 15249  df-cj 15295  df-re 15296  df-im 15297  df-sqrt 15431  df-abs 15432  df-limsup 15667  df-clim 15684  df-rlim 15685  df-sum 15883  df-ef 16262  df-sin 16264  df-cos 16265  df-pi 16267  df-dvds 16452  df-gcd 16694  df-numer 16940  df-denom 16941  df-struct 17354  df-sets 17371  df-slot 17389  df-ndx 17401  df-base 17417  df-ress 17438  df-plusg 17470  df-mulr 17471  df-starv 17472  df-sca 17473  df-vsca 17474  df-ip 17475  df-tset 17476  df-ple 17477  df-ds 17479  df-unif 17480  df-hom 17481  df-cco 17482  df-rest 17622  df-topn 17623  df-0g 17641  df-gsum 17642  df-topgen 17643  df-pt 17644  df-prds 17647  df-xrs 17703  df-qtop 17708  df-imas 17709  df-xps 17711  df-mre 17785  df-mrc 17786  df-acs 17788  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-submnd 19008  df-mulg 19307  df-cntz 19561  df-cmn 20026  df-psmet 21700  df-xmet 21701  df-met 21702  df-bl 21703  df-mopn 21704  df-fbas 21705  df-fg 21706  df-cnfld 21709  df-top 23242  df-topon 23259  df-topsp 23281  df-bases 23294  df-cld 23367  df-ntr 23368  df-cls 23369  df-nei 23446  df-lp 23484  df-perf 23485  df-cn 23575  df-cnp 23576  df-haus 23663  df-tx 23911  df-hmeo 24104  df-fil 24195  df-fm 24287  df-flim 24288  df-flf 24289  df-xms 24669  df-ms 24670  df-tms 24671  df-cncf 25229  df-limc 26216  df-dv 26217  df-log 26914  df-squarenn 44041  df-pell1qr 44042  df-pell14qr 44043  df-pell1234qr 44044  df-pellfund 44045  df-rmx 44102  df-rmy 44103

This theorem is used by:  jm2.26  44202