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

Theorem pntpbnd1 24152
Description: Lemma for pntpbnd 24154. (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 12124 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )  e.  Fin )
2 ioossre 11640 . . . . . . . . . . . . . 14  |-  ( X (,) +oo )  C_  RR
3 pntpbnd1.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  ( X (,) +oo ) )
42, 3sseldi 3440 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
5 0red 9627 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  RR )
6 pntpbnd1.x . . . . . . . . . . . . . . . 16  |-  X  =  ( exp `  (
2  /  E ) )
7 2re 10646 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
8 ioossre 11640 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) 1 )  C_  RR
9 pntpbnd1.e . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
108, 9sseldi 3440 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E  e.  RR )
11 eliooord 11638 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
129, 11syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
1312simpld 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  E )
1410, 13elrpd 11301 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR+ )
15 rerpdivcl 11293 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  E  e.  RR+ )  -> 
( 2  /  E
)  e.  RR )
167, 14, 15sylancr 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2  /  E
)  e.  RR )
1716reefcld 14032 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  (
2  /  E ) )  e.  RR )
186, 17syl5eqel 2494 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
19 efgt0 14047 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  /  E )  e.  RR  ->  0  <  ( exp `  (
2  /  E ) ) )
2016, 19syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( exp `  ( 2  /  E
) ) )
2120, 6syl6breqr 4435 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  X )
22 eliooord 11638 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,) +oo )  ->  ( X  <  Y  /\  Y  < +oo ) )
233, 22syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  < +oo )
)
2423simpld 457 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
255, 18, 4, 21, 24lttrd 9777 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  Y )
265, 4, 25ltled 9765 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  Y )
27 flge0nn0 11992 . . . . . . . . . . . . 13  |-  ( ( Y  e.  RR  /\  0  <_  Y )  -> 
( |_ `  Y
)  e.  NN0 )
284, 26, 27syl2anc 659 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  Y
)  e.  NN0 )
29 nn0p1nn 10876 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  NN0  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
3028, 29syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
31 elfzuz 11738 . . . . . . . . . . 11  |-  ( n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
32 eluznn 11197 . . . . . . . . . . 11  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  n  e.  NN )
3330, 31, 32syl2an 475 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  NN )
3433nnrpd 11302 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  RR+ )
35 pntpbnd.r . . . . . . . . . . 11  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
3635pntrf 24129 . . . . . . . . . 10  |-  R : RR+
--> RR
3736ffvelrni 6008 . . . . . . . . 9  |-  ( n  e.  RR+  ->  ( R `
 n )  e.  RR )
3834, 37syl 17 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  RR )
3933peano2nnd 10593 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  +  1 )  e.  NN )
4033, 39nnmulcld 10624 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
4138, 40nndivred 10625 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  e.  RR )
4241adantlr 713 . . . . . 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 )
431, 42fsumrecl 13705 . . . . 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 )
4438adantlr 713 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  e.  RR )
45 fveq2 5849 . . . . . . . . . 10  |-  ( i  =  n  ->  ( R `  i )  =  ( R `  n ) )
4645breq2d 4407 . . . . . . . . 9  |-  ( i  =  n  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  n ) ) )
4746rspccva 3159 . . . . . . . 8  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  0  <_  ( R `  n ) )
4847adantll 712 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( R `  n )
)
4940adantlr 713 . . . . . . . 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 )
5049nnred 10591 . . . . . . 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 )
5149nngt0d 10620 . . . . . . 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 ) ) )
52 divge0 10452 . . . . . . 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 ) ) ) )
5344, 48, 50, 51, 52syl22anc 1231 . . . . . 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 ) ) ) )
541, 42, 53fsumge0 13760 . . . . 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 ) ) ) )
5543, 54absidd 13403 . . . 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 ) ) ) )
5642, 53absidd 13403 . . . . 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 ) ) ) )
5756sumeq2dv 13674 . . . 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 ) ) ) )
5855, 57eqtr4d 2446 . . 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 ) ) ) ) )
59 fzfid 12124 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  e.  Fin )
6041adantlr 713 . . . . . 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 )
6160recnd 9652 . . . . 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 )
6259, 61fsumneg 13753 . . . 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 ) ) ) )
6338adantlr 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  e.  RR )
6463renegcld 10027 . . . . . . . . 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 )
6545breq1d 4405 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( R `  i
)  <_  0  <->  ( R `  n )  <_  0
) )
6665rspccva 3159 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( R `  i
)  <_  0  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6766adantll 712 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6863le0neg1d 10164 . . . . . . . . . 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 )
) )
6967, 68mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  -u ( R `  n )
)
7040adantlr 713 . . . . . . . . . 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 )
7170nnred 10591 . . . . . . . . 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 )
7270nngt0d 10620 . . . . . . . . 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 ) ) )
73 divge0 10452 . . . . . . . . 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 ) ) ) )
7464, 69, 71, 72, 73syl22anc 1231 . . . . . . . 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 ) ) ) )
7538recnd 9652 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  CC )
7640nncnd 10592 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  CC )
7740nnne0d 10621 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  =/=  0
)
7875, 76, 77divnegd 10374 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -u ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  =  ( -u ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
7978adantlr 713 . . . . . . . 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 ) ) ) )
8074, 79breqtrrd 4421 . . . . . . 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 ) ) ) )
8160le0neg1d 10164 . . . . . . 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 ) ) ) ) )
8280, 81mpbird 232 . . . . . 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
)
8360, 82absnidd 13394 . . . . 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 ) ) ) )
8483sumeq2dv 13674 . . . 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 ) ) ) )
8559, 60fsumrecl 13705 . . . . 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 )
8660renegcld 10027 . . . . . . . 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 )
8759, 86, 80fsumge0 13760 . . . . . . 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 ) ) ) )
8887, 62breqtrd 4419 . . . . . 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 ) ) ) )
8985le0neg1d 10164 . . . . . 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 ) ) ) ) )
9088, 89mpbird 232 . . . . 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 )
9185, 90absnidd 13394 . . . 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 ) ) ) )
9262, 84, 913eqtr4rd 2454 . . 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 ) ) ) ) )
93 pntpbnd1.c . . . . . . . . . . . . 13  |-  C  =  ( A  +  2 )
94 pntpbnd1.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR+ )
95 2rp 11270 . . . . . . . . . . . . . 14  |-  2  e.  RR+
96 rpaddcl 11286 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR+  /\  2  e.  RR+ )  ->  ( A  +  2 )  e.  RR+ )
9794, 95, 96sylancl 660 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  2 )  e.  RR+ )
9893, 97syl5eqel 2494 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR+ )
9998, 14rpdivcld 11321 . . . . . . . . . . 11  |-  ( ph  ->  ( C  /  E
)  e.  RR+ )
10099rpred 11304 . . . . . . . . . 10  |-  ( ph  ->  ( C  /  E
)  e.  RR )
101100reefcld 14032 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
102 pnfxr 11374 . . . . . . . . 9  |- +oo  e.  RR*
103 icossre 11659 . . . . . . . . 9  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\ +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
104101, 102, 103sylancl 660 . . . . . . . 8  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
105 pntpbnd1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )
106104, 105sseldd 3443 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
107106, 4remulcld 9654 . . . . . 6  |-  ( ph  ->  ( K  x.  Y
)  e.  RR )
1084recnd 9652 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
109108mulid2d 9644 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  =  Y )
110 1red 9641 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
111 efgt1 14060 . . . . . . . . . . 11  |-  ( ( C  /  E )  e.  RR+  ->  1  < 
( exp `  ( C  /  E ) ) )
11299, 111syl 17 . . . . . . . . . 10  |-  ( ph  ->  1  <  ( exp `  ( C  /  E
) ) )
113 elicopnf 11674 . . . . . . . . . . . . 13  |-  ( ( exp `  ( C  /  E ) )  e.  RR  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
114101, 113syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
115114simplbda 622 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )  ->  ( exp `  ( C  /  E ) )  <_  K )
116105, 115mpdan 666 . . . . . . . . . 10  |-  ( ph  ->  ( exp `  ( C  /  E ) )  <_  K )
117110, 101, 106, 112, 116ltletrd 9776 . . . . . . . . 9  |-  ( ph  ->  1  <  K )
118 ltmul1 10433 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  K  e.  RR  /\  ( Y  e.  RR  /\  0  <  Y ) )  -> 
( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
119110, 106, 4, 25, 118syl112anc 1234 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
120117, 119mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  <  ( K  x.  Y ) )
121109, 120eqbrtrrd 4417 . . . . . . 7  |-  ( ph  ->  Y  <  ( K  x.  Y ) )
1224, 107, 121ltled 9765 . . . . . 6  |-  ( ph  ->  Y  <_  ( K  x.  Y ) )
123 flword2 11986 . . . . . 6  |-  ( ( Y  e.  RR  /\  ( K  x.  Y
)  e.  RR  /\  Y  <_  ( K  x.  Y ) )  -> 
( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
1244, 107, 122, 123syl3anc 1230 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
125107flcld 11972 . . . . . 6  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ZZ )
126 uzid 11141 . . . . . 6  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ZZ  ->  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y
) ) ) )
127125, 126syl 17 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) )
128 elfzuzb 11736 . . . . 5  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ( |_
`  Y ) ... ( |_ `  ( K  x.  Y )
) )  <->  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  /\  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) ) )
129124, 127, 128sylanbrc 662 . . . 4  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y
) ) ) )
130 oveq2 6286 . . . . . . . 8  |-  ( x  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) ) )
131130raleqdv 3010 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i ) ) )
132130raleqdv 3010 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0 ) )
133131, 132orbi12d 708 . . . . . 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 ) ) )
134133imbi2d 314 . . . . 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 ) ) ) )
135 oveq2 6286 . . . . . . . 8  |-  ( x  =  m  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... m ) )
136135raleqdv 3010 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )
) )
137135raleqdv 3010 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) ( R `  i )  <_  0
) )
138136, 137orbi12d 708 . . . . . 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 ) ) )
139138imbi2d 314 . . . . 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 ) ) ) )
140 oveq2 6286 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) )
141140raleqdv 3010 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )
) )
142140raleqdv 3010 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) ( R `  i )  <_  0
) )
143141, 142orbi12d 708 . . . . . 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 ) ) )
144143imbi2d 314 . . . . 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 ) ) ) )
145 oveq2 6286 . . . . . . . 8  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) )
146145raleqdv 3010 . . . . . . 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 ) ) )
147145raleqdv 3010 . . . . . . 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 ) )
148146, 147orbi12d 708 . . . . . 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 ) ) )
149148imbi2d 314 . . . . 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 ) ) ) )
150 elfzle3 11746 . . . . . . . . 9  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) )
151 elfzel2 11740 . . . . . . . . . . . 12  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  ZZ )
152151zred 11008 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  RR )
153152ltp1d 10516 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  < 
( ( |_ `  Y )  +  1 ) )
154 peano2re 9787 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  RR  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
155152, 154syl 17 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
156152, 155ltnled 9764 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  <  ( ( |_ `  Y )  +  1 )  <->  -.  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) ) )
157153, 156mpbid 210 . . . . . . . . 9  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  -.  ( ( |_ `  Y )  +  1 )  <_  ( |_ `  Y ) )
158150, 157pm2.21dd 174 . . . . . . . 8  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( R `  i )  <_  0 )
159158rgen 2764 . . . . . . 7  |-  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0
160159olci 389 . . . . . 6  |-  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 )
161160a1ii 12 . . . . 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 ) ) )
162 elfzofz 11874 . . . . . . . . . 10  |-  ( m  e.  ( ( |_
`  Y )..^ ( |_ `  ( K  x.  Y ) ) )  ->  m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) ) )
163 elfzp12 11812 . . . . . . . . . . 11  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  ->  ( m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) )  <-> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
164124, 163syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( ( |_ `  Y
) ... ( |_ `  ( K  x.  Y
) ) )  <->  ( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) ) )
165162, 164syl5ib 219 . . . . . . . . 9  |-  ( ph  ->  ( m  e.  ( ( |_ `  Y
)..^ ( |_ `  ( K  x.  Y
) ) )  -> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
166165imp 427 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ( |_ `  Y )..^ ( |_ `  ( K  x.  Y
) ) ) )  ->  ( m  =  ( |_ `  Y
)  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) )
16730nnrpd 11302 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  RR+ )
16836ffvelrni 6008 . . . . . . . . . . . . . 14  |-  ( ( ( |_ `  Y
)  +  1 )  e.  RR+  ->  ( R `
 ( ( |_
`  Y )  +  1 ) )  e.  RR )
169167, 168syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R `  (
( |_ `  Y
)  +  1 ) )  e.  RR )
1705, 169letrid 9769 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  (
( |_ `  Y
)  +  1 ) )  <_  0 ) )
171170adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  ( ( |_ `  Y )  +  1 ) )  <_ 
0 ) )
172 oveq1 6285 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( |_ `  Y )  ->  (
m  +  1 )  =  ( ( |_
`  Y )  +  1 ) )
173172oveq2d 6294 . . . . . . . . . . . . . . 15  |-  ( m  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) )  =  ( ( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) ) )
1744flcld 11972 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  Y
)  e.  ZZ )
175174peano2zd 11011 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  ZZ )
176 fzsn 11780 . . . . . . . . . . . . . . . 16  |-  ( ( ( |_ `  Y
)  +  1 )  e.  ZZ  ->  (
( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) )  =  { ( ( |_ `  Y )  +  1 ) } )
177175, 176syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( |_
`  Y )  +  1 ) ... (
( |_ `  Y
)  +  1 ) )  =  { ( ( |_ `  Y
)  +  1 ) } )
178173, 177sylan9eqr 2465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  { ( ( |_
`  Y )  +  1 ) } )
179178raleqdv 3010 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) } 0  <_  ( R `  i ) ) )
180 ovex 6306 . . . . . . . . . . . . . 14  |-  ( ( |_ `  Y )  +  1 )  e. 
_V
181 fveq2 5849 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  ( R `  i )  =  ( R `  ( ( |_ `  Y )  +  1 ) ) )
182181breq2d 4407 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
183180, 182ralsn 4011 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( |_ `  Y
)  +  1 ) } 0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) )
184179, 183syl6bb 261 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
185178raleqdv 3010 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) }  ( R `  i )  <_  0 ) )
186181breq1d 4405 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
187180, 186ralsn 4011 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( |_ `  Y
)  +  1 ) }  ( R `  i )  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0 )
188185, 187syl6bb 261 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
189184, 188orbi12d 708 . . . . . . . . . . 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 ) ) )
190171, 189mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0 ) )
191190a1d 25 . . . . . . . . 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 ) ) )
192 elfzuz 11738 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
193192adantl 464 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
194 eluzfz2 11748 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
195193, 194syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
196 fveq2 5849 . . . . . . . . . . . . . . . . 17  |-  ( i  =  m  ->  ( R `  i )  =  ( R `  m ) )
197196breq2d 4407 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  m ) ) )
198197rspcv 3156 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
199195, 198syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
200 pntpbnd1.3 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
201200adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
202 eluznn 11197 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  m  e.  NN )
20330, 192, 202syl2an 475 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  NN )
204203adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  m  e.  NN )
205 elfzle1 11743 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  (
( |_ `  Y
)  +  1 )  <_  m )
206205adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  +  1 )  <_  m
)
207 elfzelz 11742 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ZZ )
208 zltp1le 10954 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( |_ `  Y
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( ( |_ `  Y )  <  m  <->  ( ( |_ `  Y
)  +  1 )  <_  m ) )
209174, 207, 208syl2an 475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  < 
m  <->  ( ( |_
`  Y )  +  1 )  <_  m
) )
210206, 209mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( |_ `  Y )  <  m
)
211 fllt 11980 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Y  e.  RR  /\  m  e.  ZZ )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m ) )
2124, 207, 211syl2an 475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m
) )
213210, 212mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  Y  <  m )
214 elfzle2 11744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  <_  ( |_ `  ( K  x.  Y )
) )
215214adantl 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( |_ `  ( K  x.  Y ) ) )
216 flge 11979 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( K  x.  Y
)  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  ( K  x.  Y )  <->  m  <_  ( |_ `  ( K  x.  Y
) ) ) )
217107, 207, 216syl2an 475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  <_  ( K  x.  Y
)  <->  m  <_  ( |_
`  ( K  x.  Y ) ) ) )
218215, 217mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( K  x.  Y ) )
219213, 218jca 530 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  /\  m  <_ 
( K  x.  Y
) ) )
220219adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) )
2219ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  E  e.  ( 0 (,) 1 ) )
2223ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  Y  e.  ( X (,) +oo ) )
223 simpr 459 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
22435, 221, 6, 222, 204, 220, 223pntpbnd1a 24151 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( abs `  (
( R `  m
)  /  m ) )  <_  E )
225 breq2 4399 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( Y  <  y  <->  Y  <  m ) )
226 breq1 4398 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  (
y  <_  ( K  x.  Y )  <->  m  <_  ( K  x.  Y ) ) )
227225, 226anbi12d 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( Y  <  y  /\  y  <_  ( K  x.  Y ) )  <-> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) ) )
228 fveq2 5849 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  ( R `  y )  =  ( R `  m ) )
229 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  y  =  m )
230228, 229oveq12d 6296 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  m  ->  (
( R `  y
)  /  y )  =  ( ( R `
 m )  /  m ) )
