Theorem jm2.26lem3 26962

Description: Lemma for jm2.26 26963. Use acongrep 26935 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.)

Assertion

Ref	Expression
jm2.26lem3	|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) /\ ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) -> K = M )

Proof of Theorem jm2.26lem3

Step	Hyp	Ref	Expression
1		simplll 735	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> A e. ( ZZ>= ` 2 ) )
2		elfzelz 11015	. . . . . . . . . . . 12 |- ( K e. ( 0 ... N ) -> K e. ZZ )
3	2	adantr 452	. . . . . . . . . . 11 |- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> K e. ZZ )
4	3	ad2antlr 708	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> K e. ZZ )
5		rmyabs 26913	. . . . . . . . . 10 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( abs ` ( A Yrm K ) ) = ( A Yrm ( abs ` K ) ) )
6	1, 4, 5	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( abs ` ( A Yrm K ) ) = ( A Yrm ( abs ` K ) ) )
7	3	zred 10331	. . . . . . . . . . . 12 |- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> K e. RR )
8	7	ad2antlr 708	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> K e. RR )
9		elfzle1 11016	. . . . . . . . . . . . 13 |- ( K e. ( 0 ... N ) -> 0 <_ K )
10	9	adantr 452	. . . . . . . . . . . 12 |- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> 0 <_ K )
11	10	ad2antlr 708	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> 0 <_ K )
12	8, 11	absidd 12180	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( abs ` K ) = K )
13	12	oveq2d 6056	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm ( abs ` K ) ) = ( A Yrm K ) )
14	6, 13	eqtrd 2436	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( abs ` ( A Yrm K ) ) = ( A Yrm K ) )
15		elfzelz 11015	. . . . . . . . . . . 12 |- ( M e. ( 0 ... N ) -> M e. ZZ )
16	15	adantl 453	. . . . . . . . . . 11 |- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> M e. ZZ )
17	16	ad2antlr 708	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> M e. ZZ )
18		rmyabs 26913	. . . . . . . . . 10 |- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( abs ` ( A Yrm M ) ) = ( A Yrm ( abs ` M ) ) )
19	1, 17, 18	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( abs ` ( A Yrm M ) ) = ( A Yrm ( abs ` M ) ) )
20	16	zred 10331	. . . . . . . . . . . 12 |- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> M e. RR )
21	20	ad2antlr 708	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> M e. RR )
22		elfzle1 11016	. . . . . . . . . . . . 13 |- ( M e. ( 0 ... N ) -> 0 <_ M )
23	22	adantl 453	. . . . . . . . . . . 12 |- ( ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) -> 0 <_ M )
24	23	ad2antlr 708	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> 0 <_ M )
25	21, 24	absidd 12180	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( abs ` M ) = M )
26	25	oveq2d 6056	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm ( abs ` M ) ) = ( A Yrm M ) )
27	19, 26	eqtrd 2436	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( abs ` ( A Yrm M ) ) = ( A Yrm M ) )
28	14, 27	oveq12d 6058	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) = ( ( A Yrm K ) + ( A Yrm M ) ) )
29		frmy 26867	. . . . . . . . . . . 12 |- Yrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
30	29	fovcl 6134	. . . . . . . . . . 11 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( A Yrm K ) e. ZZ )
31	1, 4, 30	syl2anc 643	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) e. ZZ )
32	31	zred 10331	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) e. RR )
33	29	fovcl 6134	. . . . . . . . . . 11 |- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A Yrm M ) e. ZZ )
34	1, 17, 33	syl2anc 643	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm M ) e. ZZ )
35	34	zred 10331	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm M ) e. RR )
36	32, 35	readdcld 9071	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( A Yrm K ) + ( A Yrm M ) ) e. RR )
37		simpllr 736	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> N e. NN )
38	37	nnzd 10330	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> N e. ZZ )
39		peano2zm 10276	. . . . . . . . . . . 12 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )
40	38, 39	syl 16	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( N - 1 ) e. ZZ )
41	29	fovcl 6134	. . . . . . . . . . 11 |- ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A Yrm ( N - 1 ) ) e. ZZ )
42	1, 40, 41	syl2anc 643	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm ( N - 1 ) ) e. ZZ )
43	42	zred 10331	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm ( N - 1 ) ) e. RR )
44	29	fovcl 6134	. . . . . . . . . . 11 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm N ) e. ZZ )
45	1, 38, 44	syl2anc 643	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm N ) e. ZZ )
46	45	zred 10331	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm N ) e. RR )
47	43, 46	readdcld 9071	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) e. RR )
48		frmx 26866	. . . . . . . . . . 11 |- Xrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
49	48	fovcl 6134	. . . . . . . . . 10 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm N ) e. NN0 )
50	1, 38, 49	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Xrm N ) e. NN0 )
51	50	nn0red 10231	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Xrm N ) e. RR )
52		elfzle2 11017	. . . . . . . . . . . 12 |- ( K e. ( 0 ... ( N - 1 ) ) -> K <_ ( N - 1 ) )
53	52	adantl 453	. . . . . . . . . . 11 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K e. ( 0 ... ( N - 1 ) ) ) -> K <_ ( N - 1 ) )
54		lermy 26910	. . . . . . . . . . . . 13 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( K <_ ( N - 1 ) <-> ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) ) )
55	1, 4, 40, 54	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( K <_ ( N - 1 ) <-> ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) ) )
56	55	adantr 452	. . . . . . . . . . 11 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( K <_ ( N - 1 ) <-> ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) ) )
57	53, 56	mpbid 202	. . . . . . . . . 10 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) )
58		simplrr 738	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> M e. ( 0 ... N ) )
59		elfzle2 11017	. . . . . . . . . . . . 13 |- ( M e. ( 0 ... N ) -> M <_ N )
60	58, 59	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> M <_ N )
61		lermy 26910	. . . . . . . . . . . . 13 |- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( A Yrm M ) <_ ( A Yrm N ) ) )
62	1, 17, 38, 61	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( M <_ N <-> ( A Yrm M ) <_ ( A Yrm N ) ) )
63	60, 62	mpbid 202	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm M ) <_ ( A Yrm N ) )
64	63	adantr 452	. . . . . . . . . 10 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( A Yrm M ) <_ ( A Yrm N ) )
65		le2add 9466	. . . . . . . . . . . 12 |- ( ( ( ( A Yrm K ) e. RR /\ ( A Yrm M ) e. RR ) /\ ( ( A Yrm ( N - 1 ) ) e. RR /\ ( A Yrm N ) e. RR ) ) -> ( ( ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) /\ ( A Yrm M ) <_ ( A Yrm N ) ) -> ( ( A Yrm K ) + ( A Yrm M ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) ) )
66	32, 35, 43, 46, 65	syl22anc 1185	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) /\ ( A Yrm M ) <_ ( A Yrm N ) ) -> ( ( A Yrm K ) + ( A Yrm M ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) ) )
67	66	adantr 452	. . . . . . . . . 10 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( A Yrm K ) <_ ( A Yrm ( N - 1 ) ) /\ ( A Yrm M ) <_ ( A Yrm N ) ) -> ( ( A Yrm K ) + ( A Yrm M ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) ) )
68	57, 64, 67	mp2and 661	. . . . . . . . 9 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( ( A Yrm K ) + ( A Yrm M ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) )
69	31	zcnd 10332	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) e. CC )
70	34	zcnd 10332	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm M ) e. CC )
71	69, 70	addcomd 9224	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( A Yrm K ) + ( A Yrm M ) ) = ( ( A Yrm M ) + ( A Yrm K ) ) )
72	71	adantr 452	. . . . . . . . . 10 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( ( A Yrm K ) + ( A Yrm M ) ) = ( ( A Yrm M ) + ( A Yrm K ) ) )
73		id 20	. . . . . . . . . . . . . . . . . . 19 |- ( K =/= M -> K =/= M )
74	73	necomd 2650	. . . . . . . . . . . . . . . . . 18 |- ( K =/= M -> M =/= K )
75	74	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( K =/= M /\ K = N ) -> M =/= K )
76		simpr 448	. . . . . . . . . . . . . . . . 17 |- ( ( K =/= M /\ K = N ) -> K = N )
77	75, 76	neeqtrd 2589	. . . . . . . . . . . . . . . 16 |- ( ( K =/= M /\ K = N ) -> M =/= N )
78	77	neneqd 2583	. . . . . . . . . . . . . . 15 |- ( ( K =/= M /\ K = N ) -> -. M = N )
79	78	adantll 695	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> -. M = N )
80		nnnn0 10184	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> N e. NN0 )
81		nn0uz 10476	. . . . . . . . . . . . . . . . 17 |- NN0 = ( ZZ>= ` 0 )
82	80, 81	syl6eleq 2494	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> N e. ( ZZ>= ` 0 ) )
83	82	ad4antlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> N e. ( ZZ>= ` 0 ) )
84		simprr 734	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> M e. ( 0 ... N ) )
85	84	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> M e. ( 0 ... N ) )
86		fzm1 11082	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 0 ) -> ( M e. ( 0 ... N ) <-> ( M e. ( 0 ... ( N - 1 ) ) \/ M = N ) ) )
87	86	biimpa 471	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 0 ) /\ M e. ( 0 ... N ) ) -> ( M e. ( 0 ... ( N - 1 ) ) \/ M = N ) )
88	83, 85, 87	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( M e. ( 0 ... ( N - 1 ) ) \/ M = N ) )
89		orel2 373	. . . . . . . . . . . . . 14 |- ( -. M = N -> ( ( M e. ( 0 ... ( N - 1 ) ) \/ M = N ) -> M e. ( 0 ... ( N - 1 ) ) ) )
90	79, 88, 89	sylc 58	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> M e. ( 0 ... ( N - 1 ) ) )
91		elfzle2 11017	. . . . . . . . . . . . 13 |- ( M e. ( 0 ... ( N - 1 ) ) -> M <_ ( N - 1 ) )
92	90, 91	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> M <_ ( N - 1 ) )
93		lermy 26910	. . . . . . . . . . . . . 14 |- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( M <_ ( N - 1 ) <-> ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) ) )
94	1, 17, 40, 93	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( M <_ ( N - 1 ) <-> ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) ) )
95	94	adantr 452	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( M <_ ( N - 1 ) <-> ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) ) )
96	92, 95	mpbid 202	. . . . . . . . . . 11 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) )
97		simplrl 737	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> K e. ( 0 ... N ) )
98		elfzle2 11017	. . . . . . . . . . . . . 14 |- ( K e. ( 0 ... N ) -> K <_ N )
99	97, 98	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> K <_ N )
100		lermy 26910	. . . . . . . . . . . . . 14 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ /\ N e. ZZ ) -> ( K <_ N <-> ( A Yrm K ) <_ ( A Yrm N ) ) )
101	1, 4, 38, 100	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( K <_ N <-> ( A Yrm K ) <_ ( A Yrm N ) ) )
102	99, 101	mpbid 202	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) <_ ( A Yrm N ) )
103	102	adantr 452	. . . . . . . . . . 11 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( A Yrm K ) <_ ( A Yrm N ) )
104		le2add 9466	. . . . . . . . . . . . 13 |- ( ( ( ( A Yrm M ) e. RR /\ ( A Yrm K ) e. RR ) /\ ( ( A Yrm ( N - 1 ) ) e. RR /\ ( A Yrm N ) e. RR ) ) -> ( ( ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) /\ ( A Yrm K ) <_ ( A Yrm N ) ) -> ( ( A Yrm M ) + ( A Yrm K ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) ) )
105	35, 32, 43, 46, 104	syl22anc 1185	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) /\ ( A Yrm K ) <_ ( A Yrm N ) ) -> ( ( A Yrm M ) + ( A Yrm K ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) ) )
106	105	adantr 452	. . . . . . . . . . 11 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( ( ( A Yrm M ) <_ ( A Yrm ( N - 1 ) ) /\ ( A Yrm K ) <_ ( A Yrm N ) ) -> ( ( A Yrm M ) + ( A Yrm K ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) ) )
107	96, 103, 106	mp2and 661	. . . . . . . . . 10 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( ( A Yrm M ) + ( A Yrm K ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) )
108	72, 107	eqbrtrd 4192	. . . . . . . . 9 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) /\ K = N ) -> ( ( A Yrm K ) + ( A Yrm M ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) )
109	37	nnnn0d 10230	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> N e. NN0 )
110	109, 81	syl6eleq 2494	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> N e. ( ZZ>= ` 0 ) )
111		fzm1 11082	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 0 ) -> ( K e. ( 0 ... N ) <-> ( K e. ( 0 ... ( N - 1 ) ) \/ K = N ) ) )
112	111	biimpa 471	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 0 ) /\ K e. ( 0 ... N ) ) -> ( K e. ( 0 ... ( N - 1 ) ) \/ K = N ) )
113	110, 97, 112	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( K e. ( 0 ... ( N - 1 ) ) \/ K = N ) )
114	68, 108, 113	mpjaodan 762	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( A Yrm K ) + ( A Yrm M ) ) <_ ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) )
115		jm2.24 26918	. . . . . . . . 9 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) < ( A Xrm N ) )
116	1, 38, 115	syl2anc 643	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) < ( A Xrm N ) )
117	36, 47, 51, 114, 116	lelttrd 9184	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( A Yrm K ) + ( A Yrm M ) ) < ( A Xrm N ) )
118	28, 117	eqbrtrd 4192	. . . . . 6 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) )
119		simpr 448	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> K =/= M )
120		rmyeq 26909	. . . . . . . . 9 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ /\ M e. ZZ ) -> ( K = M <-> ( A Yrm K ) = ( A Yrm M ) ) )
121	120	necon3bid 2602	. . . . . . . 8 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ /\ M e. ZZ ) -> ( K =/= M <-> ( A Yrm K ) =/= ( A Yrm M ) ) )
122	1, 4, 17, 121	syl3anc 1184	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( K =/= M <-> ( A Yrm K ) =/= ( A Yrm M ) ) )
123	119, 122	mpbid 202	. . . . . 6 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) =/= ( A Yrm M ) )
124	7	ad2antlr 708	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> K e. RR )
125		0re 9047	. . . . . . . . . . . . . 14 |- 0 e. RR
126	125	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> 0 e. RR )
127		simpr 448	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> K = -u M )
128	22	ad2antll 710	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> 0 <_ M )
129	20	adantl 453	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> M e. RR )
130	129	le0neg2d 9555	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( 0 <_ M <-> -u M <_ 0 ) )
131	128, 130	mpbid 202	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> -u M <_ 0 )
132	131	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> -u M <_ 0 )
133	127, 132	eqbrtrd 4192	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> K <_ 0 )
134	10	ad2antlr 708	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> 0 <_ K )
135		letri3 9116	. . . . . . . . . . . . . 14 |- ( ( K e. RR /\ 0 e. RR ) -> ( K = 0 <-> ( K <_ 0 /\ 0 <_ K ) ) )
136	135	biimpar 472	. . . . . . . . . . . . 13 |- ( ( ( K e. RR /\ 0 e. RR ) /\ ( K <_ 0 /\ 0 <_ K ) ) -> K = 0 )
137	124, 126, 133, 134, 136	syl22anc 1185	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> K = 0 )
138		simpr 448	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> K = 0 )
139		simplr 732	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> K = -u M )
140	139, 138	eqtr3d 2438	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> -u M = 0 )
141	129	recnd 9070	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> M e. CC )
142	141	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> M e. CC )
143	142	negeq0d 9359	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> ( M = 0 <-> -u M = 0 ) )
144	140, 143	mpbird 224	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> M = 0 )
145	138, 144	eqtr4d 2439	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) /\ K = 0 ) -> K = M )
146	137, 145	mpdan 650	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K = -u M ) -> K = M )
147	146	ex 424	. . . . . . . . . 10 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( K = -u M -> K = M ) )
148	147	necon3d 2605	. . . . . . . . 9 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( K =/= M -> K =/= -u M ) )
149	148	imp 419	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> K =/= -u M )
150	58, 15	syl 16	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> M e. ZZ )
151	150	znegcld 10333	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> -u M e. ZZ )
152		rmyeq 26909	. . . . . . . . . 10 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ /\ -u M e. ZZ ) -> ( K = -u M <-> ( A Yrm K ) = ( A Yrm -u M ) ) )
153	152	necon3bid 2602	. . . . . . . . 9 |- ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ /\ -u M e. ZZ ) -> ( K =/= -u M <-> ( A Yrm K ) =/= ( A Yrm -u M ) ) )
154	1, 4, 151, 153	syl3anc 1184	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( K =/= -u M <-> ( A Yrm K ) =/= ( A Yrm -u M ) ) )
155	149, 154	mpbid 202	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) =/= ( A Yrm -u M ) )
156		rmyneg 26881	. . . . . . . 8 |- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A Yrm -u M ) = -u ( A Yrm M ) )
157	1, 17, 156	syl2anc 643	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm -u M ) = -u ( A Yrm M ) )
158	155, 157	neeqtrd 2589	. . . . . 6 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( A Yrm K ) =/= -u ( A Yrm M ) )
159	118, 123, 158	3jca 1134	. . . . 5 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ K =/= M ) -> ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) )
160	159	ex 424	. . . 4 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( K =/= M -> ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) )
161		simplll 735	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> A e. ( ZZ>= ` 2 ) )
162	3	ad2antlr 708	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> K e. ZZ )
163	161, 162, 30	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Yrm K ) e. ZZ )
164	163	zcnd 10332	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Yrm K ) e. CC )
165	16	ad2antlr 708	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> M e. ZZ )
166	161, 165, 33	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Yrm M ) e. ZZ )
167	166	zcnd 10332	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Yrm M ) e. CC )
168	164, 167	negsubd 9373	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) + -u ( A Yrm M ) ) = ( ( A Yrm K ) - ( A Yrm M ) ) )
169	168	fveq2d 5691	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + -u ( A Yrm M ) ) ) = ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) )
170	167	negcld 9354	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -u ( A Yrm M ) e. CC )
171	164, 170	addcld 9063	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) + -u ( A Yrm M ) ) e. CC )
172	171	abscld 12193	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + -u ( A Yrm M ) ) ) e. RR )
173	164	abscld 12193	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( A Yrm K ) ) e. RR )
174	167	abscld 12193	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( A Yrm M ) ) e. RR )
175	173, 174	readdcld 9071	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) e. RR )
176		nnz 10259	. . . . . . . . . . . . . . 15 |- ( N e. NN -> N e. ZZ )
177	176	adantl 453	. . . . . . . . . . . . . 14 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. ZZ )
178	177	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> N e. ZZ )
179	49	nn0zd 10329	. . . . . . . . . . . . 13 |- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm N ) e. ZZ )
180	161, 178, 179	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Xrm N ) e. ZZ )
181	180	zred 10331	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Xrm N ) e. RR )
182	164, 170	abstrid 12213	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + -u ( A Yrm M ) ) ) <_ ( ( abs ` ( A Yrm K ) ) + ( abs ` -u ( A Yrm M ) ) ) )
183		absneg 12037	. . . . . . . . . . . . . . 15 |- ( ( A Yrm M ) e. CC -> ( abs ` -u ( A Yrm M ) ) = ( abs ` ( A Yrm M ) ) )
184	183	eqcomd 2409	. . . . . . . . . . . . . 14 |- ( ( A Yrm M ) e. CC -> ( abs ` ( A Yrm M ) ) = ( abs ` -u ( A Yrm M ) ) )
185	167, 184	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( A Yrm M ) ) = ( abs ` -u ( A Yrm M ) ) )
186	185	oveq2d 6056	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) = ( ( abs ` ( A Yrm K ) ) + ( abs ` -u ( A Yrm M ) ) ) )
187	182, 186	breqtrrd 4198	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + -u ( A Yrm M ) ) ) <_ ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) )
188		simpr1 963	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) )
189	172, 175, 181, 187, 188	lelttrd 9184	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + -u ( A Yrm M ) ) ) < ( A Xrm N ) )
190	169, 189	eqbrtrrd 4194	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) < ( A Xrm N ) )
191	163, 166	zsubcld 10336	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - ( A Yrm M ) ) e. ZZ )
192	191	zcnd 10332	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - ( A Yrm M ) ) e. CC )
193	192	abscld 12193	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) e. RR )
194	193, 181	ltnled 9176	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) < ( A Xrm N ) <-> -. ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) ) )
195	190, 194	mpbid 202	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -. ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) )
196		simpr2 964	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Yrm K ) =/= ( A Yrm M ) )
197	164, 167, 196	subne0d 9376	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - ( A Yrm M ) ) =/= 0 )
198		dvdsleabs 12851	. . . . . . . . 9 |- ( ( ( A Xrm N ) e. ZZ /\ ( ( A Yrm K ) - ( A Yrm M ) ) e. ZZ /\ ( ( A Yrm K ) - ( A Yrm M ) ) =/= 0 ) -> ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) -> ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) ) )
199	180, 191, 197, 198	syl3anc 1184	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) -> ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - ( A Yrm M ) ) ) ) )
200	195, 199	mtod 170	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -. ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) )
201	164, 167	subnegd 9374	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - -u ( A Yrm M ) ) = ( ( A Yrm K ) + ( A Yrm M ) ) )
202	201	fveq2d 5691	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) = ( abs ` ( ( A Yrm K ) + ( A Yrm M ) ) ) )
203	164, 167	addcld 9063	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) + ( A Yrm M ) ) e. CC )
204	203	abscld 12193	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + ( A Yrm M ) ) ) e. RR )
205	164, 167	abstrid 12213	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + ( A Yrm M ) ) ) <_ ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) )
206	204, 175, 181, 205, 188	lelttrd 9184	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) + ( A Yrm M ) ) ) < ( A Xrm N ) )
207	202, 206	eqbrtrd 4192	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) < ( A Xrm N ) )
208	166	znegcld 10333	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -u ( A Yrm M ) e. ZZ )
209	163, 208	zsubcld 10336	. . . . . . . . . . . 12 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - -u ( A Yrm M ) ) e. ZZ )
210	209	zcnd 10332	. . . . . . . . . . 11 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - -u ( A Yrm M ) ) e. CC )
211	210	abscld 12193	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) e. RR )
212	211, 181	ltnled 9176	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) < ( A Xrm N ) <-> -. ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) )
213	207, 212	mpbid 202	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -. ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) )
214		simpr3 965	. . . . . . . . . 10 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( A Yrm K ) =/= -u ( A Yrm M ) )
215	164, 170, 214	subne0d 9376	. . . . . . . . 9 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Yrm K ) - -u ( A Yrm M ) ) =/= 0 )
216		dvdsleabs 12851	. . . . . . . . 9 |- ( ( ( A Xrm N ) e. ZZ /\ ( ( A Yrm K ) - -u ( A Yrm M ) ) e. ZZ /\ ( ( A Yrm K ) - -u ( A Yrm M ) ) =/= 0 ) -> ( ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) -> ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) )
217	180, 209, 215, 216	syl3anc 1184	. . . . . . . 8 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) -> ( A Xrm N ) <_ ( abs ` ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) )
218	213, 217	mtod 170	. . . . . . 7 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -. ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) )
219	200, 218	jca 519	. . . . . 6 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> ( -. ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) /\ -. ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) )
220		pm4.56 482	. . . . . 6 |- ( ( -. ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) /\ -. ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) <-> -. ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) )
221	219, 220	sylib 189	. . . . 5 |- ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) /\ ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) ) -> -. ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) )
222	221	ex 424	. . . 4 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( ( ( ( abs ` ( A Yrm K ) ) + ( abs ` ( A Yrm M ) ) ) < ( A Xrm N ) /\ ( A Yrm K ) =/= ( A Yrm M ) /\ ( A Yrm K ) =/= -u ( A Yrm M ) ) -> -. ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) )
223	160, 222	syld 42	. . 3 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( K =/= M -> -. ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) )
224	223	necon4ad 2628	. 2 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) ) -> ( ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) -> K = M ) )
225	224	3impia 1150	1 |- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) /\ ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) -> K = M )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   class class class wbr 4172   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   < clt 9076   <_ cle 9077   - cmin 9247   -ucneg 9248   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   ...cfz 10999   abscabs 11994   || cdivides 12807   X_rm crmx 26853   Y_rm crmy 26854

This theorem is referenced by:  jm2.26  26963

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-omul 6688  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-acn 7785  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ioc 10877  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-shft 11837  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-ef 12625  df-sin 12627  df-cos 12628  df-pi 12630  df-dvds 12808  df-gcd 12962  df-numer 13082  df-denom 13083  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-fbas 16654  df-fg 16655  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-lp 17155  df-perf 17156  df-cn 17245  df-cnp 17246  df-haus 17333  df-tx 17547  df-hmeo 17740  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-limc 19706  df-dv 19707  df-log 20407  df-squarenn 26794  df-pell1qr 26795  df-pell14qr 26796  df-pell1234qr 26797  df-pellfund 26798  df-rmx 26855  df-rmy 26856