jm2.26

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

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

Proof

Step	Hyp	Ref	Expression
1		acongrep	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℤ ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) )
2	1	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) )
3		acongrep	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ∃ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) )
4	3	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ∃ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) )
5		2z	⊢ 2 ∈ ℤ
6		simpl1l	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) )
7		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
8	7	adantl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
9	6 8	syl	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑁 ∈ ℤ )
10		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ )
11	5 9 10	sylancr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 2 · 𝑁 ) ∈ ℤ )
12		simplrl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝐾 ∈ ℤ )
13	12	3ad2antl1	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝐾 ∈ ℤ )
14		simpl3l	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑚 ∈ ( 0 ... 𝑁 ) )
15	14	elfzelzd	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑚 ∈ ℤ )
16		simplrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑀 ∈ ℤ )
17	16	3ad2antl1	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑀 ∈ ℤ )
18		simpl2r	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) )
19		simpl2l	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
20		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
21	20	3ad2antl1	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝐴 ∈ ( ℤ_≥ ‘ 2 ) )
22		frmx	⊢ X_rm : ( ( ℤ_≥ ‘ 2 ) × ℤ ) ⟶ ℕ₀
23	22	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∈ ℕ₀ )
24	23	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 X_rm 𝑁 ) ∈ ℤ )
25	21 9 24	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 𝐴 X_rm 𝑁 ) ∈ ℤ )
26	19	elfzelzd	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑘 ∈ ℤ )
27		frmy	⊢ Y_rm : ( ( ℤ_≥ ‘ 2 ) × ℤ ) ⟶ ℤ
28	27	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑘 ∈ ℤ ) → ( 𝐴 Y_rm 𝑘 ) ∈ ℤ )
29	21 26 28	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 𝐴 Y_rm 𝑘 ) ∈ ℤ )
30	27	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Y_rm 𝑀 ) ∈ ℤ )
31	21 17 30	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 𝐴 Y_rm 𝑀 ) ∈ ℤ )
32	27	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐴 Y_rm 𝑚 ) ∈ ℤ )
33	21 15 32	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 𝐴 Y_rm 𝑚 ) ∈ ℤ )
34	27	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐴 Y_rm 𝐾 ) ∈ ℤ )
35	21 13 34	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( 𝐴 Y_rm 𝐾 ) ∈ ℤ )
36		jm2.26a	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝐾 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝐾 ) ) ) ) )
37	21 9 26 13 36	syl22anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝐾 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝐾 ) ) ) ) )
38	18 37	mpd	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝐾 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝐾 ) ) ) )
39		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
40		acongtr	⊢ ( ( ( ( 𝐴 X_rm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Y_rm 𝑘 ) ∈ ℤ ) ∧ ( ( 𝐴 Y_rm 𝐾 ) ∈ ℤ ∧ ( 𝐴 Y_rm 𝑀 ) ∈ ℤ ) ∧ ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝐾 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝐾 ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
41	25 29 35 31 38 39 40	syl222anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) )
42		simpl3r	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) )
43		acongsym	⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝑀 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑀 − - 𝑚 ) ) )
44	11 15 17 42 43	syl31anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝑀 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑀 − - 𝑚 ) ) )
45		jm2.26a	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑀 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑀 − - 𝑚 ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) ) )
46	21 9 17 15 45	syl22anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑀 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑀 − - 𝑚 ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) ) )
47	44 46	mpd	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) )
48		acongtr	⊢ ( ( ( ( 𝐴 X_rm 𝑁 ) ∈ ℤ ∧ ( 𝐴 Y_rm 𝑘 ) ∈ ℤ ) ∧ ( ( 𝐴 Y_rm 𝑀 ) ∈ ℤ ∧ ( 𝐴 Y_rm 𝑚 ) ∈ ℤ ) ∧ ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑀 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) )
49	25 29 31 33 41 47 48	syl222anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) )
50		jm2.26lem3	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − ( 𝐴 Y_rm 𝑚 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝑘 ) − - ( 𝐴 Y_rm 𝑚 ) ) ) ) → 𝑘 = 𝑚 )
51	6 19 14 49 50	syl121anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → 𝑘 = 𝑚 )
52		id	⊢ ( 𝑘 = 𝑚 → 𝑘 = 𝑚 )
53		eqidd	⊢ ( 𝑘 = 𝑚 → 𝐾 = 𝐾 )
54	52 53	acongeq12d	⊢ ( 𝑘 = 𝑚 → ( ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ↔ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝐾 ) ) ) )
55	51 54	syl	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ↔ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝐾 ) ) ) )
56	18 55	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝐾 ) ) )
57		acongsym	⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝐾 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑚 ) ) )
58	11 15 13 56 57	syl31anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑚 ) ) )
59		acongtr	⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑚 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑚 ) ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) )
60	11 13 15 17 58 42 59	syl222anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) ∧ ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) ) ∧ ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) )
61	60	3exp1	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) ) ) )
62	61	expd	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) ) ) ) )
63	62	rexlimdv	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 2 · 𝑁 ) ∥ ( 𝑘 − 𝐾 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑘 − - 𝐾 ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) ) ) )
64	4 63	mpd	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑚 ∈ ( 0 ... 𝑁 ) ∧ ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) ) )
65	64	expd	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) ) ) )
66	65	rexlimdv	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 2 · 𝑁 ) ∥ ( 𝑚 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝑚 − - 𝑀 ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) ) )
67	2 66	mpd	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) → ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) )
68		jm2.26a	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
69	7 68	sylanl2	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) → ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ) )
70	67 69	impbid	⊢ ( ( ( 𝐴 ∈ ( ℤ_≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − ( 𝐴 Y_rm 𝑀 ) ) ∨ ( 𝐴 X_rm 𝑁 ) ∥ ( ( 𝐴 Y_rm 𝐾 ) − - ( 𝐴 Y_rm 𝑀 ) ) ) ↔ ( ( 2 · 𝑁 ) ∥ ( 𝐾 − 𝑀 ) ∨ ( 2 · 𝑁 ) ∥ ( 𝐾 − - 𝑀 ) ) ) )

Metamath Proof Explorer

Theorem jm2.26

Proof