MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntpbnd1 Unicode version

Theorem pntpbnd1 20735
Description: Lemma for pntpbnd 20737. (Contributed by Mario Carneiro, 11-Apr-2016.)
Hypotheses
Ref Expression
pntpbnd.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
pntpbnd1.e  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
pntpbnd1.x  |-  X  =  ( exp `  (
2  /  E ) )
pntpbnd1.y  |-  ( ph  ->  Y  e.  ( X (,)  +oo ) )
pntpbnd1.1  |-  ( ph  ->  A  e.  RR+ )
pntpbnd1.2  |-  ( ph  ->  A. i  e.  NN  A. j  e.  ZZ  ( abs `  sum_ y  e.  ( i ... j ) ( ( R `  y )  /  (
y  x.  ( y  +  1 ) ) ) )  <_  A
)
pntpbnd1.c  |-  C  =  ( A  +  2 )
pntpbnd1.k  |-  ( ph  ->  K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo ) )
pntpbnd1.3  |-  ( ph  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
Assertion
Ref Expression
pntpbnd1  |-  ( ph  -> 
sum_ n  e.  (
( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  <_  A )
Distinct variable groups:    i, j, n, y, K    ph, n    R, i, j, n, y    i,
a, j, n, y, A    n, E, y   
i, Y, j, n, y
Allowed substitution hints:    ph( y, i, j, a)    C( y, i, j, n, a)    R( a)    E( i, j, a)    K( a)    X( y, i, j, n, a)    Y( a)

Proof of Theorem pntpbnd1
Dummy variables  m  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 11035 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )  e.  Fin )
2 ioossre 10712 . . . . . . . . . . . . . 14  |-  ( X (,)  +oo )  C_  RR
3 pntpbnd1.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  ( X (,)  +oo ) )
42, 3sseldi 3178 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
5 0re 8838 . . . . . . . . . . . . . . 15  |-  0  e.  RR
65a1i 10 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  RR )
7 pntpbnd1.x . . . . . . . . . . . . . . . 16  |-  X  =  ( exp `  (
2  /  E ) )
8 2re 9815 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
9 ioossre 10712 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) 1 )  C_  RR
10 pntpbnd1.e . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
119, 10sseldi 3178 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E  e.  RR )
12 eliooord 10710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
1310, 12syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
1413simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  E )
1511, 14elrpd 10388 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR+ )
16 rerpdivcl 10381 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  E  e.  RR+ )  -> 
( 2  /  E
)  e.  RR )
178, 15, 16sylancr 644 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2  /  E
)  e.  RR )
1817reefcld 12369 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  (
2  /  E ) )  e.  RR )
197, 18syl5eqel 2367 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
20 efgt0 12383 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  /  E )  e.  RR  ->  0  <  ( exp `  (
2  /  E ) ) )
2117, 20syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( exp `  ( 2  /  E
) ) )
2221, 7syl6breqr 4063 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  X )
23 eliooord 10710 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,)  +oo )  ->  ( X  <  Y  /\  Y  <  +oo ) )
243, 23syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  <  +oo )
)
2524simpld 445 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
266, 19, 4, 22, 25lttrd 8977 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  Y )
276, 4, 26ltled 8967 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  Y )
28 flge0nn0 10948 . . . . . . . . . . . . 13  |-  ( ( Y  e.  RR  /\  0  <_  Y )  -> 
( |_ `  Y
)  e.  NN0 )
294, 27, 28syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  Y
)  e.  NN0 )
30 nn0p1nn 10003 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  NN0  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
3129, 30syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
32 elfzuz 10794 . . . . . . . . . . 11  |-  ( n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
33 nnuz 10263 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
3433uztrn2 10245 . . . . . . . . . . 11  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  n  e.  NN )
3531, 32, 34syl2an 463 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  NN )
3635nnrpd 10389 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  RR+ )
37 pntpbnd.r . . . . . . . . . . 11  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
3837pntrf 20712 . . . . . . . . . 10  |-  R : RR+
--> RR
3938ffvelrni 5664 . . . . . . . . 9  |-  ( n  e.  RR+  ->  ( R `
 n )  e.  RR )
