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

Theorem pntpbnd1 21241
Description: Lemma for pntpbnd 21243. (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 11275 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )  e.  Fin )
2 ioossre 10936 . . . . . . . . . . . . . 14  |-  ( X (,)  +oo )  C_  RR
3 pntpbnd1.y . . . . . . . . . . . . . 14  |-  ( ph  ->  Y  e.  ( X (,)  +oo ) )
42, 3sseldi 3314 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  e.  RR )
5 0re 9055 . . . . . . . . . . . . . . 15  |-  0  e.  RR
65a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  RR )
7 pntpbnd1.x . . . . . . . . . . . . . . . 16  |-  X  =  ( exp `  (
2  /  E ) )
8 2re 10033 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
9 ioossre 10936 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0 (,) 1 )  C_  RR
10 pntpbnd1.e . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )
119, 10sseldi 3314 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E  e.  RR )
12 eliooord 10934 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E  e.  ( 0 (,) 1 )  ->  (
0  <  E  /\  E  <  1 ) )
1310, 12syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  <  E  /\  E  <  1
) )
1413simpld 446 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  E )
1511, 14elrpd 10610 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR+ )
16 rerpdivcl 10603 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  E  e.  RR+ )  -> 
( 2  /  E
)  e.  RR )
178, 15, 16sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2  /  E
)  e.  RR )
1817reefcld 12653 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( exp `  (
2  /  E ) )  e.  RR )
197, 18syl5eqel 2496 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
20 efgt0 12667 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  /  E )  e.  RR  ->  0  <  ( exp `  (
2  /  E ) ) )
2117, 20syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <  ( exp `  ( 2  /  E
) ) )
2221, 7syl6breqr 4220 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  X )
23 eliooord 10934 . . . . . . . . . . . . . . . . 17  |-  ( Y  e.  ( X (,)  +oo )  ->  ( X  <  Y  /\  Y  <  +oo ) )
243, 23syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  <  Y  /\  Y  <  +oo )
)
2524simpld 446 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  <  Y )
266, 19, 4, 22, 25lttrd 9195 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  Y )
276, 4, 26ltled 9185 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  Y )
28 flge0nn0 11188 . . . . . . . . . . . . 13  |-  ( ( Y  e.  RR  /\  0  <_  Y )  -> 
( |_ `  Y
)  e.  NN0 )
294, 27, 28syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( |_ `  Y
)  e.  NN0 )
30 nn0p1nn 10223 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  NN0  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
3129, 30syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  NN )
32 elfzuz 11019 . . . . . . . . . . 11  |-  ( n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
33 nnuz 10485 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
3433uztrn2 10467 . . . . . . . . . . 11  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  n  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  n  e.  NN )
3531, 32, 34syl2an 464 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  NN )
3635nnrpd 10611 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  n  e.  RR+ )
37 pntpbnd.r . . . . . . . . . . 11  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
3837pntrf 21218 . . . . . . . . . 10  |-  R : RR+
--> RR
3938ffvelrni 5836 . . . . . . . . 9  |-  ( n  e.  RR+  ->  ( R `
 n )  e.  RR )
4036, 39syl 16 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  RR )
4135peano2nnd 9981 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  +  1 )  e.  NN )
4235, 41nnmulcld 10011 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
4340, 42nndivred 10012 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  e.  RR )
4443adantlr 696 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  RR )
451, 44fsumrecl 12491 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  ->  sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) )  e.  RR )
4640adantlr 696 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  e.  RR )
47 fveq2 5695 . . . . . . . . . 10  |-  ( i  =  n  ->  ( R `  i )  =  ( R `  n ) )
4847breq2d 4192 . . . . . . . . 9  |-  ( i  =  n  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  n ) ) )
4948rspccva 3019 . . . . . . . 8  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  0  <_  ( R `  n ) )
5049adantll 695 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( R `  n )
)
5142adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
5251nnred 9979 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  RR )
5351nngt0d 10007 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <  (
n  x.  ( n  +  1 ) ) )
54 divge0 9843 . . . . . . 7  |-  ( ( ( ( R `  n )  e.  RR  /\  0  <_  ( R `  n ) )  /\  ( ( n  x.  ( n  +  1 ) )  e.  RR  /\  0  <  ( n  x.  ( n  + 
1 ) ) ) )  ->  0  <_  ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
5546, 50, 52, 53, 54syl22anc 1185 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
561, 44, 55fsumge0 12537 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
0  <_  sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
5745, 56absidd 12188 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
5844, 55absidd 12188 . . . . 5  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i ) )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  =  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )
5958sumeq2dv 12460 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  ->  sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( abs `  ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
6057, 59eqtr4d 2447 . . 3  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) )  -> 
( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
61 fzfid 11275 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  e.  Fin )
6243adantlr 696 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  RR )
6362recnd 9078 . . . . 5  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  CC )
6461, 63fsumneg 12533 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) )
-u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  =  -u sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
6540adantlr 696 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  e.  RR )
6665renegcld 9428 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  -u ( R `  n )  e.  RR )
6747breq1d 4190 . . . . . . . . . . . 12  |-  ( i  =  n  ->  (
( R `  i
)  <_  0  <->  ( R `  n )  <_  0
) )
6867rspccva 3019 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( R `  i
)  <_  0  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
6968adantll 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( R `  n )  <_  0
)
7065le0neg1d 9562 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  <_ 
0  <->  0  <_  -u ( R `  n )
) )
7169, 70mpbid 202 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  -u ( R `  n )
)
7242adantlr 696 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  NN )
7372nnred 9979 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  RR )
7472nngt0d 10007 . . . . . . . . 9  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <  (
n  x.  ( n  +  1 ) ) )
75 divge0 9843 . . . . . . . . 9  |-  ( ( ( -u ( R `
 n )  e.  RR  /\  0  <_  -u ( R `  n
) )  /\  (
( n  x.  (
n  +  1 ) )  e.  RR  /\  0  <  ( n  x.  ( n  +  1 ) ) ) )  ->  0  <_  ( -u ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
7666, 71, 73, 74, 75syl22anc 1185 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  ( -u ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
7740recnd 9078 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  n )  e.  CC )
7842nncnd 9980 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  e.  CC )
7942nnne0d 10008 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( n  x.  ( n  +  1 ) )  =/=  0
)
8077, 78, 79divnegd 9767 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -u ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  =  ( -u ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
8180adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  -u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  =  (
-u ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
8276, 81breqtrrd 4206 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  0  <_  -u (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
8362le0neg1d 9562 . . . . . . 7  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) )  <_ 
0  <->  0  <_  -u (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
8482, 83mpbird 224 . . . . . 6  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  <_  0
)
8562, 84absnidd 12179 . . . . 5  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  =  -u (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )
8685sumeq2dv 12460 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) )  =  sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )
-u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
8761, 62fsumrecl 12491 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) )  e.  RR )
8862renegcld 9428 . . . . . . . 8  |-  ( ( ( ph  /\  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 )  /\  n  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) )  ->  -u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) )  e.  RR )
8961, 88, 82fsumge0 12537 . . . . . . 7  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  0  <_  sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) )
-u ( ( R `
 n )  / 
