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

Theorem pntpbnd1 22967
Description: Lemma for pntpbnd 22969. (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 11911 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )  e.  Fin )
2 ioossre 11467 . . . . . . . . . . . . . 14  |-  ( X (,) +oo )  C_  RR
3 pntpbnd1.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  ( X (,) +oo ) )
42, 3sseldi 3461 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
5 0red 9497 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  RR )
6 pntpbnd1.x . . . . . . . . . . . . . . . 16  |-  X  =  ( exp `  (
2  /  E ) )
7 2re 10501 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
8 ioossre 11467 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) 1 )  C_  RR
9 pntpbnd1.e . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
108, 9sseldi 3461 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E  e.  RR )
11 eliooord 11465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
129, 11syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
1312simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  E )
1410, 13elrpd 11135 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR+ )
15 rerpdivcl 11128 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  E  e.  RR+ )  -> 
( 2  /  E
)  e.  RR )
167, 14, 15sylancr 663 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2  /  E
)  e.  RR )
1716reefcld 13490 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  (
2  /  E ) )  e.  RR )
186, 17syl5eqel 2546 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
19 efgt0 13504 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  /  E )  e.  RR  ->  0  <  ( exp `  (
2  /  E ) ) )
2016, 19syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( exp `  ( 2  /  E
) ) )
2120, 6syl6breqr 4439 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  X )
22 eliooord 11465 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,) +oo )  ->  ( X  <  Y  /\  Y  < +oo ) )
233, 22syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  < +oo )
)
2423simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
255, 18, 4, 21, 24lttrd 9642 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  Y )
265, 4, 25ltled 9632 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  Y )
27 flge0nn0 11782 . . . . . . . . . . . . 13  |-  ( ( Y  e.  RR  /\  0  <_  Y )  -> 
( |_ `  Y
)  e.  NN0 )
284, 26, 27syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  Y
)  e.  NN0 )
29 nn0p1nn 10729 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  NN0  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
3028, 29syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
31 elfzuz 11565 . . . . . . . . . . 11  |-  ( n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
32 eluznn 11035 . . . . . . . . . . 11  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  n  e.  NN )
3330, 31, 32syl2an 477 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  NN )
3433nnrpd 11136 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  RR+ )
35 pntpbnd.r . . . . . . . . . . 11  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
3635pntrf 22944 . . . . . . . . . 10  |-  R : RR+
--> RR
3736ffvelrni 5950 . . . . . . . . 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 10449 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  +  1 )  e.  NN )
4033, 39nnmulcld 10479 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
4138, 40nndivred 10480 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  e.  RR )
4241adantlr 714 . . . . . 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 13328 . . . . 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 714 . . . . . . 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 5798 . . . . . . . . . 10  |-  ( i  =  n  ->  ( R `  i )  =  ( R `  n ) )
4645breq2d 4411 . . . . . . . . 9  |-  ( i  =  n  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  n ) ) )
4746rspccva 3176 . . . . . . . 8  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  0  <_  ( R `  n ) )
4847adantll 713 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( R `  n )
)
4940adantlr 714 . . . . . . . 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 10447 . . . . . . 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 10475 . . . . . . 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 10308 . . . . . . 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 1220 . . . . . 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 13375 . . . . 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 13026 . . . 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 13026 . . . . 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 13297 . . . 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 2498 . . 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 11911 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  e.  Fin )
6041adantlr 714 . . . . . 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 9522 . . . . 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 13371 . . . 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 714 . . . . . . . . . 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 9885 . . . . . . . . 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 4409 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( R `  i
)  <_  0  <->  ( R `  n )  <_  0
) )
6665rspccva 3176 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( R `  i
)  <_  0  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6766adantll 713 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6863le0neg1d 10021 . . . . . . . . . 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 714 . . . . . . . . . 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 10447 . . . . . . . . 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 10475 . . . . . . . . 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 10308 . . . . . . . . 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 1220 . . . . . . . 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 9522 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  CC )
7640nncnd 10448 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  CC )
7740nnne0d 10476 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  =/=  0
)
7875, 76, 77divnegd 10230 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -u ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  =  ( -u ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
7978adantlr 714 . . . . . . . 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 4425 . . . . . . 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 10021 . . . . . . 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 13017 . . . . 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 13297 . . . 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 13328 . . . . 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 9885 . . . . . . . 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 13375 . . . . . . 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 4423 . . . . . 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 10021 . . . . . 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 13017 . . . 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 2506 . . 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 11106 . . . . . . . . . . . . . 14  |-  2  e.  RR+
96 rpaddcl 11121 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR+  /\  2  e.  RR+ )  ->  ( A  +  2 )  e.  RR+ )
9794, 95, 96sylancl 662 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  2 )  e.  RR+ )
9893, 97syl5eqel 2546 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR+ )
9998, 14rpdivcld 11154 . . . . . . . . . . 11  |-  ( ph  ->  ( C  /  E
)  e.  RR+ )
10099rpred 11137 . . . . . . . . . 10  |-  ( ph  ->  ( C  /  E
)  e.  RR )
101100reefcld 13490 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
102 pnfxr 11202 . . . . . . . . 9  |- +oo  e.  RR*
103 icossre 11486 . . . . . . . . 9  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\ +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
104101, 102, 103sylancl 662 . . . . . . . 8  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,) +oo )  C_  RR )
105 pntpbnd1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )
106104, 105sseldd 3464 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
107106, 4remulcld 9524 . . . . . 6  |-  ( ph  ->  ( K  x.  Y
)  e.  RR )
1084recnd 9522 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
109108mulid2d 9514 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  =  Y )
110 1red 9511 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
111 efgt1 13517 . . . . . . . . . . 11  |-  ( ( C  /  E )  e.  RR+  ->  1  < 
( exp `  ( C  /  E ) ) )
11299, 111syl 16 . . . . . . . . . 10  |-  ( ph  ->  1  <  ( exp `  ( C  /  E
) ) )
113 elicopnf 11501 . . . . . . . . . . . . 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 624 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( exp `  ( C  /  E ) ) [,) +oo ) )  ->  ( exp `  ( C  /  E ) )  <_  K )
116105, 115mpdan 668 . . . . . . . . . 10  |-  ( ph  ->  ( exp `  ( C  /  E ) )  <_  K )
117110, 101, 106, 112, 116ltletrd 9641 . . . . . . . . 9  |-  ( ph  ->  1  <  K )
118 ltmul1 10289 . . . . . . . . . 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 1223 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
120117, 119mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  <  ( K  x.  Y ) )
121109, 120eqbrtrrd 4421 . . . . . . 7  |-  ( ph  ->  Y  <  ( K  x.  Y ) )
1224, 107, 121ltled 9632 . . . . . 6  |-  ( ph  ->  Y  <_  ( K  x.  Y ) )
123 flword2 11777 . . . . . 6  |-  ( ( Y  e.  RR  /\  ( K  x.  Y
)  e.  RR  /\  Y  <_  ( K  x.  Y ) )  -> 
( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
1244, 107, 122, 123syl3anc 1219 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
125107flcld 11764 . . . . . 6  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ZZ )
126 uzid 10985 . . . . . 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 11563 . . . . 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 664 . . . 4  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y
) ) ) )
130 oveq2 6207 . . . . . . . 8  |-  ( x  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) ) )
131130raleqdv 3027 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i ) ) )
132130raleqdv 3027 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0 ) )
133131, 132orbi12d 709 . . . . . 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 6207 . . . . . . . 8  |-  ( x  =  m  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... m ) )
136135raleqdv 3027 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )
) )
137135raleqdv 3027 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) ( R `  i )  <_  0
) )
138136, 137orbi12d 709 . . . . . 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 6207 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) )
141140raleqdv 3027 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )
) )
142140raleqdv 3027 . . . . . . 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 709 . . . . . 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 6207 . . . . . . . 8  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) )
146145raleqdv 3027 . . . . . . 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 3027 . . . . . . 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 709 . . . . . 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 11573 . . . . . . . . 9  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) )
151 elfzel2 11567 . . . . . . . . . . . 12  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  ZZ )
152151zred 10857 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  RR )
153152ltp1d 10373 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  < 
( ( |_ `  Y )  +  1 ) )
154 peano2re 9652 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  RR  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
155152, 154syl 16 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
156152, 155ltnled 9631 . . . . . . . . . 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 2897 . . . . . . 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 11683 . . . . . . . . . 10  |-  ( m  e.  ( ( |_
`  Y )..^ ( |_ `  ( K  x.  Y ) ) )  ->  m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) ) )
163 elfzp12 11655 . . . . . . . . . . 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 11136 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  RR+ )
16836ffvelrni 5950 . . . . . . . . . . . . . 14  |-  ( ( ( |_ `  Y
)  +  1 )  e.  RR+  ->  ( R `
 ( ( |_
`  Y )  +  1 ) )  e.  RR )
169167, 168syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R `  (
( |_ `  Y
)  +  1 ) )  e.  RR )
1705, 169letrid 9634 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  (
( |_ `  Y
)  +  1 ) )  <_  0 ) )
171170adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  ( ( |_ `  Y )  +  1 ) )  <_ 
0 ) )
172 oveq1 6206 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( |_ `  Y )  ->  (
m  +  1 )  =  ( ( |_
`  Y )  +  1 ) )
173172oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( m  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) )  =  ( ( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) ) )
1744flcld 11764 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  Y
)  e.  ZZ )
175174peano2zd 10860 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  ZZ )
176 fzsn 11616 . . . . . . . . . . . . . . . 16  |-  ( ( ( |_ `  Y
)  +  1 )  e.  ZZ  ->  (
( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) )  =  { ( ( |_ `  Y )  +  1 ) } )
177175, 176syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( |_
`  Y )  +  1 ) ... (
( |_ `  Y
)  +  1 ) )  =  { ( ( |_ `  Y
)  +  1 ) } )
178173, 177sylan9eqr 2517 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  { ( ( |_
`  Y )  +  1 ) } )
179178raleqdv 3027 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) } 0  <_  ( R `  i ) ) )
180 ovex 6224 . . . . . . . . . . . . . 14  |-  ( ( |_ `  Y )  +  1 )  e. 
_V
181 fveq2 5798 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  ( R `  i )  =  ( R `  ( ( |_ `  Y )  +  1 ) ) )
182181breq2d 4411 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
183180, 182ralsn 4022 . . . . . . . . . . . . 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 3027 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) }  ( R `  i )  <_  0 ) )
186181breq1d 4409 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
187180, 186ralsn 4022 . . . . . . . . . . . . 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 709 . . . . . . . . . . 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 11565 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
193192adantl 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
194 eluzfz2 11575 . . . . . . . . . . . . . . . 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 5798 . . . . . . . . . . . . . . . . 17  |-  ( i  =  m  ->  ( R `  i )  =  ( R `  m ) )
197196breq2d 4411 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  m ) ) )
198197rspcv 3173 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . 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 11035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  m  e.  NN )
20330, 192, 202syl2an 477 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  NN )
204203adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  m  e.  NN )
205 elfzle1 11570 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  (
( |_ `  Y
)  +  1 )  <_  m )
206205adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  +  1 )  <_  m
)
207 elfzelz 11569 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ZZ )
208 zltp1le 10804 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( |_ `  Y
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( ( |_ `  Y )  <  m  <->  ( ( |_ `  Y
)  +  1 )  <_  m ) )
209174, 207, 208syl2an 477 . . . . . . . . . . . . . . . . . . . . . . 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 11772 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Y  e.  RR  /\  m  e.  ZZ )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m ) )
2124, 207, 211syl2an 477 . . . . . . . . . . . . . . . . . . . . . 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 11571 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  <_  ( |_ `  ( K  x.  Y )
) )
215214adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( |_ `  ( K  x.  Y ) ) )
216 flge 11771 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( K  x.  Y
)  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  ( K  x.  Y )  <->  m  <_  ( |_ `  ( K  x.  Y
) ) ) )
217107, 207, 216syl2an 477 . . . . . . . . . . . . . . . . . . . . . 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 532 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  /\  m  <_ 
( K  x.  Y
) ) )
220219adantr 465 . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  E  e.  ( 0 (,) 1 ) )
2223ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  Y  e.  ( X (,) +oo ) )
223 simpr 461 . . . . . . . . . . . . . . . . . . . 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 22966 . . . . . . . . . . . . . . . . . . 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 4403 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( Y  <  y  <->  Y  <  m ) )
226 breq1 4402 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  (
y  <_  ( K  x.  Y )  <->  m  <_  ( K  x.  Y ) ) )
227225, 226anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( Y  <  y  /\  y  <_  ( K  x.  Y ) )  <-> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) ) )
228 fveq2 5798 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  ( R `  y )  =  ( R `  m ) )
229 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  y  =  m )
230228, 229oveq12d 6217 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  m  ->  (
( R `  y
)  /  y )  =  ( ( R `
 m )  /  m ) )
