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	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℕ) \land (K \in (0 \dots N) \land M \in (0 \dots N)) \land ((A X_{rm} N) ∥ ((A Y_{rm} K) - (A Y_{rm} M)) \lor (A X_{rm} N) ∥ ((A Y_{rm} K) - (- (A Y_{rm} M))))) \to K = M$

Proof

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

Metamath Proof Explorer

Theorem jm2.26lem3

Proof