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

Theorem pntpbnd1 22722
Description: Lemma for pntpbnd 22724. (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 11781 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )  e.  Fin )
2 ioossre 11347 . . . . . . . . . . . . . 14  |-  ( X (,) +oo )  C_  RR
3 pntpbnd1.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  ( X (,) +oo ) )
42, 3sseldi 3344 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
5 0red 9377 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  RR )
6 pntpbnd1.x . . . . . . . . . . . . . . . 16  |-  X  =  ( exp `  (
2  /  E ) )
7 2re 10381 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
8 ioossre 11347 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) 1 )  C_  RR
9 pntpbnd1.e . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
108, 9sseldi 3344 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E  e.  RR )
11 eliooord 11345 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
129, 11syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
1312simpld 456 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  E )
1410, 13elrpd 11015 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR+ )
15 rerpdivcl 11008 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  E  e.  RR+ )  -> 
( 2  /  E
)  e.  RR )
167, 14, 15sylancr 658 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2  /  E
)  e.  RR )
1716reefcld 13358 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  (
2  /  E ) )  e.  RR )
186, 17syl5eqel 2519 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
19 efgt0 13372 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  /  E )  e.  RR  ->  0  <  ( exp `  (
2  /  E ) ) )
2016, 19syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( exp `  ( 2  /  E
) ) )
2120, 6syl6breqr 4322 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  X )
22 eliooord 11345 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,) +oo )  ->  ( X  <  Y  /\  Y  < +oo ) )
233, 22syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  < +oo )
)
2423simpld 456 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
255, 18, 4, 21, 24lttrd 9522 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  Y )
265, 4, 25ltled 9512 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  Y )
27 flge0nn0 11652 . . . . . . . . . . . . 13  |-  ( ( Y  e.  RR  /\  0  <_  Y )  -> 
( |_ `  Y
)  e.  NN0 )
284, 26, 27syl2anc 656 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  Y
)  e.  NN0 )
29 nn0p1nn 10609 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  NN0  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
3028, 29syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
31 elfzuz 11438 . . . . . . . . . . 11  |-  ( n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
32 eluznn 10915 . . . . . . . . . . 11  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  n  e.  NN )
3330, 31, 32syl2an 474 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  NN )
3433nnrpd 11016 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  RR+ )
35 pntpbnd.r . . . . . . . . . . 11  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
3635pntrf 22699 . . . . . . . . . 10  |-  R : RR+
--> RR
3736ffvelrni 5832 . . . . . . . . 9  |-  ( n  e.  RR+  ->  ( R `
 n )  e.  RR )
3834, 37syl 16 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  RR )
3933peano2nnd 10329 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  +  1 )  e.  NN )
4033, 39nnmulcld 10359 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
4138, 40nndivred 10360 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  e.  RR )
4241adantlr 709 . . . . . 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 13197 . . . . 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 709 . . . . . . 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 5681 . . . . . . . . . 10  |-  ( i  =  n  ->  ( R `  i )  =  ( R `  n ) )
4645breq2d 4294 . . . . . . . . 9  |-  ( i  =  n  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  n ) ) )
4746rspccva 3063 . . . . . . . 8  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  0  <_  ( R `  n ) )
4847adantll 708 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( R `  n )
)
4940adantlr 709 . . . . . . . 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 10327 . . . . . . 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 10355 . . . . . . 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 10188 . . . . . . 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 1214 . . . . . 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 13243 . . . . 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 12895 . . . 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 12895 . . . . 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 13166 . . . 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 2470 . . 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 11781 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  e.  Fin )
6041adantlr 709 . . . . . 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 9402 . . . . 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 13239 . . . 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 709 . . . . . . . . . 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 9765 . . . . . . . . 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 4292 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( R `  i
)  <_  0  <->  ( R `  n )  <_  0
) )
6665rspccva 3063 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( R `  i
)  <_  0  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6766adantll 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6863le0neg1d 9901 . . . . . . . . . 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 709 . . . . . . . . . 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 10327 . . . . . . . . 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 10355 . . . . . . . . 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 10188 . . . . . . . . 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 1214 . . . . . . . 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 9402 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  CC )
7640nncnd 10328 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  CC )
7740nnne0d 10356 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  =/=  0
)
7875, 76, 77divnegd 10110 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -u ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  =  ( -u ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
7978adantlr 709 . . . . . . . 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 4308 . . . . . . 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 9901 . . . . . . 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 12886 . . . . 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 13166 . . . 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 13197 . . . . 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 9765 . . . . . . . 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 13243 . . . . . . 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 4306 . . . . . 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 9901 . . . . . 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 12886 . . . 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 2478 . . 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 10986 . . . . . . . . . . . . . 14  |-  2  e.  RR+
96 rpaddcl 11001 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR+  /\  2  e.  RR+ )  ->  ( A  +  2 )  e.  RR+ )
9794, 95, 96sylancl 657 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  2 )  e.  RR+ )
9893, 97syl5eqel 2519 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR+ )
9998, 14rpdivcld 11034 . . . . . . . . . . 11  |-  ( ph  ->  ( C  /  E
)  e.  RR+ )
10099rpred 11017 . . . . . . . . . 10  |-  ( ph  ->  ( C  /  E
)  e.  RR )
101100reefcld 13358 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
102 pnfxr 11082 . . . . . . . . 9  |- +oo  e.  RR*
103 icossre 11366 . . . . . . . . 9  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\ +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
104101, 102, 103sylancl 657 . . . . . . . 8  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
105 pntpbnd1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )
106104, 105sseldd 3347 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
107106, 4remulcld 9404 . . . . . 6  |-  ( ph  ->  ( K  x.  Y
)  e.  RR )
1084recnd 9402 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
109108mulid2d 9394 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  =  Y )
110 1red 9391 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
111 efgt1 13385 . . . . . . . . . . 11  |-  ( ( C  /  E )  e.  RR+  ->  1  < 
( exp `  ( C  /  E ) ) )
11299, 111syl 16 . . . . . . . . . 10  |-  ( ph  ->  1  <  ( exp `  ( C  /  E
) ) )
113 elicopnf 11375 . . . . . . . . . . . . 13  |-  ( ( exp `  ( C  /  E ) )  e.  RR  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
114101, 113syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
115114simplbda 621 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )  ->  ( exp `  ( C  /  E ) )  <_  K )
116105, 115mpdan 663 . . . . . . . . . 10  |-  ( ph  ->  ( exp `  ( C  /  E ) )  <_  K )
117110, 101, 106, 112, 116ltletrd 9521 . . . . . . . . 9  |-  ( ph  ->  1  <  K )
118 ltmul1 10169 . . . . . . . . . 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 1217 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
120117, 119mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  <  ( K  x.  Y ) )
121109, 120eqbrtrrd 4304 . . . . . . 7  |-  ( ph  ->  Y  <  ( K  x.  Y ) )
1224, 107, 121ltled 9512 . . . . . 6  |-  ( ph  ->  Y  <_  ( K  x.  Y ) )
123 flword2 11647 . . . . . 6  |-  ( ( Y  e.  RR  /\  ( K  x.  Y
)  e.  RR  /\  Y  <_  ( K  x.  Y ) )  -> 
( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
1244, 107, 122, 123syl3anc 1213 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
125107flcld 11634 . . . . . 6  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ZZ )
126 uzid 10865 . . . . . 6  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ZZ  ->  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y
) ) ) )
127125, 126syl 16 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) )
128 elfzuzb 11436 . . . . 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 659 . . . 4  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y
) ) ) )
130 oveq2 6090 . . . . . . . 8  |-  ( x  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) ) )
131130raleqdv 2915 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i ) ) )
132130raleqdv 2915 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0 ) )
133131, 132orbi12d 704 . . . . . 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 316 . . . . 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 6090 . . . . . . . 8  |-  ( x  =  m  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... m ) )
136135raleqdv 2915 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )
) )
137135raleqdv 2915 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) ( R `  i )  <_  0
) )
138136, 137orbi12d 704 . . . . . 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 316 . . . . 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 6090 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) )
141140raleqdv 2915 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )
) )
142140raleqdv 2915 . . . . . . 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 704 . . . . . 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 316 . . . . 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 6090 . . . . . . . 8  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) )
146145raleqdv 2915 . . . . . . 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 2915 . . . . . . 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 704 . . . . . 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 316 . . . . 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 11446 . . . . . . . . 9  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) )
151 elfzel2 11440 . . . . . . . . . . . 12  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  ZZ )
152151zred 10737 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  RR )
153152ltp1d 10253 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  < 
( ( |_ `  Y )  +  1 ) )
154 peano2re 9532 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  RR  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
155152, 154syl 16 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
156152, 155ltnled 9511 . . . . . . . . . 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 2773 . . . . . . 7  |-  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0
160159olci 391 . . . . . 6  |-  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 )
161160a1ii 27 . . . . 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 11553 . . . . . . . . . 10  |-  ( m  e.  ( ( |_
`  Y )..^ ( |_ `  ( K  x.  Y ) ) )  ->  m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) ) )
163 elfzp12 11525 . . . . . . . . . . 11  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  ->  ( m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) )  <-> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
164124, 163syl 16 . . . . . . . . . 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 429 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ( |_ `  Y )..^ ( |_ `  ( K  x.  Y
) ) ) )  ->  ( m  =  ( |_ `  Y
)  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) )
16730nnrpd 11016 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  RR+ )
16836ffvelrni 5832 . . . . . . . . . . . . . 14  |-  ( ( ( |_ `  Y
)  +  1 )  e.  RR+  ->  ( R `
 ( ( |_
`  Y )  +  1 ) )  e.  RR )
169167, 168syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R `  (
( |_ `  Y
)  +  1 ) )  e.  RR )
1705, 169letrid 9514 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  (
( |_ `  Y
)  +  1 ) )  <_  0 ) )
171170adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  ( ( |_ `  Y )  +  1 ) )  <_ 
0 ) )
172 oveq1 6089 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( |_ `  Y )  ->  (
m  +  1 )  =  ( ( |_
`  Y )  +  1 ) )
173172oveq2d 6098 . . . . . . . . . . . . . . 15  |-  ( m  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) )  =  ( ( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) ) )
1744flcld 11634 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  Y
)  e.  ZZ )
175174peano2zd 10740 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  ZZ )
176 fzsn 11489 . . . . . . . . . . . . . . . 16  |-  ( ( ( |_ `  Y
)  +  1 )  e.  ZZ  ->  (
( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) )  =  { ( ( |_ `  Y )  +  1 ) } )
177175, 176syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( |_
`  Y )  +  1 ) ... (
( |_ `  Y
)  +  1 ) )  =  { ( ( |_ `  Y
)  +  1 ) } )
178173, 177sylan9eqr 2489 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  { ( ( |_
`  Y )  +  1 ) } )
179178raleqdv 2915 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) } 0  <_  ( R `  i ) ) )
180 ovex 6107 . . . . . . . . . . . . . 14  |-  ( ( |_ `  Y )  +  1 )  e. 
_V
181 fveq2 5681 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  ( R `  i )  =  ( R `  ( ( |_ `  Y )  +  1 ) ) )
182181breq2d 4294 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
183180, 182ralsn 3905 . . . . . . . . . . . . 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 2915 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) }  ( R `  i )  <_  0 ) )
186181breq1d 4292 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
187180, 186ralsn 3905 . . . . . . . . . . . . 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 704 . . . . . . . . . . 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 11438 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
193192adantl 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
194 eluzfz2 11448 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
195193, 194syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
196 fveq2 5681 . . . . . . . . . . . . . . . . 17  |-  ( i  =  m  ->  ( R `  i )  =  ( R `  m ) )
197196breq2d 4294 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  m ) ) )
198197rspcv 3060 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
199195, 198syl 16 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . 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 10915 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  m  e.  NN )
20330, 192, 202syl2an 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  NN )
204203adantr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  m  e.  NN )
205 elfzle1 11443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  (
( |_ `  Y
)  +  1 )  <_  m )
206205adantl 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  +  1 )  <_  m
)
207 elfzelz 11442 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ZZ )
208 zltp1le 10684 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( |_ `  Y
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( ( |_ `  Y )  <  m  <->  ( ( |_ `  Y
)  +  1 )  <_  m ) )
209174, 207, 208syl2an 474 . . . . . . . . . . . . . . . . . . . . . . 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 11642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Y  e.  RR  /\  m  e.  ZZ )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m ) )
2124, 207, 211syl2an 474 . . . . . . . . . . . . . . . . . . . . . 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 11444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  <_  ( |_ `  ( K  x.  Y )
) )
215214adantl 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( |_ `  ( K  x.  Y ) ) )
216 flge 11641 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( K  x.  Y
)  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  ( K  x.  Y )  <->  m  <_  ( |_ `  ( K  x.  Y
) ) ) )
217107, 207, 216syl2an 474 . . . . . . . . . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  /\  m  <_ 
( K  x.  Y
) ) )
220219adantr 462 . . . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  E  e.  ( 0 (,) 1 ) )
2223ad2antrr 720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  Y  e.  ( X (,) +oo ) )
223 simpr 458 . . . . . . . . . . . . . . . . . . . 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 22721 . . . . . . . . . . . . . . . . . . 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 4286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( Y  <  y  <->  Y  <  m ) )
226 breq1 4285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  (
y  <_  ( K  x.  Y )  <->  m  <_  ( K  x.  Y ) ) )
227225, 226anbi12d 705 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( Y  <  y  /\  y  <_  ( K  x.  Y ) )  <-> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) ) )
228 fveq2 5681 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  ( R `  y )  =  ( R `  m ) )
229 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  y  =  m )
230228, 229oveq12d 6100 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  m  ->  (
( R `  y
)  /  y )  =  ( ( R `
 m )  /  m ) )
