Theorem jm2.26 39606

Description: Lemma 2.26 of [JonesMatijasevic] p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014.)

Assertion

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

Proof of Theorem jm2.26

Dummy variables 𝑘 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		acongrep 39584	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℤ) → ∃𝑚 ∈ (0...𝑁)((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))
2	1	ad2ant2l 744	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ∃𝑚 ∈ (0...𝑁)((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))
3		acongrep 39584	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) → ∃𝑘 ∈ (0...𝑁)((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)))
4	3	ad2ant2lr 746	. . . . . 6 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ∃𝑘 ∈ (0...𝑁)((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)))
5		2z 12017	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
6		simpl1l 1220	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ))
7		nnz 12007	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
8	7	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℤ)
9	6, 8	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑁 ∈ ℤ)
10		zmulcl 12034	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
11	5, 9, 10	sylancr 589	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (2 · 𝑁) ∈ ℤ)
12		simplrl 775	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝐾 ∈ ℤ)
13	12	3ad2antl1 1181	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝐾 ∈ ℤ)
14		simpl3l 1224	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑚 ∈ (0...𝑁))
15		elfzelz 12911	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑚 ∈ ℤ)
17		simplrr 776	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑀 ∈ ℤ)
18	17	3ad2antl1 1181	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑀 ∈ ℤ)
19		simpl2r 1223	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)))
20		simpl2l 1222	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑘 ∈ (0...𝑁))
21		simplll 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝐴 ∈ (ℤ≥‘2))
22	21	3ad2antl1 1181	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝐴 ∈ (ℤ≥‘2))
23		frmx 39517	. . . . . . . . . . . . . . . . . 18 ⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0
24	23	fovcl 7281	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ0)
25	24	nn0zd 12088	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℤ)
26	22, 9, 25	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (𝐴 Xrm 𝑁) ∈ ℤ)
27		elfzelz 12911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
28	20, 27	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑘 ∈ ℤ)
29		frmy 39518	. . . . . . . . . . . . . . . . 17 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
30	29	fovcl 7281	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑘 ∈ ℤ) → (𝐴 Yrm 𝑘) ∈ ℤ)
31	22, 28, 30	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (𝐴 Yrm 𝑘) ∈ ℤ)
32	29	fovcl 7281	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
33	22, 18, 32	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (𝐴 Yrm 𝑀) ∈ ℤ)
34	29	fovcl 7281	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑚 ∈ ℤ) → (𝐴 Yrm 𝑚) ∈ ℤ)
35	22, 16, 34	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (𝐴 Yrm 𝑚) ∈ ℤ)
36	29	fovcl 7281	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐴 Yrm 𝐾) ∈ ℤ)
37	22, 13, 36	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (𝐴 Yrm 𝐾) ∈ ℤ)
38		jm2.26a 39604	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝐾)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝐾)))))
39	22, 9, 28, 13, 38	syl22anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝐾)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝐾)))))
40	19, 39	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝐾)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝐾))))
41		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))))
42		acongtr 39582	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑘) ∈ ℤ) ∧ ((𝐴 Yrm 𝐾) ∈ ℤ ∧ (𝐴 Yrm 𝑀) ∈ ℤ) ∧ (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝐾)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝐾))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝑀))))
43	26, 31, 37, 33, 40, 41, 42	syl222anc 1382	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝑀))))
44		simpl3r 1225	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))
45		acongsym 39580	. . . . . . . . . . . . . . . . 17 ⊢ ((((2 · 𝑁) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀))) → ((2 · 𝑁) ∥ (𝑀 − 𝑚) ∨ (2 · 𝑁) ∥ (𝑀 − -𝑚)))
46	11, 16, 18, 44, 45	syl31anc 1369	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((2 · 𝑁) ∥ (𝑀 − 𝑚) ∨ (2 · 𝑁) ∥ (𝑀 − -𝑚)))
47		jm2.26a 39604	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝑀 − 𝑚) ∨ (2 · 𝑁) ∥ (𝑀 − -𝑚)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − -(𝐴 Yrm 𝑚)))))
48	22, 9, 18, 16, 47	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (((2 · 𝑁) ∥ (𝑀 − 𝑚) ∨ (2 · 𝑁) ∥ (𝑀 − -𝑚)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − -(𝐴 Yrm 𝑚)))))
49	46, 48	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − -(𝐴 Yrm 𝑚))))
50		acongtr 39582	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 Xrm 𝑁) ∈ ℤ ∧ (𝐴 Yrm 𝑘) ∈ ℤ) ∧ ((𝐴 Yrm 𝑀) ∈ ℤ ∧ (𝐴 Yrm 𝑚) ∈ ℤ) ∧ (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝑀))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑀) − -(𝐴 Yrm 𝑚))))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝑚))))
51	26, 31, 33, 35, 43, 49, 50	syl222anc 1382	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝑚))))
52		jm2.26lem3 39605	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝑘 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁)) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − (𝐴 Yrm 𝑚)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝑘) − -(𝐴 Yrm 𝑚)))) → 𝑘 = 𝑚)
53	6, 20, 14, 51, 52	syl121anc 1371	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝑘 = 𝑚)
54		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → 𝑘 = 𝑚)
55		eqidd 2824	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑚 → 𝐾 = 𝐾)
56	54, 55	acongeq12d 39583	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑚 → (((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)) ↔ ((2 · 𝑁) ∥ (𝑚 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑚 − -𝐾))))
57	53, 56	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → (((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)) ↔ ((2 · 𝑁) ∥ (𝑚 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑚 − -𝐾))))
58	19, 57	mpbid 234	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((2 · 𝑁) ∥ (𝑚 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑚 − -𝐾)))
59		acongsym 39580	. . . . . . . . . . 11 ⊢ ((((2 · 𝑁) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑚 − -𝐾))) → ((2 · 𝑁) ∥ (𝐾 − 𝑚) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑚)))
60	11, 16, 13, 58, 59	syl31anc 1369	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((2 · 𝑁) ∥ (𝐾 − 𝑚) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑚)))
61		acongtr 39582	. . . . . . . . . 10 ⊢ ((((2 · 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (((2 · 𝑁) ∥ (𝐾 − 𝑚) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑚)) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)))
62	11, 13, 16, 18, 60, 44, 61	syl222anc 1382	. . . . . . . . 9 ⊢ (((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)))) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)))
63	62	3exp1 1348	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑘 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾))) → ((𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀))))))
64	63	expd 418	. . . . . . 7 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑘 ∈ (0...𝑁) → (((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)) → ((𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)))))))
65	64	rexlimdv 3285	. . . . . 6 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (∃𝑘 ∈ (0...𝑁)((2 · 𝑁) ∥ (𝑘 − 𝐾) ∨ (2 · 𝑁) ∥ (𝑘 − -𝐾)) → ((𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀))))))
66	4, 65	mpd 15	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑚 ∈ (0...𝑁) ∧ ((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀))) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)))))
67	66	expd 418	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑚 ∈ (0...𝑁) → (((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀))))))
68	67	rexlimdv 3285	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (∃𝑚 ∈ (0...𝑁)((2 · 𝑁) ∥ (𝑚 − 𝑀) ∨ (2 · 𝑁) ∥ (𝑚 − -𝑀)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)))))
69	2, 68	mpd 15	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) → ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀))))
70		jm2.26a 39604	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
71	7, 70	sylanl2 679	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
72	69, 71	impbid 214	1 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) ↔ ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   ∈ wcel 2114  ∃wrex 3141   class class class wbr 5068  ‘cfv 6357  (class class class)co 7158  0cc0 10539   · cmul 10544   − cmin 10872  -cneg 10873  ℕcn 11640  2c2 11695  ℕ₀cn0 11900  ℤcz 11984  ℤ_≥cuz 12246  ...cfz 12895   ∥ cdvds 15609   X_rm crmx 39504   Y_rm crmy 39505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-inf2 9106  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616  ax-pre-sup 10617  ax-addf 10618  ax-mulf 10619

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-2o 8105  df-oadd 8108  df-omul 8109  df-er 8291  df-map 8410  df-pm 8411  df-ixp 8464  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-fi 8877  df-sup 8908  df-inf 8909  df-oi 8976  df-card 9370  df-acn 9373  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-xnn0 11971  df-z 11985  df-dec 12102  df-uz 12247  df-q 12352  df-rp 12393  df-xneg 12510  df-xadd 12511  df-xmul 12512  df-ioo 12745  df-ioc 12746  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-fl 13165  df-mod 13241  df-seq 13373  df-exp 13433  df-fac 13637  df-bc 13666  df-hash 13694  df-shft 14428  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-limsup 14830  df-clim 14847  df-rlim 14848  df-sum 15045  df-ef 15423  df-sin 15425  df-cos 15426  df-pi 15428  df-dvds 15610  df-gcd 15846  df-numer 16077  df-denom 16078  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910  df-psmet 20539  df-xmet 20540  df-met 20541  df-bl 20542  df-mopn 20543  df-fbas 20544  df-fg 20545  df-cnfld 20548  df-top 21504  df-topon 21521  df-topsp 21543  df-bases 21556  df-cld 21629  df-ntr 21630  df-cls 21631  df-nei 21708  df-lp 21746  df-perf 21747  df-cn 21837  df-cnp 21838  df-haus 21925  df-tx 22172  df-hmeo 22365  df-fil 22456  df-fm 22548  df-flim 22549  df-flf 22550  df-xms 22932  df-ms 22933  df-tms 22934  df-cncf 23488  df-limc 24466  df-dv 24467  df-log 25142  df-squarenn 39445  df-pell1qr 39446  df-pell14qr 39447  df-pell1234qr 39448  df-pellfund 39449  df-rmx 39506  df-rmy 39507

This theorem is referenced by:  jm2.27a  39609