4036, 39syl 15 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  RR )
4135peano2nnd 9763 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  +  1 )  e.  NN )
4235, 41nnmulcld 9793 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
4340, 42nndivred 9794 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  e.  RR )
4443adantlr 695 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  RR )
451, 44fsumrecl 12207 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  ->  sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) )  e.  RR )
4640adantlr 695 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  e.  RR )
47 fveq2 5525 . . . . . . . . . 10  |-  ( i  =  n  ->  ( R `  i )  =  ( R `  n ) )
4847breq2d 4035 . . . . . . . . 9  |-  ( i  =  n  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  n ) ) )
4948rspccva 2883 . . . . . . . 8  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  0  <_  ( R `  n ) )
5049adantll 694 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( R `  n )
)
5142adantlr 695 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
5251nnred 9761 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  RR )
5351nngt0d 9789 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <  (
n  x.  ( n  +  1 ) ) )
54 divge0 9625 . . . . . . 7  |-  ( ( ( ( R `  n )  e.  RR  /\  0  <_  ( R `  n ) )  /\  ( ( n  x.  ( n  +  1 ) )  e.  RR  /\  0  <  ( n  x.  ( n  + 
1 ) ) ) )  ->  0  <_  ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
5546, 50, 52, 53, 54syl22anc 1183 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
561, 44, 55fsumge0 12253 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
0  <_  sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
5745, 56absidd 11905 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
5844, 55absidd 11905 . . . . 5  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  =  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )
5958sumeq2dv 12176 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  ->  sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( abs `  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
6057, 59eqtr4d 2318 . . 3  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
61 fzfid 11035 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  e.  Fin )
6243adantlr 695 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  RR )
6362recnd 8861 . . . . 5  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  CC )
6461, 63fsumneg 12249 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) )
-u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  =  -u sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
6540adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  e.  RR )
6665renegcld 9210 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  -u ( R `  n )  e.  RR )
6747breq1d 4033 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( R `  i
)  <_  0  <->  ( R `  n )  <_  0
) )
6867rspccva 2883 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( R `  i
)  <_  0  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6968adantll 694 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
7065le0neg1d 9344 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  <_ 
0  <->  0  <_  -u ( R `  n )
) )
7169, 70mpbid 201 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  -u ( R `  n )
)
7242adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
7372nnred 9761 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  RR )
7472nngt0d 9789 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <  (
n  x.  ( n  +  1 ) ) )
75 divge0 9625 . . . . . . . . 9  |-  ( ( ( -u ( R `
 n )  e.  RR  /\  0  <_  -u ( R `  n
) )  /\  (
( n  x.  (
n  +  1 ) )  e.  RR  /\  0  <  ( n  x.  ( n  +  1 ) ) ) )  ->  0  <_  ( -u ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
7666, 71, 73, 74, 75syl22anc 1183 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( -u ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
7740recnd 8861 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  CC )
7842nncnd 9762 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  CC )
7942nnne0d 9790 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  =/=  0
)
8077, 78, 79divnegd 9549 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -u ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  =  ( -u ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
8180adantlr 695 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  -u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  =  (
-u ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
8276, 81breqtrrd 4049 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  -u (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
8362le0neg1d 9344 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  <_ 
0  <->  0  <_  -u (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
8482, 83mpbird 223 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  <_  0
)
8562, 84absnidd 11896 . . . . 5  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  =  -u (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
8685sumeq2dv 12176 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  =  sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )
-u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
8761, 62fsumrecl 12207 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) )  e.  RR )
8862renegcld 9210 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  -u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  RR )
8961, 88, 82fsumge0 12253 . . . . . . 7  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  0  <_  sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )
-u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
9089, 64breqtrd 4047 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  0  <_  -u sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
9187le0neg1d 9344 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) )  <_  0  <->  0  <_  -u sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
9290, 91mpbird 223 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) )  <_  0 )
9387, 92absnidd 11896 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  -u sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
9464, 86, 933eqtr4rd 2326 . . 3  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
95 pntpbnd1.c . . . . . . . . . . . . 13  |-  C  =  ( A  +  2 )
96 pntpbnd1.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR+ )
97 2rp 10359 . . . . . . . . . . . . . 14  |-  2  e.  RR+
98 rpaddcl 10374 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR+  /\  2  e.  RR+ )  ->  ( A  +  2 )  e.  RR+ )
9996, 97, 98sylancl 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  2 )  e.  RR+ )
10095, 99syl5eqel 2367 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR+ )
101100, 15rpdivcld 10407 . . . . . . . . . . 11  |-  ( ph  ->  ( C  /  E
)  e.  RR+ )
102101rpred 10390 . . . . . . . . . 10  |-  ( ph  ->  ( C  /  E
)  e.  RR )
103102reefcld 12369 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
104 pnfxr 10455 . . . . . . . . 9  |-  +oo  e.  RR*
105 icossre 10730 . . . . . . . . 9  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\  +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,)  +oo )  C_  RR )
106103, 104, 105sylancl 643 . . . . . . . 8  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,)  +oo )  C_  RR )
107 pntpbnd1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo ) )
108106, 107sseldd 3181 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
109108, 4remulcld 8863 . . . . . 6  |-  ( ph  ->  ( K  x.  Y
)  e.  RR )
1104recnd 8861 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
111110mulid2d 8853 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  =  Y )
112 1re 8837 . . . . . . . . . . 11  |-  1  e.  RR
113112a1i 10 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
114 efgt1 12396 . . . . . . . . . . 11  |-  ( ( C  /  E )  e.  RR+  ->  1  < 
( exp `  ( C  /  E ) ) )
115101, 114syl 15 . . . . . . . . . 10  |-  ( ph  ->  1  <  ( exp `  ( C  /  E
) ) )
116 elicopnf 10739 . . . . . . . . . . . . 13  |-  ( ( exp `  ( C  /  E ) )  e.  RR  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,) 
+oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
117103, 116syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
118117simplbda 607 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo ) )  -> 
( exp `  ( C  /  E ) )  <_  K )
119107, 118mpdan 649 . . . . . . . . . 10  |-  ( ph  ->  ( exp `  ( C  /  E ) )  <_  K )
120113, 103, 108, 115, 119ltletrd 8976 . . . . . . . . 9  |-  ( ph  ->  1  <  K )
121 ltmul1 9606 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  K  e.  RR  /\  ( Y  e.  RR  /\  0  <  Y ) )  -> 
( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
122113, 108, 4, 26, 121syl112anc 1186 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
123120, 122mpbid 201 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  <  ( K  x.  Y ) )
124111, 123eqbrtrrd 4045 . . . . . . 7  |-  ( ph  ->  Y  <  ( K  x.  Y ) )
1254, 109, 124ltled 8967 . . . . . 6  |-  ( ph  ->  Y  <_  ( K  x.  Y ) )
126 flword2 10943 . . . . . 6  |-  ( ( Y  e.  RR  /\  ( K  x.  Y
)  e.  RR  /\  Y  <_  ( K  x.  Y ) )  -> 
( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
1274, 109, 125, 126syl3anc 1182 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
128109flcld 10930 . . . . . 6  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ZZ )
129 uzid 10242 . . . . . 6  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ZZ  ->  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y
) ) ) )
130128, 129syl 15 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) )
131 elfzuzb 10792 . . . . 5  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ( |_
`  Y ) ... ( |_ `  ( K  x.  Y )
) )  <->  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  /\  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) ) )
132127, 130, 131sylanbrc 645 . . . 4  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y
) ) ) )
133 oveq2 5866 . . . . . . . 8  |-  ( x  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) ) )
134133raleqdv 2742 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i ) ) )
135133raleqdv 2742 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0 ) )
136134, 135orbi12d 690 . . . . . 6  |-  ( x  =  ( |_ `  Y )  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 ) ) )
137136imbi2d 307 . . . . 5  |-  ( x  =  ( |_ `  Y )  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 ) ) ) )
138 oveq2 5866 . . . . . . . 8  |-  ( x  =  m  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... m ) )
139138raleqdv 2742 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )
) )
140138raleqdv 2742 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) ( R `  i )  <_  0
) )
141139, 140orbi12d 690 . . . . . 6  |-  ( x  =  m  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0 ) ) )
142141imbi2d 307 . . . . 5  |-  ( x  =  m  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0 ) ) ) )
143 oveq2 5866 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) )
144143raleqdv 2742 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )
) )
145143raleqdv 2742 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) ( R `  i )  <_  0
) )
146144, 145orbi12d 690 . . . . . 6  |-  ( x  =  ( m  + 
1 )  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) ( R `  i
)  <_  0 ) ) )
147146imbi2d 307 . . . . 5  |-  ( x  =  ( m  + 
1 )  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0 ) ) ) )
148 oveq2 5866 . . . . . . . 8  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) )
149148raleqdv 2742 . . . . . . 7  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) ) )
150148raleqdv 2742 . . . . . . 7  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 ) )
151149, 150orbi12d 690 . . . . . 6  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 ) ) )
152151imbi2d 307 . . . . 5  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 ) ) ) )
153 elfzle3 10802 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) )
154 elfzel2 10796 . . . . . . . . . . . . 13  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  ZZ )
155154zred 10117 . . . . . . . . . . . 12  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  RR )
156155ltp1d 9687 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  < 
( ( |_ `  Y )  +  1 ) )
157 peano2re 8985 . . . . . . . . . . . . 13  |-  ( ( |_ `  Y )  e.  RR  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
158155, 157syl 15 . . . . . . . . . . . 12  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
159155, 158ltnled 8966 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  <  ( ( |_ `  Y )  +  1 )  <->  -.  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) ) )
160156, 159mpbid 201 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  -.  ( ( |_ `  Y )  +  1 )  <_  ( |_ `  Y ) )
161153, 160pm2.65i 165 . . . . . . . . 9  |-  -.  i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) )
162161pm2.21i 123 . . . . . . . 8  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( R `  i )  <_  0 )
163162rgen 2608 . . . . . . 7  |-  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0
164163olci 380 . . . . . 6  |-  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 )
165164a1ii 24 . . . . 5  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  ->  ( ph  ->  ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 ) ) )
166 elfzofz 10889 . . . . . . . . . 10  |-  ( m  e.  ( ( |_
`  Y )..^ ( |_ `  ( K  x.  Y ) ) )  ->  m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) ) )
167 elfzp12 10861 . . . . . . . . . . 11  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  ->  ( m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) )  <-> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
168127, 167syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( ( |_ `  Y
) ... ( |_ `  ( K  x.  Y
) ) )  <->  ( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) ) )
169166, 168syl5ib 210 . . . . . . . . 9  |-  ( ph  ->  ( m  e.  ( ( |_ `  Y
)..^ ( |_ `  ( K  x.  Y
) ) )  -> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
170169imp 418 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ( |_ `  Y )..^ ( |_ `  ( K  x.  Y
) ) ) )  ->  ( m  =  ( |_ `  Y
)  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) )
17131nnrpd 10389 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  RR+ )
17238ffvelrni 5664 . . . . . . . . . . . . . 14  |-  ( ( ( |_ `  Y
)  +  1 )  e.  RR+  ->  ( R `
 ( ( |_
`  Y )  +  1 ) )  e.  RR )
173171, 172syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R `  (
( |_ `  Y
)  +  1 ) )  e.  RR )
1746, 173letrid 8969 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  (
( |_ `  Y
)  +  1 ) )  <_  0 ) )
175174adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  ( ( |_ `  Y )  +  1 ) )  <_ 
0 ) )
176 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( |_ `  Y )  ->  (
m  +  1 )  =  ( ( |_
`  Y )  +  1 ) )
177176oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( m  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) )  =  ( ( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) ) )
1784flcld 10930 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  Y
)  e.  ZZ )
179178peano2zd 10120 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  ZZ )
180 fzsn 10833 . . . . . . . . . . . . . . . 16  |-  ( ( ( |_ `  Y
)  +  1 )  e.  ZZ  ->  (
( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) )  =  { ( ( |_ `  Y )  +  1 ) } )
181179, 180syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( |_
`  Y )  +  1 ) ... (
( |_ `  Y
)  +  1 ) )  =  { ( ( |_ `  Y
)  +  1 ) } )
182177, 181sylan9eqr 2337 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  { ( ( |_
`  Y )  +  1 ) } )
183182raleqdv 2742 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) } 0  <_  ( R `  i ) ) )
184 ovex 5883 . . . . . . . . . . . . . 14  |-  ( ( |_ `  Y )  +  1 )  e. 
_V
185 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  ( R `  i )  =  ( R `  ( ( |_ `  Y )  +  1 ) ) )
186185breq2d 4035 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
187184, 186ralsn 3674 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( |_ `  Y
)  +  1 ) } 0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) )
188183, 187syl6bb 252 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
189182raleqdv 2742 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) }  ( R `  i )  <_  0 ) )
190185breq1d 4033 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
191184, 190ralsn 3674 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( |_ `  Y
)  +  1 ) }  ( R `  i )  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0 )
192189, 191syl6bb 252 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
193188, 192orbi12d 690 . . . . . . . . . . 11  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0 )  <->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  ( ( |_ `  Y )  +  1 ) )  <_ 
0 ) ) )
194175, 193mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0 ) )
195194a1d 22 . . . . . . . . 9  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0 )  -> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) ( R `  i
)  <_  0 ) ) )
196 elfzuz 10794 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
197196adantl 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
198 eluzfz2 10804 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
199197, 198syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
200 fveq2 5525 . . . . . . . . . . . . . . . . 17  |-  ( i  =  m  ->  ( R `  i )  =  ( R `  m ) )
201200breq2d 4035 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  m ) ) )
202201rspcv 2880 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
203199, 202syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
204 pntpbnd1.3 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
205204adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
20633uztrn2 10245 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  m  e.  NN )
20731, 196, 206syl2an 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  NN )
208207adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  m  e.  NN )
209 elfzle1 10799 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  (
( |_ `  Y
)  +  1 )  <_  m )
210209adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  +  1 )  <_  m
)
211 elfzelz 10798 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ZZ )
212 zltp1le 10067 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( |_ `  Y
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( ( |_ `  Y )  <  m  <->  ( ( |_ `  Y
)  +  1 )  <_  m ) )
213178, 211, 212syl2an 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  < 
m  <->  ( ( |_
`  Y )  +  1 )  <_  m
) )
214210, 213mpbird 223 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( |_ `  Y )  <  m
)
215 fllt 10938 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Y  e.  RR  /\  m  e.  ZZ )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m ) )
2164, 211, 215syl2an 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m
) )
217214, 216mpbird 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  Y  <  m )
218 elfzle2 10800 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  <_  ( |_ `  ( K  x.  Y )
) )
219218adantl 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( |_ `  ( K  x.  Y ) ) )
220 flge 10937 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( K  x.  Y
)  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  ( K  x.  Y )  <->  m  <_  ( |_ `  ( K  x.  Y
) ) ) )
221109, 211, 220syl2an 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  <_  ( K  x.  Y
)  <->  m  <_  ( |_
`  ( K  x.  Y ) ) ) )
222219, 221mpbird 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( K  x.  Y ) )
223217, 222jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  /\  m  <_ 
( K  x.  Y
) ) )
224223adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) )
22510ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  E  e.  ( 0 (,) 1 ) )
2263ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  Y  e.  ( X (,)  +oo ) )
227 simpr 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( abs `  ( R `  m )
)  <_  ( abs `  ( ( R `  ( m  +  1
) )  -  ( R `  m )
) ) )
22837, 225, 7, 226, 208, 224, 227pntpbnd1a 20734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( abs `  (
( R `  m
)  /  m ) )  <_  E )
229 breq2 4027 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( Y  <  y  <->  Y  <  m ) )
230 breq1 4026 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  (
y  <_  ( K  x.  Y )  <->  m  <_  ( K  x.  Y ) ) )
231229, 230anbi12d 691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( Y  <  y  /\  y  <_  ( K  x.  Y ) )  <-> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) ) )
232 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  ( R `  y )  =  ( R `  m ) )
233 id 19 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  y  =  m )
234232, 233oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  m  ->  (
( R `  y
)  /  y )  =  ( ( R `
 m )  /  m ) )
235234fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  m
)  /  m ) ) )
236235breq1d 4033 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  E  <->  ( abs `  ( ( R `  m )  /  m
) )  <_  E
) )
237231, 236anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  m  ->  (
( ( Y  < 
y  /\  y  <_  ( K  x.  Y ) )  /\  ( abs `  ( ( R `  y )  /  y
) )  <_  E
)  <->  ( ( Y  <  m  /\  m  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 m )  /  m ) )  <_  E ) ) )
238237rspcev 2884 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  NN  /\  ( ( Y  < 
m  /\  m  <_  ( K  x.  Y ) )  /\  ( abs `  ( ( R `  m )  /  m
) )  <_  E
) )  ->  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
239208, 224, 228, 238syl12anc 1180 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  E. y  e.  NN  ( ( Y  < 
y  /\  y  <_  ( K  x.  Y ) )  /\  ( abs `  ( ( R `  y )  /  y
) )  <_  E
) )
240205, 239mtand 640 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  ( abs `  ( R `  m ) )  <_ 
( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
241240adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
242207nnrpd 10389 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  RR+ )
24338ffvelrni 5664 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  RR+  ->  ( R `
 m )  e.  RR )
244242, 243syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  m )  e.  RR )
245244adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  RR )
246245recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  CC )
247246subid1d 9146 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  =  ( R `  m ) )
248207peano2nnd 9763 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  NN )
249248nnrpd 10389 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  RR+ )
25038ffvelrni 5664 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  e.  RR+  ->  ( R `
 ( m  + 
1 ) )  e.  RR )
251249, 250syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  ( m  +  1 ) )  e.  RR )
252251adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
2535a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  e.  RR )
254 letric 8921 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  ( R `  ( m  +  1 ) )  e.  RR )  -> 
( 0  <_  ( R `  ( m  +  1 ) )  \/  ( R `  ( m  +  1
) )  <_  0
) )
2555, 251, 254sylancr 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  ( m  +  1
) )  \/  ( R `  ( m  +  1 ) )  <_  0 ) )
256255ord 366 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  0  <_  ( R `  ( m  +  1
) )  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
257256imp 418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  0  <_  ( R `  (
m  +  1 ) ) )  ->  ( R `  ( m  +  1 ) )  <_  0 )
258257adantrl 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  0
)
259252, 253, 245, 258lesub2dd 9389 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  <_  (
( R `  m
)  -  ( R `
 ( m  + 
1 ) ) ) )
260247, 259eqbrtrrd 4045 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  <_  (
( R `  m
)  -  ( R `
 ( m  + 
1 ) ) ) )
261 simprl 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  <_  ( R `  m )
)
262245, 261absidd 11905 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( abs `  ( R `  m )
)  =  ( R `
 m ) )
263252, 253, 245, 258, 261letrd 8973 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  ( R `  m )
)
264252, 245, 263abssuble0d 11915 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) )  =  ( ( R `  m )  -  ( R `  ( m  +  1
) ) ) )
265260, 262, 2643brtr4d 4053 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( abs `  ( R `  m )
)  <_  ( abs `  ( ( R `  ( m  +  1
) )  -  ( R `  m )
) ) )
266265expr 598 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  ( -.  0  <_  ( R `
 ( m  + 
1 ) )  -> 
( abs `  ( R `  m )
)  <_  ( abs `  ( ( R `  ( m  +  1
) )  -  ( R `  m )
) ) ) )
267241, 266mt3d 117 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  0  <_  ( R `  (
m  +  1 ) ) )
268267ex 423 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  m )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
269203, 268syld 40 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
270 ovex 5883 . . . . . . . . . . . . . 14  |-  ( m  +  1 )  e. 
_V
271 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( i  =  ( m  + 
1 )  ->  ( R `  i )  =  ( R `  ( m  +  1
) ) )
272271breq2d 4035 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1 ) ) ) )
273270, 272ralsn 3674 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
m  +  1 ) } 0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1
) ) )
274269, 273syl6ibr 218 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  A. i  e.  { ( m  + 
1 ) } 0  <_  ( R `  i ) ) )
275274ancld 536 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  /\  A. i  e.  { (
m  +  1 ) } 0  <_  ( R `  i )
) ) )
276 fzsuc 10835 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
277197, 276syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
278277raleqdv 2742 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) 0  <_  ( R `  i ) ) )
279 ralunb 3356 . . . . . . . . . . . 12  |-  ( A. i  e.  ( (
( ( |_ `  Y )  +  1 ) ... m )  u.  { ( m  +  1 ) } ) 0  <_  ( R `  i )  <->  ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  /\  A. i  e.  { (
m  +  1 ) } 0  <_  ( R `  i )
) )
280278, 279syl6bb 252 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  /\  A. i  e.  { (
m  +  1 ) } 0  <_  ( R `  i )
) ) )
281275, 280sylibrd 225 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )
) )
282200breq1d 4033 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
( R `  i
)  <_  0  <->  ( R `  m )  <_  0
) )
283282rspcv 2880 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0  ->  ( R `  m )  <_  0 ) )
284199, 283syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  m )  <_  0 ) )
285240adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
286256con1d 116 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  ( R `  ( m  +  1 ) )  <_  0  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
287286imp 418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  ( R `  ( m  +  1 ) )  <_  0 )  -> 
0  <_  ( R `  ( m  +  1 ) ) )
288287adantrl 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  <_  ( R `  ( m  +  1 ) ) )
289244adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  RR )
290289renegcld 9210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  e.  RR )
291251adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
292290, 291addge02d 9361 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( 0  <_ 
( R `  (
m  +  1 ) )  <->  -u ( R `  m )  <_  (
( R `  (
m  +  1 ) )  +  -u ( R `  m )
) ) )
293288, 292mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  <_  (
( R `  (
m  +  1 ) )  +  -u ( R `  m )
) )
294291recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  CC )
295289recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  CC )
296294, 295negsubd 9163 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( ( R `
 ( m  + 
1 ) )  + 
-u ( R `  m ) )  =  ( ( R `  ( m  +  1
) )  -  ( R `  m )
) )
297293, 296breqtrd 4047 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  <_  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) )
298 simprl 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  0
)
299289, 298absnidd 11896 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  ( R `  m )
)  =  -u ( R `  m )
)
3005a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  e.  RR )
301289, 300, 291, 298, 288letrd 8973 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  ( R `  ( m  +  1 ) ) )
302289, 291, 301abssubge0d 11914 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) )  =  ( ( R `  ( m  +  1 ) )  -  ( R `  m ) ) )
303297, 299, 3023brtr4d 4053 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  ( R `  m )
)  <_  ( abs `  ( ( R `  ( m  +  1
) )  -  ( R `  m )
) ) )
304303expr 598 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  ( -.  ( R `  (
m  +  1 ) )  <_  0  ->  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) ) )
305285, 304mt3d 117 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  ( R `  ( m  +  1 ) )  <_  0 )
306305ex 423 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  m )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0
) )
307284, 306syld 40 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
308271breq1d 4033 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0
) )
309270, 308ralsn 3674 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
m  +  1 ) }  ( R `  i )  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0 )
310307, 309syl6ibr 218 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  A. i  e.  { ( m  + 
1 ) }  ( R `  i )  <_  0 ) )
311310ancld 536 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( A. i  e.  (
(