231230fveq2d 5853 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  m
)  /  m ) ) )
232231breq1d 4405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  E  <->  ( abs `  ( ( R `  m )  /  m
) )  <_  E
) )
233227, 232anbi12d 709 . . . . . . . . . . . . . . . . . . . 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 ) ) )
234233rspcev 3160 . . . . . . . . . . . . . . . . . . 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 ) )
235204, 220, 224, 234syl12anc 1228 . . . . . . . . . . . . . . . . . 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
) )
236201, 235mtand 657 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  ( abs `  ( R `  m ) )  <_ 
( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
237236adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
238203nnrpd 11302 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  RR+ )
23936ffvelrni 6008 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  RR+  ->  ( R `
 m )  e.  RR )
240238, 239syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  m )  e.  RR )
241240adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  RR )
242241recnd 9652 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  CC )
243242subid1d 9956 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  =  ( R `  m ) )
244203peano2nnd 10593 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  NN )
245244nnrpd 11302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  RR+ )
24636ffvelrni 6008 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  e.  RR+  ->  ( R `
 ( m  + 
1 ) )  e.  RR )
247245, 246syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  ( m  +  1 ) )  e.  RR )
248247adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
249 0red 9627 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  e.  RR )
250 0re 9626 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  RR
251 letric 9716 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  ( R `  ( m  +  1 ) )  e.  RR )  -> 
( 0  <_  ( R `  ( m  +  1 ) )  \/  ( R `  ( m  +  1
) )  <_  0
) )
252250, 247, 251sylancr 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  ( m  +  1
) )  \/  ( R `  ( m  +  1 ) )  <_  0 ) )
253252ord 375 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  0  <_  ( R `  ( m  +  1
) )  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
254253imp 427 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  0  <_  ( R `  (
m  +  1 ) ) )  ->  ( R `  ( m  +  1 ) )  <_  0 )
255254adantrl 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  0
)
256248, 249, 241, 255lesub2dd 10209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  <_  (
( R `  m
)  -  ( R `
 ( m  + 
1 ) ) ) )
257243, 256eqbrtrrd 4417 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  <_  (
( R `  m
)  -  ( R `
 ( m  + 
1 ) ) ) )
258 simprl 756 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  <_  ( R `  m )
)
259241, 258absidd 13403 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( abs `  ( R `  m )
)  =  ( R `
 m ) )