( n  x.  (
n  +  1 ) ) ) )
9089, 64breqtrd 4204 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  0  <_  -u sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
9187le0neg1d 9562 . . . . . 6  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( sum_ n  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) )  <_  0  <->  0  <_  -u sum_ n  e.  ( ( ( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( ( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
9290, 91mpbird 224 . . . . 5  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) )  <_  0 )
9387, 92absnidd 12179 . . . 4  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  -u sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( ( R `  n )  /  (
n  x.  ( n  +  1 ) ) ) )
9464, 86, 933eqtr4rd 2455 . . 3  |-  ( (
ph  /\  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 )  ->  ( abs `  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) ( ( R `  n )  /  ( n  x.  ( n  +  1 ) ) ) )  =  sum_ n  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ( abs `  (
( R `  n
)  /  ( n  x.  ( n  + 
1 ) ) ) ) )
95 pntpbnd1.c . . . . . . . . . . . . 13  |-  C  =  ( A  +  2 )
96 pntpbnd1.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  RR+ )
97 2rp 10581 . . . . . . . . . . . . . 14  |-  2  e.  RR+
98 rpaddcl 10596 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR+  /\  2  e.  RR+ )  ->  ( A  +  2 )  e.  RR+ )
9996, 97, 98sylancl 644 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A  +  2 )  e.  RR+ )
10095, 99syl5eqel 2496 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  RR+ )
101100, 15rpdivcld 10629 . . . . . . . . . . 11  |-  ( ph  ->  ( C  /  E
)  e.  RR+ )
102101rpred 10612 . . . . . . . . . 10  |-  ( ph  ->  ( C  /  E
)  e.  RR )
103102reefcld 12653 . . . . . . . . 9  |-  ( ph  ->  ( exp `  ( C  /  E ) )  e.  RR )
104 pnfxr 10677 . . . . . . . . 9  |-  +oo  e.  RR*
105 icossre 10955 . . . . . . . . 9  |-  ( ( ( exp `  ( C  /  E ) )  e.  RR  /\  +oo  e.  RR* )  ->  (
( exp `  ( C  /  E ) ) [,)  +oo )  C_  RR )
106103, 104, 105sylancl 644 . . . . . . . 8  |-  ( ph  ->  ( ( exp `  ( C  /  E ) ) [,)  +oo )  C_  RR )
107 pntpbnd1.k . . . . . . . 8  |-  ( ph  ->  K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo ) )
108106, 107sseldd 3317 . . . . . . 7  |-  ( ph  ->  K  e.  RR )
109108, 4remulcld 9080 . . . . . 6  |-  ( ph  ->  ( K  x.  Y
)  e.  RR )
1104recnd 9078 . . . . . . . . 9  |-  ( ph  ->  Y  e.  CC )
111110mulid2d 9070 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  =  Y )
112 1re 9054 . . . . . . . . . . 11  |-  1  e.  RR
113112a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  RR )
114 efgt1 12680 . . . . . . . . . . 11  |-  ( ( C  /  E )  e.  RR+  ->  1  < 
( exp `  ( C  /  E ) ) )
115101, 114syl 16 . . . . . . . . . 10  |-  ( ph  ->  1  <  ( exp `  ( C  /  E
) ) )
116 elicopnf 10964 . . . . . . . . . . . . 13  |-  ( ( exp `  ( C  /  E ) )  e.  RR  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,) 
+oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
117103, 116syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo )  <->  ( K  e.  RR  /\  ( exp `  ( C  /  E
) )  <_  K
) ) )
118117simplbda 608 . . . . . . . . . . 11  |-  ( (
ph  /\  K  e.  ( ( exp `  ( C  /  E ) ) [,)  +oo ) )  -> 
( exp `  ( C  /  E ) )  <_  K )
119107, 118mpdan 650 . . . . . . . . . 10  |-  ( ph  ->  ( exp `  ( C  /  E ) )  <_  K )
120113, 103, 108, 115, 119ltletrd 9194 . . . . . . . . 9  |-  ( ph  ->  1  <  K )
121 ltmul1 9824 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  K  e.  RR  /\  ( Y  e.  RR  /\  0  <  Y ) )  -> 
( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
122113, 108, 4, 26, 121syl112anc 1188 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  K  <->  ( 1  x.  Y )  <  ( K  x.  Y ) ) )
123120, 122mpbid 202 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  Y
)  <  ( K  x.  Y ) )
124111, 123eqbrtrrd 4202 . . . . . . 7  |-  ( ph  ->  Y  <  ( K  x.  Y ) )
1254, 109, 124ltled 9185 . . . . . 6  |-  ( ph  ->  Y  <_  ( K  x.  Y ) )
126 flword2 11183 . . . . . 6  |-  ( ( Y  e.  RR  /\  ( K  x.  Y
)  e.  RR  /\  Y  <_  ( K  x.  Y ) )  -> 
( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
1274, 109, 125, 126syl3anc 1184 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  Y ) ) )
128109flcld 11170 . . . . . 6  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ZZ )
129 uzid 10464 . . . . . 6  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ZZ  ->  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y
) ) ) )
130128, 129syl 16 . . . . 5  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) )
131 elfzuzb 11017 . . . . 5  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ( |_
`  Y ) ... ( |_ `  ( K  x.  Y )
) )  <->  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  /\  ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  ( K  x.  Y ) ) ) ) )
132127, 130, 131sylanbrc 646 . . . 4  |-  ( ph  ->  ( |_ `  ( K  x.  Y )
)  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y
) ) ) )
133 oveq2 6056 . . . . . . . 8  |-  ( x  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) ) )
134133raleqdv 2878 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i ) ) )
135133raleqdv 2878 . . . . . . 7  |-  ( x  =  ( |_ `  Y )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0 ) )
136134, 135orbi12d 691 . . . . . 6  |-  ( x  =  ( |_ `  Y )  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 ) ) )
137136imbi2d 308 . . . . 5  |-  ( x  =  ( |_ `  Y )  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 ) ) ) )
138 oveq2 6056 . . . . . . . 8  |-  ( x  =  m  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... m ) )
139138raleqdv 2878 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )
) )
140138raleqdv 2878 . . . . . . 7  |-  ( x  =  m  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) ( R `  i )  <_  0
) )
141139, 140orbi12d 691 . . . . . 6  |-  ( x  =  m  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0 ) ) )
142141imbi2d 308 . . . . 5  |-  ( x  =  m  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0 ) ) ) )
143 oveq2 6056 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) )
144143raleqdv 2878 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )
) )
145143raleqdv 2878 . . . . . . 7  |-  ( x  =  ( m  + 
1 )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) ( R `  i )  <_  0
) )
146144, 145orbi12d 691 . . . . . 6  |-  ( x  =  ( m  + 
1 )  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... (
m  +  1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) ) ( R `  i
)  <_  0 ) ) )
147146imbi2d 308 . . . . 5  |-  ( x  =  ( m  + 
1 )  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0 ) ) ) )
148 oveq2 6056 . . . . . . . 8  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ( |_ `  Y )  +  1 ) ... x )  =  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) ) )
149148raleqdv 2878 . . . . . . 7  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) 0  <_  ( R `  i )  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i ) ) )
150148raleqdv 2878 . . . . . . 7  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0  <->  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ( R `  i
)  <_  0 ) )
151149, 150orbi12d 691 . . . . . 6  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... x
) 0  <_  ( R `  i )  \/  A. i  e.  ( ( ( |_ `  Y )  +  1 ) ... x ) ( R `  i
)  <_  0 )  <-> 
( A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 ) ) )
152151imbi2d 308 . . . . 5  |-  ( x  =  ( |_ `  ( K  x.  Y
) )  ->  (
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... x ) ( R `  i )  <_  0 ) )  <-> 
( ph  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  ( K  x.  Y
) ) ) ( R `  i )  <_  0 ) ) ) )
153 elfzle3 11027 . . . . . . . . 9  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) )
154 elfzel2 11021 . . . . . . . . . . . 12  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  ZZ )
155154zred 10339 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  e.  RR )
156155ltp1d 9905 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( |_ `  Y )  < 
( ( |_ `  Y )  +  1 ) )
157 peano2re 9203 . . . . . . . . . . . 12  |-  ( ( |_ `  Y )  e.  RR  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
158155, 157syl 16 . . . . . . . . . . 11  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  +  1 )  e.  RR )
159155, 158ltnled 9184 . . . . . . . . . 10  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  (
( |_ `  Y
)  <  ( ( |_ `  Y )  +  1 )  <->  -.  (
( |_ `  Y
)  +  1 )  <_  ( |_ `  Y ) ) )
160156, 159mpbid 202 . . . . . . . . 9  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  -.  ( ( |_ `  Y )  +  1 )  <_  ( |_ `  Y ) )
161153, 160pm2.21dd 101 . . . . . . . 8  |-  ( i  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  Y
) )  ->  ( R `  i )  <_  0 )
162161rgen 2739 . . . . . . 7  |-  A. i  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  Y ) ) ( R `  i
)  <_  0
163162olci 381 . . . . . 6  |-  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( |_ `  Y ) ) ( R `  i )  <_  0 )
164163a1ii 25 . . . . 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 ) ) )
165 elfzofz 11117 . . . . . . . . . 10  |-  ( m  e.  ( ( |_
`  Y )..^ ( |_ `  ( K  x.  Y ) ) )  ->  m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) ) )
166 elfzp12 11089 . . . . . . . . . . 11  |-  ( ( |_ `  ( K  x.  Y ) )  e.  ( ZZ>= `  ( |_ `  Y ) )  ->  ( m  e.  ( ( |_ `  Y ) ... ( |_ `  ( K  x.  Y ) ) )  <-> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
167127, 166syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( ( |_ `  Y
) ... ( |_ `  ( K  x.  Y
) ) )  <->  ( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) ) )
168165, 167syl5ib 211 . . . . . . . . 9  |-  ( ph  ->  ( m  e.  ( ( |_ `  Y
)..^ ( |_ `  ( K  x.  Y
) ) )  -> 
( m  =  ( |_ `  Y )  \/  m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_
`  ( K  x.  Y ) ) ) ) ) )
169168imp 419 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ( |_ `  Y )..^ ( |_ `  ( K  x.  Y
) ) ) )  ->  ( m  =  ( |_ `  Y
)  \/  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) ) )
17031nnrpd 10611 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  RR+ )
17138ffvelrni 5836 . . . . . . . . . . . . . 14  |-  ( ( ( |_ `  Y
)  +  1 )  e.  RR+  ->  ( R `
 ( ( |_
`  Y )  +  1 ) )  e.  RR )
172170, 171syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R `  (
( |_ `  Y
)  +  1 ) )  e.  RR )
1736, 172letrid 9187 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  (
( |_ `  Y
)  +  1 ) )  <_  0 ) )
174173adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( 0  <_  ( R `  ( ( |_ `  Y )  +  1 ) )  \/  ( R `  ( ( |_ `  Y )  +  1 ) )  <_ 
0 ) )
175 oveq1 6055 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( |_ `  Y )  ->  (
m  +  1 )  =  ( ( |_
`  Y )  +  1 ) )
176175oveq2d 6064 . . . . . . . . . . . . . . 15  |-  ( m  =  ( |_ `  Y )  ->  (
( ( |_ `  Y )  +  1 ) ... ( m  +  1 ) )  =  ( ( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) ) )
1774flcld 11170 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( |_ `  Y
)  e.  ZZ )
178177peano2zd 10342 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( |_ `  Y )  +  1 )  e.  ZZ )
179 fzsn 11058 . . . . . . . . . . . . . . . 16  |-  ( ( ( |_ `  Y
)  +  1 )  e.  ZZ  ->  (
( ( |_ `  Y )  +  1 ) ... ( ( |_ `  Y )  +  1 ) )  =  { ( ( |_ `  Y )  +  1 ) } )
180178, 179syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( |_
`  Y )  +  1 ) ... (
( |_ `  Y
)  +  1 ) )  =  { ( ( |_ `  Y
)  +  1 ) } )
181176, 180sylan9eqr 2466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  { ( ( |_
`  Y )  +  1 ) } )
182181raleqdv 2878 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) } 0  <_  ( R `  i ) ) )
183 ovex 6073 . . . . . . . . . . . . . 14  |-  ( ( |_ `  Y )  +  1 )  e. 
_V
184 fveq2 5695 . . . . . . . . . . . . . . 15  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  ( R `  i )  =  ( R `  ( ( |_ `  Y )  +  1 ) ) )
185184breq2d 4192 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
186183, 185ralsn 3817 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( |_ `  Y
)  +  1 ) } 0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) )
187182, 186syl6bb 253 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  <->  0  <_  ( R `  ( ( |_ `  Y )  +  1 ) ) ) )
188181raleqdv 2878 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  A. i  e.  { ( ( |_
`  Y )  +  1 ) }  ( R `  i )  <_  0 ) )
189184breq1d 4190 . . . . . . . . . . . . . 14  |-  ( i  =  ( ( |_
`  Y )  +  1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
190183, 189ralsn 3817 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
( |_ `  Y
)  +  1 ) }  ( R `  i )  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0 )
191188, 190syl6bb 253 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0  <->  ( R `  ( ( |_ `  Y )  +  1 ) )  <_  0
) )
192187, 191orbi12d 691 . . . . . . . . . . 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 ) ) )
193174, 192mpbird 224 . . . . . . . . . 10  |-  ( (
ph  /\  m  =  ( |_ `  Y ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) 0  <_  ( R `  i )  \/  A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) ) ( R `  i )  <_  0 ) )
194193a1d 23 . . . . . . . . 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 ) ) )
195 elfzuz 11019 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
196195adantl 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )
197 eluzfz2 11029 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
198196, 197syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  ( ( ( |_
`  Y )  +  1 ) ... m
) )
199 fveq2 5695 . . . . . . . . . . . . . . . . 17  |-  ( i  =  m  ->  ( R `  i )  =  ( R `  m ) )
200199breq2d 4192 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  m ) ) )
201200rspcv 3016 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
202198, 201syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  m
) ) )
203 pntpbnd1.3 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
204203adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  E. y  e.  NN  ( ( Y  <  y  /\  y  <_  ( K  x.  Y
) )  /\  ( abs `  ( ( R `
 y )  / 
y ) )  <_  E ) )
20533uztrn2 10467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( |_ `  Y )  +  1 )  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  Y )  +  1 ) ) )  ->  m  e.  NN )
20631, 195, 205syl2an 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  NN )
207206adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  m  e.  NN )
208 elfzle1 11024 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  (
( |_ `  Y
)  +  1 )  <_  m )
209208adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  +  1 )  <_  m
)
210 elfzelz 11023 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  e.  ZZ )
211 zltp1le 10289 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( |_ `  Y
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( ( |_ `  Y )  <  m  <->  ( ( |_ `  Y
)  +  1 )  <_  m ) )
212177, 210, 211syl2an 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( |_ `  Y )  < 
m  <->  ( ( |_
`  Y )  +  1 )  <_  m
) )
213209, 212mpbird 224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( |_ `  Y )  <  m
)
214 fllt 11178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Y  e.  RR  /\  m  e.  ZZ )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m ) )
2154, 210, 214syl2an 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  <->  ( |_ `  Y )  <  m
) )
216213, 215mpbird 224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  Y  <  m )
217 elfzle2 11025 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... ( |_ `  ( K  x.  Y )
) )  ->  m  <_  ( |_ `  ( K  x.  Y )
) )
218217adantl 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( |_ `  ( K  x.  Y ) ) )
219 flge 11177 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( K  x.  Y
)  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  ( K  x.  Y )  <->  m  <_  ( |_ `  ( K  x.  Y
) ) ) )
220109, 210, 219syl2an 464 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  <_  ( K  x.  Y
)  <->  m  <_  ( |_
`  ( K  x.  Y ) ) ) )
221218, 220mpbird 224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  <_  ( K  x.  Y ) )
222216, 221jca 519 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( Y  <  m  /\  m  <_ 
( K  x.  Y
) ) )
223222adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) )
22410ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  E  e.  ( 0 (,) 1 ) )
2253ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  ->  Y  e.  ( X (,)  +oo ) )
226 simpr 448 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
22737, 224, 7, 225, 207, 223, 226pntpbnd1a 21240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( abs `  ( R `  m
) )  <_  ( abs `  ( ( R `
 ( m  + 
1 ) )  -  ( R `  m ) ) ) )  -> 
( abs `  (
( R `  m
)  /  m ) )  <_  E )
228 breq2 4184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( Y  <  y  <->  Y  <  m ) )
229 breq1 4183 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  (
y  <_  ( K  x.  Y )  <->  m  <_  ( K  x.  Y ) ) )
230228, 229anbi12d 692 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( Y  <  y  /\  y  <_  ( K  x.  Y ) )  <-> 
( Y  <  m  /\  m  <_  ( K  x.  Y ) ) ) )
231 fveq2 5695 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  ( R `  y )  =  ( R `  m ) )
232 id 20 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  m  ->  y  =  m )
233231, 232oveq12d 6066 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  m  ->  (
( R `  y
)  /  y )  =  ( ( R `
 m )  /  m ) )
234233fveq2d 5699 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  m  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  m
)  /  m ) ) )
235234breq1d 4190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  m  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  E  <->  ( abs `  ( ( R `  m )  /  m
) )  <_  E
) )
236230, 235anbi12d 692 . . . . . . . . . . . . . . . . . . . 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 ) ) )
237236rspcev 3020 . . . . . . . . . . . . . . . . . . 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 ) )
238207, 223, 227, 237syl12anc 1182 . . . . . . . . . . . . . . . . . 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
) )
239204, 238mtand 641 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  -.  ( abs `  ( R `  m ) )  <_ 
( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
240239adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
241206nnrpd 10611 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  m  e.  RR+ )
24238ffvelrni 5836 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  RR+  ->  ( R `
 m )  e.  RR )
243241, 242syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  m )  e.  RR )
244243adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  RR )
245244recnd 9078 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  e.  CC )
246245subid1d 9364 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  =  ( R `  m ) )
247206peano2nnd 9981 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  NN )
248247nnrpd 10611 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( m  +  1 )  e.  RR+ )
24938ffvelrni 5836 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  e.  RR+  ->  ( R `
 ( m  + 
1 ) )  e.  RR )
250248, 249syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( R `  ( m  +  1 ) )  e.  RR )
251250adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
2525a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  e.  RR )
253 letric 9138 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  ( R `  ( m  +  1 ) )  e.  RR )  -> 
( 0  <_  ( R `  ( m  +  1 ) )  \/  ( R `  ( m  +  1
) )  <_  0
) )
2545, 250, 253sylancr 645 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  ( m  +  1
) )  \/  ( R `  ( m  +  1 ) )  <_  0 ) )
255254ord 367 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  0  <_  ( R `  ( m  +  1
) )  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
256255imp 419 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  0  <_  ( R `  (
m  +  1 ) ) )  ->  ( R `  ( m  +  1 ) )  <_  0 )
257256adantrl 697 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  0
)
258251, 252, 244, 257lesub2dd 9607 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( ( R `
 m )  - 
0 )  <_  (
( R `  m
)  -  ( R `
 ( m  + 
1 ) ) ) )
259246, 258eqbrtrrd 4202 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  m )  <_  (
( R `  m
)  -  ( R `
 ( m  + 
1 ) ) ) )
260 simprl 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  0  <_  ( R `  m )
)
261244, 260absidd 12188 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( abs `  ( R `  m )
)  =  ( R `
 m ) )
262251, 252, 244, 257, 260letrd 9191 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( 0  <_  ( R `  m )  /\  -.  0  <_  ( R `  ( m  +  1
) ) ) )  ->  ( R `  ( m  +  1
) )  <_  ( R `  m )
)
263251, 244, 262abssuble0d 12198 . . . . . . . . . . . . . . . . . 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
) ) ) )
264259, 261, 2633brtr4d 4210 . . . . . . . . . . . . . . . . 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 )
) ) )
265264expr 599 . . . . . . . . . . . . . . . 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 )
) ) ) )
266240, 265mt3d 119 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  0  <_ 
( R `  m
) )  ->  0  <_  ( R `  (
m  +  1 ) ) )
267266ex 424 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( 0  <_  ( R `  m )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
268202, 267syld 42 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) 0  <_  ( R `  i )  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
269 ovex 6073 . . . . . . . . . . . . . 14  |-  ( m  +  1 )  e. 
_V
270 fveq2 5695 . . . . . . . . . . . . . . 15  |-  ( i  =  ( m  + 
1 )  ->  ( R `  i )  =  ( R `  ( m  +  1
) ) )
271270breq2d 4192 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1 ) ) ) )
272269, 271ralsn 3817 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
m  +  1 ) } 0  <_  ( R `  i )  <->  0  <_  ( R `  ( m  +  1
) ) )
273268, 272syl6ibr 219 . . . . . . . . . . . 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 ) ) )
274273ancld 537 . . . . . . . . . . 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 )
) ) )
275 fzsuc 11060 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  (
( |_ `  Y
)  +  1 ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
276196, 275syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( (
( |_ `  Y
)  +  1 ) ... ( m  + 
1 ) )  =  ( ( ( ( |_ `  Y )  +  1 ) ... m )  u.  {
( m  +  1 ) } ) )
277276raleqdv 2878 . . . . . . . . . . . 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 ) ) )
278 ralunb 3496 . . . . . . . . . . . 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 )
) )
279277, 278syl6bb 253 . . . . . . . . . . 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 )
) ) )
280274, 279sylibrd 226 . . . . . . . . . 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 )
) )
281199breq1d 4190 . . . . . . . . . . . . . . . 16  |-  ( i  =  m  ->  (
( R `  i
)  <_  0  <->  ( R `  m )  <_  0
) )
282281rspcv 3016 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ( ( |_ `  Y )  +  1 ) ... m )  ->  ( A. i  e.  (
( ( |_ `  Y )  +  1 ) ... m ) ( R `  i
)  <_  0  ->  ( R `  m )  <_  0 ) )
283198, 282syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  m )  <_  0 ) )
284239adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  -.  ( abs `  ( R `
 m ) )  <_  ( abs `  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) ) )
285255con1d 118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( -.  ( R `  ( m  +  1 ) )  <_  0  ->  0  <_  ( R `  (
m  +  1 ) ) ) )
286285imp 419 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  -.  ( R `  ( m  +  1 ) )  <_  0 )  -> 
0  <_  ( R `  ( m  +  1 ) ) )
287286adantrl 697 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  <_  ( R `  ( m  +  1 ) ) )
288243adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  RR )
289288renegcld 9428 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  e.  RR )
290250adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  RR )
291289, 290addge02d 9579 . . . . . . . . . . . . . . . . . . . 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 )
) ) )
292287, 291mpbid 202 . . . . . . . . . . . . . . . . . . 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 )
) )
293290recnd 9078 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  ( m  +  1
) )  e.  CC )
294288recnd 9078 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  e.  CC )
295293, 294negsubd 9381 . . . . . . . . . . . . . . . . . . 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 )
) )
296292, 295breqtrd 4204 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  -u ( R `  m )  <_  (
( R `  (
m  +  1 ) )  -  ( R `
 m ) ) )
297 simprl 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  0
)
298288, 297absnidd 12179 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( abs `  ( R `  m )
)  =  -u ( R `  m )
)
2995a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  0  e.  RR )
300288, 299, 290, 297, 287letrd 9191 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( ( R `  m )  <_  0  /\  -.  ( R `  ( m  +  1 ) )  <_  0 ) )  ->  ( R `  m )  <_  ( R `  ( m  +  1 ) ) )
301288, 290, 300abssubge0d 12197 . . . . . . . . . . . . . . . . . 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 ) ) )
302296, 298, 3013brtr4d 4210 . . . . . . . . . . . . . . . . 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 )
) ) )
303302expr 599 . . . . . . . . . . . . . . . 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 ) ) ) ) )
304284, 303mt3d 119 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  /\  ( R `
 m )  <_ 
0 )  ->  ( R `  ( m  +  1 ) )  <_  0 )
305304ex 424 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( ( R `  m )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0
) )
306283, 305syld 42 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ( ( |_
`  Y )  +  1 ) ... ( |_ `  ( K  x.  Y ) ) ) )  ->  ( A. i  e.  ( (
( |_ `  Y
)  +  1 ) ... m ) ( R `  i )  <_  0  ->  ( R `  ( m  +  1 ) )  <_  0 ) )
307270breq1d 4190 . . . . . . . . . . . . . 14  |-  ( i  =  ( m  + 
1 )  ->  (
( R `  i
)  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0
) )
308269, 307ralsn 3817 . . . . . . . . . . . . 13  |-  ( A. i  e.  { (
m  +  1 ) }  ( R `  i )  <_  0  <->  ( R `  ( m  +  1 ) )  <_  0 )
309306, 308syl6ibr 219 . . . . . . . . . . . 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 ) )
310309ancld 537 . . . . . . . . . . 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
) ) )
311276raleqdv 2878 . . . . . . . . . . . 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