231230fveq2d 5685 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  m
)  /  m ) ) )
232231breq1d 4292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  E  <->  ( abs `  ( ( R `  m )  /  m
) )  <_  E
) )
233227, 232anbi12d 705 . . . . . . . . . . . . . . . . . . . 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 3064 . . . . . . . . . . . . . . . . . . 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 1211 . . . . . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  ( abs `  ( R `  m ) )  <_ 
( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
237236adantr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
238203nnrpd 11016 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  RR+ )
23936ffvelrni 5832 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  RR+  ->  ( R `
 m )  e.  RR )
240238, 239syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  m )  e.  RR )
241240adantr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  RR )
242241recnd 9402 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  CC )
243242subid1d 9698 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  =  ( R `  m ) )
244203peano2nnd 10329 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  NN )
245244nnrpd 11016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  RR+ )
24636ffvelrni 5832 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  e.  RR+  ->  ( R `
 ( m  + 
1 ) )  e.  RR )
247245, 246syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  ( m  +  1 ) )  e.  RR )
248247adantr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
249 0red 9377 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  e.  RR )
250 0re 9376 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  RR
251 letric 9465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  ( R `  ( m  +  1 ) )  e.  RR )  -> 
( 0  <_  ( R `  ( m  +  1 ) )  \/  ( R `  ( m  +  1
) )  <_  0
) )
252250, 247, 251sylancr 658 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  ( m  +  1
) )  \/  ( R `  ( m  +  1 ) )  <_  0 ) )
253252ord 377 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  0  <_  ( R `  ( m  +  1
) )  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
254253imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  0  <_  ( R `  (
m  +  1 ) ) )  ->  ( R `  ( m  +  1 ) )  <_  0 )
255254adantrl 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  0
)
256248, 249, 241, 255lesub2dd 9946 . . . . . . . . . . . . . . . . . . 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 4304 . . . . . . . . . . . . . . . . . 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 750 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  <_  ( R `  m )
)
259241, 258absidd 12895 . . . . . . . . . . . . . . . . . 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 9518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  ( R `  m )
)
261248, 241, 260abssuble0d 12905 . . . . . . . . . . . . . . . . . 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 4312 . . . . . . . . . . . . . . . . 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 612 . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  m )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
266199, 265syld 44 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
267 ovex 6107 . . . . . . . . . . . . . 14  |-  ( m  +  1 )  e. 
_V
268 fveq2 5681 . . . . . . . . . . . . . . 15  |-  ( i  =  ( m  + 
1 )  ->  ( R `  i )  =  ( R `  ( m  +  1
) ) )
269268breq2d 4294 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1 ) ) ) )
270267, 269ralsn 3905 . . . . . . . . . . . . 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 550 . . . . . . . . . . 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 11491 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
274193, 273syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
275274raleqdv 2915 . . . . . . . . . . . 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 3527 . . . . . . . . . . . 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 4292 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
( R `  i
)  <_  0  <->  ( R `  m )  <_  0
) )
280279rspcv 3060 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0  ->  ( R `  m )  <_  0 ) )
281195, 280syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  m )  <_  0 ) )
282236adantr 462 . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  ( R `  ( m  +  1 ) )  <_  0 )  -> 
0  <_  ( R `  ( m  +  1 ) ) )
285284adantrl 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  <_  ( R `  ( m  +  1 ) ) )
286240adantr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  RR )
287286renegcld 9765 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  e.  RR )
288247adantr 462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
289287, 288addge02d 9918 . . . . . . . . . . . . . . . . . . . 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 9402 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  CC )
292286recnd 9402 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  CC )
293291, 292negsubd 9715 . . . . . . . . . . . . . . . . . . 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 4306 . . . . . . . . . . . . . . . . . 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 750 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  0
)
296286, 295absnidd 12886 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  ( R `  m )
)  =  -u ( R `  m )
)
297 0red 9377 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  e.  RR )
298286, 297, 288, 295, 285letrd 9518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  ( R `  ( m  +  1 ) ) )
299286, 288, 298abssubge0d 12904 . . . . . . . . . . . . . . . . . 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 4312 . . . . . . . . . . . . . . . . 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 612 . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  m )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0
) )
304281, 303syld 44 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
305268breq1d 4292 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0
) )
306267, 305ralsn 3905 . . . . . . . . . . . . 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 550 . . . . . . . . . . 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 2915 . . . . . . . . . . . 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 ralunb