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

Metamath Proof Explorer

Theorem jm2.26

Proof