260248, 249, 241, 255, 258letrd 9773 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  ( R `  m )
)
261248, 241, 260abssuble0d 13413 . . . . . . . . . . . . . . . . . 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
) ) ) )
262257, 259, 2613brtr4d 4425 . . . . . . . . . . . . . . . . 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 )
) ) )
263262expr 613 . . . . . . . . . . . . . . . 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 )
) ) ) )
264237, 263mt3d 125 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  0  <_  ( R `  (
m  +  1 ) ) )
265264ex 432 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  m )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
266199, 265syld 42 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
267 ovex 6306 . . . . . . . . . . . . . 14  |-  ( m  +  1 )  e. 
_V
268 fveq2 5849 . . . . . . . . . . . . . . 15  |-  ( i  =  ( m  + 
1 )  ->  ( R `  i )  =  ( R `  ( m  +  1
) ) )
269268breq2d 4407 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1 ) ) ) )
270267, 269ralsn 4011 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
m  +  1 ) } 0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1
) ) )
271266, 270syl6ibr 227 . . . . . . . . . . . 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 ) ) )
272271ancld 551 . . . . . . . . . . 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 )
) ) )
273 fzsuc 11782 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
274193, 273syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
275274raleqdv 3010 . . . . . . . . . . . 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 ) ) )
276 ralunb 3624 . . . . . . . . . . . 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 )
) )
277275, 276syl6bb 261 . . . . . . . . . . 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 )
) ) )
278272, 277sylibrd 234 . . . . . . . . . 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 )
) )
279196breq1d 4405 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
( R `  i
)  <_  0  <->  ( R `  m )  <_  0
) )
280279rspcv 3156 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0  ->  ( R `  m )  <_  0 ) )
281195, 280syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  m )  <_  0 ) )
282236adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
283253con1d 124 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  ( R `  ( m  +  1 ) )  <_  0  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
284283imp 427 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  ( R `  ( m  +  1 ) )  <_  0 )  -> 
0  <_  ( R `  ( m  +  1 ) ) )
285284adantrl 714 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  <_  ( R `  ( m  +  1 ) ) )
286240adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  RR )
287286renegcld 10027 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  e.  RR )
288247adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
289287, 288addge02d 10181 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
290285, 289mpbid 210 . . . . . . . . . . . . . . . . . . 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 )
) )
291288recnd 9652 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  CC )
292286recnd 9652 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  CC )
293291, 292negsubd 9973 . . . . . . . . . . . . . . . . . . 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 )
) )
294290, 293breqtrd 4419 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  <_  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) )
295 simprl 756 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  0
)
296286, 295absnidd 13394 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  ( R `  m )
)  =  -u ( R `  m )
)
297 0red 9627 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  e.  RR )
298286, 297, 288, 295, 285letrd 9773 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  ( R `  ( m  +  1 ) ) )
299286, 288, 298abssubge0d 13412 . . . . . . . . . . . . . . . . . 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 ) ) )
300294, 296, 2993brtr4d 4425 . . . . . . . . . . . . . . . . 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 )
) ) )
301300expr 613 . . . . . . . . . . . . . . . 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 ) ) ) ) )
302282, 301mt3d 125 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  ( R `  ( m  +  1 ) )  <_  0 )
303302ex 432 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  m )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0
) )
304281, 303syld 42 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
305268breq1d 4405 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0
) )
306267, 305ralsn 4011 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
m  +  1 ) }  ( R `  i )  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0 )
307304, 306syl6ibr 227 . . . . . . . . . . . 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 ) )
308307ancld 551 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0  /\  A. i  e.  { ( m  +  1 ) }  ( R `  i )  <_  0
) ) )
309274raleqdv 3010 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  A. i  e.  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) ( R `  i )  <_  0 ) )
310