231230fveq2d 5802 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  m
)  /  m ) ) )
232231breq1d 4409 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  E  <->  ( abs `  ( ( R `  m )  /  m
) )  <_  E
) )
233227, 232anbi12d 710 . . . . . . . . . . . . . . . . . . . 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 3177 . . . . . . . . . . . . . . . . . . 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 1217 . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  ( abs `  ( R `  m ) )  <_ 
( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
237236adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
238203nnrpd 11136 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  RR+ )
23936ffvelrni 5950 . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  RR )
242241recnd 9522 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  CC )
243242subid1d 9818 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  =  ( R `  m ) )
244203peano2nnd 10449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  NN )
245244nnrpd 11136 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  RR+ )
24636ffvelrni 5950 . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
249 0red 9497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  e.  RR )
250 0re 9496 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  RR
251 letric 9585 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  ( R `  ( m  +  1 ) )  e.  RR )  -> 
( 0  <_  ( R `  ( m  +  1 ) )  \/  ( R `  ( m  +  1
) )  <_  0
) )
252250, 247, 251sylancr 663 . . . . . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  0
)
256248, 249, 241, 255lesub2dd 10066 . . . . . . . . . . . . . . . . . . 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 4421 . . . . . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  <_  ( R `  m )
)
259241, 258absidd 13026 . . . . . . . . . . . . . . . . . 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 9638 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  ( R `  m )
)
261248, 241, 260abssuble0d 13036 . . . . . . . . . . . . . . . . . 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 4429 . . . . . . . . . . . . . . . . 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 615 . . . . . . . . . . . . . . . 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 6224 . . . . . . . . . . . . . 14  |-  ( m  +  1 )  e. 
_V
268 fveq2 5798 . . . . . . . . . . . . . . 15  |-  ( i  =  ( m  + 
1 )  ->  ( R `  i )  =  ( R `  ( m  +  1
) ) )
269268breq2d 4411 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1 ) ) ) )
270267, 269ralsn 4022 . . . . . . . . . . . . 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 553 . . . . . . . . . . 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 11618 . . . . . . . . . . . . . 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 3027 . . . . . . . . . . . 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 3644 . . . . . . . . . . . 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 4409 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
( R `  i
)  <_  0  <->  ( R `  m )  <_  0
) )
280279rspcv 3173 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  <_  ( R `  ( m  +  1 ) ) )
286240adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  RR )
287286renegcld 9885 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  e.  RR )
288247adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
289287, 288addge02d 10038 . . . . . . . . . . . . . . . . . . . 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 9522 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  CC )
292286recnd 9522 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  CC )
293291, 292negsubd 9835 . . . . . . . . . . . . . . . . . . 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 4423 . . . . . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  0
)
296286, 295absnidd 13017 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  ( R `  m )
)  =  -u ( R `  m )
)
297 0red 9497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  e.  RR )
298286, 297, 288, 295, 285letrd 9638 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  ( R `  ( m  +  1 ) ) )
299286, 288, 298abssubge0d 13035 . . . . . . . . . . . . . . . . . 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 4429 . . . . . . . . . . . . . . . . 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 615 . . . . . . . . . . . . . . . 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 4409 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0
) )
306267, 305ralsn 4022 . . . . . . . . . . . . 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 553 . . . . . . . . . . 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 3027 . . . . . . . . . . . 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&nbs