Metamath Proof Explorer

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 
|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> K = M )

Proof

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