Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.26lem3 Unicode version

Theorem jm2.26lem3 26417
Description: Lemma for jm2.26 26418. Use acongrep 26390 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
StepHypRef Expression
1 simplll 734 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  A  e.  ( ZZ>= ` 
2 ) )
2 elfzelz 10890 . . . . . . . . . . . 12  |-  ( K  e.  ( 0 ... N )  ->  K  e.  ZZ )
32adantr 451 . . . . . . . . . . 11  |-  ( ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) )  ->  K  e.  ZZ )
43ad2antlr 707 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  K  e.  ZZ )
5 rmyabs 26368 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ )  ->  ( abs `  ( A Yrm  K ) )  =  ( A Yrm  ( abs `  K ) ) )
61, 4, 5syl2anc 642 . . . . . . . . 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
) ) )
73zred 10209 . . . . . . . . . . . 12  |-  ( ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) )  ->  K  e.  RR )
87ad2antlr 707 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  K  e.  RR )
9 elfzle1 10891 . . . . . . . . . . . . 13  |-  ( K  e.  ( 0 ... N )  ->  0  <_  K )
109adantr 451 . . . . . . . . . . . 12  |-  ( ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) )  ->  0  <_  K
)
1110ad2antlr 707 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
0  <_  K )
128, 11absidd 12001 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( abs `  K
)  =  K )
1312oveq2d 5961 . . . . . . . . 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 ) )
146, 13eqtrd 2390 . . . . . . . 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 10890 . . . . . . . . . . . 12  |-  ( M  e.  ( 0 ... N )  ->  M  e.  ZZ )
1615adantl 452 . . . . . . . . . . 11  |-  ( ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) )  ->  M  e.  ZZ )
1716ad2antlr 707 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  M  e.  ZZ )
18 rmyabs 26368 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  M  e.  ZZ )  ->  ( abs `  ( A Yrm  M ) )  =  ( A Yrm  ( abs `  M ) ) )
191, 17, 18syl2anc 642 . . . . . . . . 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
) ) )
2016zred 10209 . . . . . . . . . . . 12  |-  ( ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) )  ->  M  e.  RR )
2120ad2antlr 707 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  M  e.  RR )
22 elfzle1 10891 . . . . . . . . . . . . 13  |-  ( M  e.  ( 0 ... N )  ->  0  <_  M )
2322adantl 452 . . . . . . . . . . . 12  |-  ( ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) )  ->  0  <_  M
)
2423ad2antlr 707 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
0  <_  M )
2521, 24absidd 12001 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( abs `  M
)  =  M )
2625oveq2d 5961 . . . . . . . . 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 ) )
2719, 26eqtrd 2390 . . . . . . . 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 ) )
2814, 27oveq12d 5963 . . . . . . 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 26322 . . . . . . . . . . . 12  |- Yrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> ZZ
3029fovcl 6036 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ )  ->  ( A Yrm 
K )  e.  ZZ )
311, 4, 30syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  K )  e.  ZZ )
3231zred 10209 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  K )  e.  RR )
3329fovcl 6036 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  M  e.  ZZ )  ->  ( A Yrm 
M )  e.  ZZ )
341, 17, 33syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  M )  e.  ZZ )
3534zred 10209 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  M )  e.  RR )
3632, 35readdcld 8952 . . . . . . . 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 735 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  N  e.  NN )
3837nnzd 10208 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  N  e.  ZZ )
39 peano2zm 10154 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
4038, 39syl 15 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( N  -  1 )  e.  ZZ )
4129fovcl 6036 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  ( N  -  1 )  e.  ZZ )  -> 
( A Yrm  ( N  - 
1 ) )  e.  ZZ )
421, 40, 41syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  ( N  - 
1 ) )  e.  ZZ )
4342zred 10209 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  ( N  - 
1 ) )  e.  RR )
4429fovcl 6036 . . . . . . . . . . 11  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  N  e.  ZZ )  ->  ( A Yrm 
N )  e.  ZZ )
451, 38, 44syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  N )  e.  ZZ )
4645zred 10209 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  N )  e.  RR )
4743, 46readdcld 8952 . . . . . . . 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 26321 . . . . . . . . . . 11  |- Xrm  : (
( ZZ>= `  2 )  X.  ZZ ) --> NN0
4948fovcl 6036 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  N  e.  ZZ )  ->  ( A Xrm 
N )  e.  NN0 )
501, 38, 49syl2anc 642 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Xrm  N )  e. 
NN0 )
5150nn0red 10111 . . . . . . . 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 10892 . . . . . . . . . . . 12  |-  ( K  e.  ( 0 ... ( N  -  1 ) )  ->  K  <_  ( N  -  1 ) )
5352adantl 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 ) )
54 lermy 26365 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  ->  ( K  <_  ( N  - 
1 )  <->  ( A Yrm  K
)  <_  ( A Yrm  ( N  -  1 ) ) ) )
551, 4, 40, 54syl3anc 1182 . . . . . . . . . . . 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 ) ) ) )
5655adantr 451 . . . . . . . . . . 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 ) ) ) )
5753, 56mpbid 201 . . . . . . . . . 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 737 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  M  e.  ( 0 ... N ) )
59 elfzle2 10892 . . . . . . . . . . . . 13  |-  ( M  e.  ( 0 ... N )  ->  M  <_  N )
6058, 59syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  M  <_  N )
61 lermy 26365 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <_  N  <->  ( A Yrm  M
)  <_  ( A Yrm  N
) ) )
621, 17, 38, 61syl3anc 1182 . . . . . . . . . . . 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 ) ) )
6360, 62mpbid 201 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  M )  <_ 
( A Yrm  N ) )
6463adantr 451 . . . . . . . . . 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 9346 . . . . . . . . . . . 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 ) ) ) )
6632, 35, 43, 46, 65syl22anc 1183 . . . . . . . . . . 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 ) ) ) )
6766adantr 451 . . . . . . . . . 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 ) ) ) )
6857, 64, 67mp2and 660 . . . . . . . . 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 ) ) )
6931zcnd 10210 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  K )  e.  CC )
7034zcnd 10210 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  M )  e.  CC )
7169, 70addcomd 9104 . . . . . . . . . . 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 ) ) )
7271adantr 451 . . . . . . . . . 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 19 . . . . . . . . . . . . . . . . . . 19  |-  ( K  =/=  M  ->  K  =/=  M )
7473necomd 2604 . . . . . . . . . . . . . . . . . 18  |-  ( K  =/=  M  ->  M  =/=  K )
7574adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( K  =/=  M  /\  K  =  N )  ->  M  =/=  K )
76 simpr 447 . . . . . . . . . . . . . . . . 17  |-  ( ( K  =/=  M  /\  K  =  N )  ->  K  =  N )
7775, 76neeqtrd 2543 . . . . . . . . . . . . . . . 16  |-  ( ( K  =/=  M  /\  K  =  N )  ->  M  =/=  N )
7877neneqd 2537 . . . . . . . . . . . . . . 15  |-  ( ( K  =/=  M  /\  K  =  N )  ->  -.  M  =  N )
7978adantll 694 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  =/= 
M )  /\  K  =  N )  ->  -.  M  =  N )
80 nnnn0 10064 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  N  e.  NN0 )
81 nn0uz 10354 . . . . . . . . . . . . . . . . . 18  |-  NN0  =  ( ZZ>= `  0 )
8280, 81syl6eleq 2448 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  N  e.  ( ZZ>= `  0 )
)
8382adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  N  e.  NN )  ->  N  e.  ( ZZ>= `  0 )
)
8483ad3antrrr 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  =/= 
M )  /\  K  =  N )  ->  N  e.  ( ZZ>= `  0 )
)
85 simprr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  M  e.  ( 0 ... N
) )
8685ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  =/= 
M )  /\  K  =  N )  ->  M  e.  ( 0 ... N
) )
87 fzm1 10954 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( M  e.  ( 0 ... N
)  <->  ( M  e.  ( 0 ... ( N  -  1 ) )  \/  M  =  N ) ) )
8887biimpa 470 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( ZZ>= ` 
0 )  /\  M  e.  ( 0 ... N
) )  ->  ( M  e.  ( 0 ... ( N  - 
1 ) )  \/  M  =  N ) )
8984, 86, 88syl2anc 642 . . . . . . . . . . . . . 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 ) )
90 orel2 372 . . . . . . . . . . . . . 14  |-  ( -.  M  =  N  -> 
( ( M  e.  ( 0 ... ( N  -  1 ) )  \/  M  =  N )  ->  M  e.  ( 0 ... ( N  -  1 ) ) ) )
9179, 89, 90sylc 56 . . . . . . . . . . . . 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 ) ) )
92 elfzle2 10892 . . . . . . . . . . . . 13  |-  ( M  e.  ( 0 ... ( N  -  1 ) )  ->  M  <_  ( N  -  1 ) )
9391, 92syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  =/= 
M )  /\  K  =  N )  ->  M  <_  ( N  -  1 ) )
94 lermy 26365 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  M  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  ->  ( M  <_  ( N  - 
1 )  <->  ( A Yrm  M
)  <_  ( A Yrm  ( N  -  1 ) ) ) )
951, 17, 40, 94syl3anc 1182 . . . . . . . . . . . . 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 ) ) ) )
9695adantr 451 . . . . . . . . . . . 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 ) ) ) )
9793, 96mpbid 201 . . . . . . . . . . 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 ) ) )
98 simplrl 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  K  e.  ( 0 ... N ) )
99 elfzle2 10892 . . . . . . . . . . . . . 14  |-  ( K  e.  ( 0 ... N )  ->  K  <_  N )
10098, 99syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  K  <_  N )
101 lermy 26365 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  <_  N  <->  ( A Yrm  K
)  <_  ( A Yrm  N
) ) )
1021, 4, 38, 101syl3anc 1182 . . . . . . . . . . . . 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 ) ) )
103100, 102mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  K )  <_ 
( A Yrm  N ) )
104103adantr 451 . . . . . . . . . . 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 ) )
105 le2add 9346 . . . . . . . . . . . . 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 ) ) ) )
10635, 32, 43, 46, 105syl22anc 1183 . . . . . . . . . . . 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 ) ) ) )
107106adantr 451 . . . . . . . . . . 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 ) ) ) )
10897, 104, 107mp2and 660 . . . . . . . . . 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 ) ) )
10972, 108eqbrtrd 4124 . . . . . . . . 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 ) ) )
11037nnnn0d 10110 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  N  e.  NN0 )
111110, 81syl6eleq 2448 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  N  e.  ( ZZ>= ` 
0 ) )
112 fzm1 10954 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( K  e.  ( 0 ... N
)  <->  ( K  e.  ( 0 ... ( N  -  1 ) )  \/  K  =  N ) ) )
113112biimpa 470 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
0 )  /\  K  e.  ( 0 ... N
) )  ->  ( K  e.  ( 0 ... ( N  - 
1 ) )  \/  K  =  N ) )
114111, 98, 113syl2anc 642 . . . . . . . . 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 ) )
11568, 109, 114mpjaodan 761 . . . . . . . 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 ) ) )
116 jm2.24 26373 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  N  e.  ZZ )  ->  (
( A Yrm  ( N  - 
1 ) )  +  ( A Yrm  N ) )  <  ( A Xrm  N ) )
1171, 38, 116syl2anc 642 . . . . . . . 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 ) )
11836, 47, 51, 115, 117lelttrd 9064 . . . . . . 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 ) )
11928, 118eqbrtrd 4124 . . . . . 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 ) )
120 simpr 447 . . . . . . 7  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  K  =/=  M )
121 rmyeq 26364 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ  /\  M  e.  ZZ )  ->  ( K  =  M  <->  ( A Yrm  K
)  =  ( A Yrm  M ) ) )
122121necon3bid 2556 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ  /\  M  e.  ZZ )  ->  ( K  =/=  M  <->  ( A Yrm  K
)  =/=  ( A Yrm  M ) ) )
1231, 4, 17, 122syl3anc 1182 . . . . . . 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 ) ) )
124120, 123mpbid 201 . . . . . 6  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  -> 
( A Yrm  K )  =/=  ( A Yrm  M ) )
1257ad2antlr 707 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  K  e.  RR )
126 0re 8928 . . . . . . . . . . . . . 14  |-  0  e.  RR
127126a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  0  e.  RR )
128 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  K  =  -u M )
12922ad2antll 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  0  <_  M )
13020adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  M  e.  RR )
131130le0neg2d 9435 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  (
0  <_  M  <->  -u M  <_ 
0 ) )
132129, 131mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  -u M  <_  0 )
133132adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  -u M  <_  0
)
134128, 133eqbrtrd 4124 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  K  <_  0
)
13510ad2antlr 707 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  0  <_  K
)
136 letri3 8997 . . . . . . . . . . . . . 14  |-  ( ( K  e.  RR  /\  0  e.  RR )  ->  ( K  =  0  <-> 
( K  <_  0  /\  0  <_  K ) ) )
137136biimpar 471 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  RR  /\  0  e.  RR )  /\  ( K  <_ 
0  /\  0  <_  K ) )  ->  K  =  0 )
138125, 127, 134, 135, 137syl22anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  K  =  0 )
139 simpr 447 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  = 
-u M )  /\  K  =  0 )  ->  K  =  0 )
140 simplr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  = 
-u M )  /\  K  =  0 )  ->  K  =  -u M )
141140, 139eqtr3d 2392 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  = 
-u M )  /\  K  =  0 )  ->  -u M  =  0 )
142130recnd 8951 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  M  e.  CC )
143142ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  = 
-u M )  /\  K  =  0 )  ->  M  e.  CC )
144143negeq0d 9239 . . . . . . . . . . . . . 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 ) )
145141, 144mpbird 223 . . . . . . . . . . . . 13  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  = 
-u M )  /\  K  =  0 )  ->  M  =  0 )
146139, 145eqtr4d 2393 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  ( ZZ>= `  2
)  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  /\  K  = 
-u M )  /\  K  =  0 )  ->  K  =  M )
147138, 146mpdan 649 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =  -u M )  ->  K  =  M )
148147ex 423 . . . . . . . . . 10  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  ( K  =  -u M  ->  K  =  M )
)
149148necon3d 2559 . . . . . . . . 9  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  M  e.  ( 0 ... N ) ) )  ->  ( K  =/=  M  ->  K  =/=  -u M ) )
150149imp 418 . . . . . . . 8  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  K  =/=  -u M )
15158, 15syl 15 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  M  e.  ZZ )
152151znegcld 10211 . . . . . . . . 9  |-  ( ( ( ( A  e.  ( ZZ>= `  2 )  /\  N  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  M  e.  ( 0 ... N
) ) )  /\  K  =/=  M )  ->  -u M  e.  ZZ )
153 rmyeq 26364 . . . . . . . . . 10  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ  /\  -u M  e.  ZZ )  ->  ( K  =  -u M  <->  ( A Yrm  K
)  =  ( A Yrm  -u M ) ) )
154153necon3bid 2556 . . . . . . . . 9  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  K  e.  ZZ  /\  -u M  e.  ZZ )  ->  ( K  =/=  -u M  <->  ( A Yrm  K
)  =/=  ( A Yrm  -u M ) ) )
1551, 4, 152, 154syl3anc 1182 . . . . . . . 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 ) ) )
156150, 155mpbid 201 . . . . . . 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 ) )
157 rmyneg 26336 . . . . . . . 8  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  M  e.  ZZ )  ->  ( A Yrm  -u M )  =  -u ( A Yrm  M ) )
1581, 17, 157syl2anc 642 . . . . . . 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 ) )
159156, 158neeqtrd 2543 . . . . . 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 ) )
160119, 124, 1593jca 1132 . . . . 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 ) ) )
161160ex 423 . . . 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 ) ) ) )
162 simplll 734 . . . . . . . . . . . . . 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 )
)
1633ad2antlr 707 . . . . . . . . . . . . . 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 )
164162, 163, 30syl2anc 642 . . . . . . . . . . . . 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 )
165164zcnd 10210 . . . . . . . . . . . 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 )
16616ad2antlr 707 . . . . . . . . . . . . . 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 )
167162, 166, 33syl2anc 642 . . . . . . . . . . . . 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 )
168167zcnd 10210 . . . . . . . . . . . 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 )
169165, 168negsubd 9253 . . . . . . . . . . 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 ) ) )
170169fveq2d 5612 . . . . . . . . . 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 ) ) ) )
171168negcld 9234 . . . . . . . . . . . . 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 )
172165, 171addcld 8944 . . . . . . . . . . . 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 )
173172abscld 12014 . . . . . . . . . . 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 )
174165abscld 12014 . . . . . . . . . . . 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 )
175168abscld 12014 . . . . . . . . . . . 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 )
176174, 175readdcld 8952 . . . . . . . . . . 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 )
177 nnz 10137 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  N  e.  ZZ )
178177adantl 452 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  N  e.  NN )  ->  N  e.  ZZ )
179178ad2antrr 706 . . . . . . . . . . . . 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 )
18049nn0zd 10207 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  N  e.  ZZ )  ->  ( A Xrm 
N )  e.  ZZ )
181162, 179, 180syl2anc 642 . . . . . . . . . . . 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 )
182181zred 10209 . . . . . . . . . . 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 )
183165, 171abstrid 12034 . . . . . . . . . . . 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 ) ) ) )
184 absneg 11858 . . . . . . . . . . . . . . 15  |-  ( ( A Yrm  M )  e.  CC  ->  ( abs `  -u ( A Yrm 
M ) )  =  ( abs `  ( A Yrm 
M ) ) )
185184eqcomd 2363 . . . . . . . . . . . . . 14  |-  ( ( A Yrm  M )  e.  CC  ->  ( abs `  ( A Yrm 
M ) )  =  ( abs `  -u ( A Yrm 
M ) ) )
186168, 185syl 15 . . . . . . . . . . . . 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 ) ) )
187186oveq2d 5961 . . . . . . . . . . . 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 ) ) ) )
188183, 187breqtrrd 4130 . . . . . . . . . . 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 ) ) ) )
189 simpr1 961 . . . . . . . . . . 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 ) )
190173, 176, 182, 188, 189lelttrd 9064 . . . . . . . . . 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 ) )
191170, 190eqbrtrrd 4126 . . . . . . . . 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 ) )
192164, 167zsubcld 10214 . . . . . . . . . . . 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 )
193192zcnd 10210 . . . . . . . . . . 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 )
194193abscld 12014 . . . . . . . . . 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 )
195194, 182ltnled 9056 . . . . . . . . 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 ) ) ) ) )
196191, 195mpbid 201 . . . . . . . 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 ) ) ) )
197 simpr2 962 . . . . . . . . . 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 ) )
198 subeq0 9163 . . . . . . . . . . . 12  |-  ( ( ( A Yrm  K )  e.  CC  /\  ( A Yrm  M )  e.  CC )  ->  ( ( ( A Yrm  K )  -  ( A Yrm 
M ) )  =  0  <->  ( A Yrm  K )  =  ( A Yrm  M ) ) )
199198necon3bid 2556 . . . . . . . . . . 11  |-  ( ( ( A Yrm  K )  e.  CC  /\  ( A Yrm  M )  e.  CC )  ->  ( ( ( A Yrm  K )  -  ( A Yrm 
M ) )  =/=  0  <->  ( A Yrm  K )  =/=  ( A Yrm  M ) ) )
200165, 168, 199syl2anc 642 . . . . . . . . . 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 ) )  =/=  0  <->  ( A Yrm 
K )  =/=  ( A Yrm 
M ) ) )
201197, 200mpbird 223 . . . . . . . . 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 )
202 dvdsleabs 12672 . . . . . . . . 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 ) ) ) ) )
203181, 192, 201, 202syl3anc 1182 . . . . . . . 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 ) ) ) ) )
204196, 203mtod 168 . . . . . . 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 ) ) )
205165, 168subnegd 9254 . . . . . . . . . . 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 ) ) )
206205fveq2d 5612 . . . . . . . . . 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 ) ) ) )
207165, 168addcld 8944 . . . . . . . . . . . 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 )
208207abscld 12014 . . . . . . . . . . 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 )
209165, 168abstrid 12034 . . . . . . . . . . 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 ) ) ) )
210208, 176, 182, 209, 189lelttrd 9064 . . . . . . . . . 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 ) )
211206, 210eqbrtrd 4124 . . . . . . . . 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 ) )
212167znegcld 10211 . . . . . . . . . . . . 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 )
213164, 212zsubcld 10214 . . . . . . . . . . . 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 )
214213zcnd 10210 . . . . . . . . . . 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 )
215214abscld 12014 . . . . . . . . . 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 )
216215, 182ltnled 9056 . . . . . . . . 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 ) ) ) ) )
217211, 216mpbid 201 . . . . . . . 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 ) ) ) )
218 simpr3 963 . . . . . . . . . 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 ) )
219 subeq0 9163 . . . . . . . . . . . 12  |-  ( ( ( A Yrm  K )  e.  CC  /\  -u ( A Yrm 
M )  e.  CC )  ->  ( ( ( A Yrm  K )  -  -u ( A Yrm 
M ) )  =  0  <->  ( A Yrm  K )  =  -u ( A Yrm  M ) ) )
220219necon3bid 2556 . . . . . . . . . . 11  |-  ( ( ( A Yrm  K )  e.  CC  /\  -u ( A Yrm 
M )  e.  CC )  ->  ( ( ( A Yrm  K )  -  -u ( A Yrm 
M ) )  =/=  0  <->  ( A Yrm  K )  =/=  -u ( A Yrm  M ) ) )
221165, 171, 220syl2anc 642 . . . . . . . . . 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 ) )  =/=  0  <->  ( A Yrm 
K )  =/=  -u ( A Yrm 
M ) ) )
222218, 221mpbird 223 . . . . . . . . 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 )
223 dvdsleabs 12672 . . . . . . . . 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 ) ) ) ) )
224181, 213, 222, 223syl3anc 1182 . . . . . . . 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 ) ) ) ) )
225217, 224mtod 168 . . . . . . 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 ) ) )
226204, 225jca 518 . . . . . 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 ) ) ) )
227 pm4.56 481 . . . . . 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 ) ) ) )
228226, 227sylib 188 . . . . 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 ) ) ) )
229228ex 423 . . . 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 ) ) ) ) )
230161, 229syld 40 . . 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 ) ) ) ) )
231230necon4ad 2582 . 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 ) )
2322313impia 1148 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 )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 934    = wceq 1642    e. wcel 1710    =/= wne 2521   class class class wbr 4104   ` cfv 5337  (class class class)co 5945   CCcc 8825   RRcr 8826   0cc0 8827   1c1 8828    + caddc 8830    < clt 8957    <_ cle 8958    - cmin 9127   -ucneg 9128   NNcn 9836   2c2 9885   NN0cn0 10057   ZZcz 10116   ZZ>=cuz 10322   ...cfz 10874   abscabs 11815    || cdivides 12628   Xrm crmx 26308   Yrm crmy 26309
This theorem is referenced by:  jm2.26  26418
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-inf2 7432  ax-cnex 8883  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-mulcom 8891  ax-addass 8892  ax-mulass 8893  ax-distr 8894  ax-i2m1 8895  ax-1ne0 8896  ax-1rid 8897  ax-rnegex 8898  ax-rrecex 8899  ax-cnre 8900  ax-pre-lttri 8901  ax-pre-lttrn 8902  ax-pre-ltadd 8903  ax-pre-mulgt0 8904  ax-pre-sup 8905  ax-addf 8906  ax-mulf 8907
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-int 3944  df-iun 3988  df-iin 3989  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-se 4435  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-isom 5346  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-of 6165  df-1st 6209  df-2nd 6210  df-riota 6391  df-recs 6475  df-rdg 6510  df-1o 6566  df-2o 6567  df-oadd 6570  df-omul 6571  df-er 6747  df-map 6862  df-pm 6863  df-ixp 6906  df-en 6952  df-dom 6953  df-sdom 6954  df-fin 6955  df-fi 7255  df-sup 7284  df-oi 7315  df-card 7662  df-acn 7665  df-cda 7884  df-pnf 8959  df-mnf 8960  df-xr 8961  df-ltxr 8962  df-le 8963  df-sub 9129  df-neg 9130  df-div 9514  df-nn 9837  df-2 9894  df-3 9895  df-4 9896  df-5 9897  df-6 9898  df-7 9899  df-8 9900  df-9 9901  df-10 9902  df-n0 10058  df-z 10117  df-dec 10217  df-uz 10323  df-q 10409  df-rp 10447  df-xneg 10544  df-xadd 10545  df-xmul 10546  df-ioo 10752  df-ioc 10753  df-ico 10754  df-icc 10755  df-fz 10875  df-fzo 10963  df-fl 11017  df-mod 11066  df-seq 11139  df-exp 11198  df-fac 11382  df-bc 11409  df-hash 11431  df-shft 11658  df-cj 11680  df-re 11681  df-im 11682  df-sqr 11816  df-abs 11817  df-limsup 12041  df-clim 12058  df-rlim 12059  df-sum 12256  df-ef 12446  df-sin 12448  df-cos 12449  df-pi 12451  df-dvds 12629  df-gcd 12783  df-numer 12903  df-denom 12904  df-struct 13247  df-ndx 13248  df-slot 13249  df-base 13250  df-sets 13251  df-ress 13252  df-plusg 13318  df-mulr 13319  df-starv 13320  df-sca 13321  df-vsca 13322  df-tset 13324  df-ple 13325  df-ds 13327  df-unif 13328  df-hom 13329  df-cco 13330  df-rest 13426  df-topn 13427  df-topgen 13443  df-pt 13444  df-prds 13447  df-xrs 13502  df-0g 13503  df-gsum 13504  df-qtop 13509  df-imas 13510  df-xps 13512  df-mre 13587  df-mrc 13588  df-acs 13590  df-mnd 14466  df-submnd 14515  df-mulg 14591  df-cntz 14892  df-cmn 15190  df-xmet 16475  df-met 16476  df-bl 16477  df-mopn 16478  df-fbas 16479  df-fg 16480  df-cnfld 16483  df-top 16742  df-bases 16744  df-topon 16745  df-topsp 16746  df-cld 16862  df-ntr 16863  df-cls 16864  df-nei 16941  df-lp 16974  df-perf 16975  df-cn 17063  df-cnp 17064  df-haus 17149  df-tx 17363  df-hmeo 17552  df-fil 17643  df-fm 17735  df-flim 17736  df-flf 17737  df-xms 17987  df-ms 17988  df-tms 17989  df-cncf 18485  df-limc 19320  df-dv 19321  df-log 20021  df-squarenn 26249  df-pell1qr 26250  df-pell14qr 26251  df-pell1234qr 26252  df-pellfund 26253  df-rmx 26310  df-rmy 26311
  Copyright terms: Public domain W3C validator