Theorem jm2.26lem3

Description: Lemma for jm2.26 . Use acongrep to find K', M' ~K, M in [ 0,N ]. Thus Y(K') ~Y(M') and both are small; K' = M' on pain of contradicting 2.24, so K ~M. (Contributed by Stefan O'Rear, 3-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2		elfzelz	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
3	2	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
4	3	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℤ )
5		rmyabs	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) = ( 𝐴 Yrm ( abs ‘ 𝐾 ) ) )
6	1 4 5	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) = ( 𝐴 Yrm ( abs ‘ 𝐾 ) ) )
7	3	zred	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
8	7	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℝ )
9		elfzle1	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝐾 )
10	9	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ 𝐾 )
11	10	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 0 ≤ 𝐾 )
12	8 11	absidd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( abs ‘ 𝐾 ) = 𝐾 )
13	12	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm ( abs ‘ 𝐾 ) ) = ( 𝐴 Yrm 𝐾 ) )
14	6 13	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) = ( 𝐴 Yrm 𝐾 ) )
15		elfzelz	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℤ )
16	15	adantl	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
17	16	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℤ )
18		rmyabs	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) = ( 𝐴 Yrm ( abs ‘ 𝑀 ) ) )
19	1 17 18	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) = ( 𝐴 Yrm ( abs ‘ 𝑀 ) ) )
20	16	zred	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
21	20	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℝ )
22		elfzle1	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑀 )
23	22	adantl	⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ 𝑀 )
24	23	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 0 ≤ 𝑀 )
25	21 24	absidd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( abs ‘ 𝑀 ) = 𝑀 )
26	25	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm ( abs ‘ 𝑀 ) ) = ( 𝐴 Yrm 𝑀 ) )
27	19 26	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) = ( 𝐴 Yrm 𝑀 ) )
28	14 27	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) = ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) )
29		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
30	29	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐴 Yrm 𝐾 ) ∈ ℤ )
31	1 4 30	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ∈ ℤ )
32	31	zred	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ∈ ℝ )
33	29	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
34	1 17 33	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
35	34	zred	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝑀 ) ∈ ℝ )
36	32 35	readdcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ∈ ℝ )
37		simpllr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑁 ∈ ℕ )
38	37	nnzd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑁 ∈ ℤ )
39		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
40	38 39	syl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
41	29	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
42	1 40 41	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
43	42	zred	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℝ )
44	29	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
45	1 38 44	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
46	45	zred	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝑁 ) ∈ ℝ )
47	43 46	readdcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ∈ ℝ )
48		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
49	48	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
50	1 38 49	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
51	50	nn0red	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Xrm 𝑁 ) ∈ ℝ )
52		elfzle2	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ≤ ( 𝑁 − 1 ) )
53	52	adantl	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐾 ≤ ( 𝑁 − 1 ) )
54		lermy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐾 ≤ ( 𝑁 − 1 ) ↔ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
55	1 4 40 54	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ≤ ( 𝑁 − 1 ) ↔ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
56	55	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐾 ≤ ( 𝑁 − 1 ) ↔ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
57	53 56	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
58		simplrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
59		elfzle2	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ≤ 𝑁 )
60	58 59	syl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ≤ 𝑁 )
61		lermy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )
62	1 17 38 61	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )
63	60 62	mpbid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) )
64	63	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) )
65		le2add	⊢ ( ( ( ( 𝐴 Yrm 𝐾 ) ∈ ℝ ∧ ( 𝐴 Yrm 𝑀 ) ∈ ℝ ) ∧ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℝ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℝ ) ) → ( ( ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∧ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
66	32 35 43 46 65	syl22anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∧ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
67	66	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∧ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm 𝑁 ) ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
68	57 64 67	mp2and	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) )
69	31	zcnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ∈ ℂ )
70	34	zcnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
71	69 70	addcomd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) = ( ( 𝐴 Yrm 𝑀 ) + ( 𝐴 Yrm 𝐾 ) ) )
72	71	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) = ( ( 𝐴 Yrm 𝑀 ) + ( 𝐴 Yrm 𝐾 ) ) )
73		id	⊢ ( 𝐾 ≠ 𝑀 → 𝐾 ≠ 𝑀 )
74	73	necomd	⊢ ( 𝐾 ≠ 𝑀 → 𝑀 ≠ 𝐾 )
75	74	adantr	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 = 𝑁 ) → 𝑀 ≠ 𝐾 )
76		simpr	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 = 𝑁 ) → 𝐾 = 𝑁 )
77	75 76	neeqtrd	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 = 𝑁 ) → 𝑀 ≠ 𝑁 )
78	77	neneqd	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 = 𝑁 ) → ¬ 𝑀 = 𝑁 )
79	78	adantll	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ¬ 𝑀 = 𝑁 )
80		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
81		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
82	80 81	eleqtrdi	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
83	82	ad4antlr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
84		simprr	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
85	84	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
86		fzm1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) ) )
87	86	biimpa	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) )
88	83 85 87	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) )
89		orel2	⊢ ( ¬ 𝑀 = 𝑁 → ( ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) → 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
90	79 88 89	sylc	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
91		elfzle2	⊢ ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑀 ≤ ( 𝑁 − 1 ) )
92	90 91	syl	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → 𝑀 ≤ ( 𝑁 − 1 ) )
93		lermy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑀 ≤ ( 𝑁 − 1 ) ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
94	1 17 40 93	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝑀 ≤ ( 𝑁 − 1 ) ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
95	94	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( 𝑀 ≤ ( 𝑁 − 1 ) ↔ ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
96	92 95	mpbid	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
97		simplrl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
98		elfzle2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
99	97 98	syl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≤ 𝑁 )
100		lermy	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )
101	1 4 38 100	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ≤ 𝑁 ↔ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) ) )
102	99 101	mpbid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) )
103	102	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) )
104		le2add	⊢ ( ( ( ( 𝐴 Yrm 𝑀 ) ∈ ℝ ∧ ( 𝐴 Yrm 𝐾 ) ∈ ℝ ) ∧ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℝ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℝ ) ) → ( ( ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∧ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) ) → ( ( 𝐴 Yrm 𝑀 ) + ( 𝐴 Yrm 𝐾 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
105	35 32 43 46 104	syl22anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∧ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) ) → ( ( 𝐴 Yrm 𝑀 ) + ( 𝐴 Yrm 𝐾 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
106	105	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( ( ( 𝐴 Yrm 𝑀 ) ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∧ ( 𝐴 Yrm 𝐾 ) ≤ ( 𝐴 Yrm 𝑁 ) ) → ( ( 𝐴 Yrm 𝑀 ) + ( 𝐴 Yrm 𝐾 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ) )
107	96 103 106	mp2and	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( ( 𝐴 Yrm 𝑀 ) + ( 𝐴 Yrm 𝐾 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) )
108	72 107	eqbrtrd	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) )
109	37	nnnn0d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑁 ∈ ℕ0 )
110	109 81	eleqtrdi	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
111		fzm1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )
112	111	biimpa	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) )
113	110 97 112	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) )
114	68 108 113	mpjaodan	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ≤ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) )
115		jm2.24	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )
116	1 38 115	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )
117	36 47 51 114 116	lelttrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) < ( 𝐴 Xrm 𝑁 ) )
118	28 117	eqbrtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) )
119		simpr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≠ 𝑀 )
120		rmyeq	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 = 𝑀 ↔ ( 𝐴 Yrm 𝐾 ) = ( 𝐴 Yrm 𝑀 ) ) )
121	120	necon3bid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ≠ 𝑀 ↔ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ) )
122	1 4 17 121	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ≠ 𝑀 ↔ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ) )
123	119 122	mpbid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) )
124	7	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 𝐾 ∈ ℝ )
125		0red	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 0 ∈ ℝ )
126		simpr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 𝐾 = - 𝑀 )
127	22	ad2antll	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → 0 ≤ 𝑀 )
128	20	adantl	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → 𝑀 ∈ ℝ )
129	128	le0neg2d	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( 0 ≤ 𝑀 ↔ - 𝑀 ≤ 0 ) )
130	127 129	mpbid	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → - 𝑀 ≤ 0 )
131	130	adantr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → - 𝑀 ≤ 0 )
132	126 131	eqbrtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 𝐾 ≤ 0 )
133	10	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 0 ≤ 𝐾 )
134		letri3	⊢ ( ( 𝐾 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐾 = 0 ↔ ( 𝐾 ≤ 0 ∧ 0 ≤ 𝐾 ) ) )
135	134	biimpar	⊢ ( ( ( 𝐾 ∈ ℝ ∧ 0 ∈ ℝ ) ∧ ( 𝐾 ≤ 0 ∧ 0 ≤ 𝐾 ) ) → 𝐾 = 0 )
136	124 125 132 133 135	syl22anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 𝐾 = 0 )
137		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → 𝐾 = 0 )
138		simplr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → 𝐾 = - 𝑀 )
139	138 137	eqtr3d	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → - 𝑀 = 0 )
140	128	recnd	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → 𝑀 ∈ ℂ )
141	140	ad2antrr	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → 𝑀 ∈ ℂ )
142	141	negeq0d	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → ( 𝑀 = 0 ↔ - 𝑀 = 0 ) )
143	139 142	mpbird	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → 𝑀 = 0 )
144	137 143	eqtr4d	⊢ ( ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) ∧ 𝐾 = 0 ) → 𝐾 = 𝑀 )
145	136 144	mpdan	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 = - 𝑀 ) → 𝐾 = 𝑀 )
146	145	ex	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐾 = - 𝑀 → 𝐾 = 𝑀 ) )
147	146	necon3d	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐾 ≠ 𝑀 → 𝐾 ≠ - 𝑀 ) )
148	147	imp	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ≠ - 𝑀 )
149	58 15	syl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℤ )
150	149	znegcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → - 𝑀 ∈ ℤ )
151		rmyeq	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ∧ - 𝑀 ∈ ℤ ) → ( 𝐾 = - 𝑀 ↔ ( 𝐴 Yrm 𝐾 ) = ( 𝐴 Yrm - 𝑀 ) ) )
152	151	necon3bid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℤ ∧ - 𝑀 ∈ ℤ ) → ( 𝐾 ≠ - 𝑀 ↔ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm - 𝑀 ) ) )
153	1 4 150 152	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ≠ - 𝑀 ↔ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm - 𝑀 ) ) )
154	148 153	mpbid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm - 𝑀 ) )
155		rmyneg	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐴 Yrm - 𝑀 ) = - ( 𝐴 Yrm 𝑀 ) )
156	1 17 155	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm - 𝑀 ) = - ( 𝐴 Yrm 𝑀 ) )
157	154 156	neeqtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) )
158	118 123 157	3jca	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ 𝐾 ≠ 𝑀 ) → ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) )
159	158	ex	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐾 ≠ 𝑀 → ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) )
160		simplll	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
161	3	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → 𝐾 ∈ ℤ )
162	160 161 30	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Yrm 𝐾 ) ∈ ℤ )
163	162	zcnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Yrm 𝐾 ) ∈ ℂ )
164	16	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → 𝑀 ∈ ℤ )
165	160 164 33	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
166	165	zcnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
167	163 166	negsubd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) = ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) )
168	167	fveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) ) = ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) )
169	166	negcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → - ( 𝐴 Yrm 𝑀 ) ∈ ℂ )
170	163 169	addcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
171	170	abscld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) ) ∈ ℝ )
172	163	abscld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) ∈ ℝ )
173	166	abscld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ∈ ℝ )
174	172 173	readdcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) ∈ ℝ )
175		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
176	175	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
177	176	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → 𝑁 ∈ ℤ )
178	49	nn0zd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
179	160 177 178	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Xrm 𝑁 ) ∈ ℤ )
180	179	zred	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Xrm 𝑁 ) ∈ ℝ )
181	163 169	abstrid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) ) ≤ ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ - ( 𝐴 Yrm 𝑀 ) ) ) )
182		absneg	⊢ ( ( 𝐴 Yrm 𝑀 ) ∈ ℂ → ( abs ‘ - ( 𝐴 Yrm 𝑀 ) ) = ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) )
183	182	eqcomd	⊢ ( ( 𝐴 Yrm 𝑀 ) ∈ ℂ → ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) = ( abs ‘ - ( 𝐴 Yrm 𝑀 ) ) )
184	166 183	syl	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) = ( abs ‘ - ( 𝐴 Yrm 𝑀 ) ) )
185	184	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) = ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ - ( 𝐴 Yrm 𝑀 ) ) ) )
186	181 185	breqtrrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) ) ≤ ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) )
187		simpr1	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) )
188	171 174 180 186 187	lelttrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + - ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) )
189	168 188	eqbrtrrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) )
190	162 165	zsubcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ )
191	190	zcnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
192	191	abscld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) ∈ ℝ )
193	192 180	ltnled	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ↔ ¬ ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) ) )
194	189 193	mpbid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ¬ ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) )
195		simpr2	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) )
196	163 166 195	subne0d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ≠ 0 )
197		dvdsleabs	⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ≠ 0 ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) ) )
198	179 190 196 197	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ) ) )
199	194 198	mtod	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ¬ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) )
200	163 166	subnegd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) = ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) )
201	200	fveq2d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) = ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ) )
202	163 166	addcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
203	202	abscld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ) ∈ ℝ )
204	163 166	abstrid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ) ≤ ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) )
205	203 174 180 204 187	lelttrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) + ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) )
206	201 205	eqbrtrd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) )
207	165	znegcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → - ( 𝐴 Yrm 𝑀 ) ∈ ℤ )
208	162 207	zsubcld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ )
209	208	zcnd	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ∈ ℂ )
210	209	abscld	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ∈ ℝ )
211	210 180	ltnled	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ↔ ¬ ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
212	206 211	mpbid	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ¬ ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
213		simpr3	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) )
214	163 169 213	subne0d	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ≠ 0 )
215		dvdsleabs	⊢ ( ( ( 𝐴 Xrm 𝑁 ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ∈ ℤ ∧ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ≠ 0 ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
216	179 208 214 215	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) → ( 𝐴 Xrm 𝑁 ) ≤ ( abs ‘ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
217	212 216	mtod	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ¬ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) )
218	199 217	jca	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ( ¬ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∧ ¬ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
219		pm4.56	⊢ ( ( ¬ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∧ ¬ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ↔ ¬ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
220	218 219	sylib	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) ∧ ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) ) → ¬ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) )
221	220	ex	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( ( abs ‘ ( 𝐴 Yrm 𝐾 ) ) + ( abs ‘ ( 𝐴 Yrm 𝑀 ) ) ) < ( 𝐴 Xrm 𝑁 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ ( 𝐴 Yrm 𝑀 ) ∧ ( 𝐴 Yrm 𝐾 ) ≠ - ( 𝐴 Yrm 𝑀 ) ) → ¬ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
222	159 221	syld	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐾 ≠ 𝑀 → ¬ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) )
223	222	necon4ad	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) → 𝐾 = 𝑀 ) )
224	223	3impia	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − ( 𝐴 Yrm 𝑀 ) ) ∨ ( 𝐴 Xrm 𝑁 ) ∥ ( ( 𝐴 Yrm 𝐾 ) − - ( 𝐴 Yrm 𝑀 ) ) ) ) → 𝐾 = 𝑀 )