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

Theorem pntrlog2bndlem5 22962
Description: Lemma for pntrlog2bnd 22965. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Hypotheses
Ref Expression
pntsval.1  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
pntrlog2bnd.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
pntrlog2bnd.t  |-  T  =  ( a  e.  RR  |->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 ) )
pntrlog2bndlem5.1  |-  ( ph  ->  B  e.  RR+ )
pntrlog2bndlem5.2  |-  ( ph  ->  A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y ) )  <_  B )
Assertion
Ref Expression
pntrlog2bndlem5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x ) )  e.  <_O(1) )
Distinct variable groups:    i, a, n, x, y    B, n, x, y    ph, n, x    S, n, x, y    R, n, x, y    T, n
Allowed substitution hints:    ph( y, i, a)    B( i, a)    R( i, a)    S( i, a)    T( x, y, i, a)

Proof of Theorem pntrlog2bndlem5
StepHypRef Expression
1 elioore 11440 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
21adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
3 1rp 11105 . . . . . . . . . . . . 13  |-  1  e.  RR+
43a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
5 1red 9511 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
6 eliooord 11465 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) +oo )  ->  ( 1  <  x  /\  x  < +oo ) )
76adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  <  x  /\  x  < +oo ) )
87simpld 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  x )
95, 2, 8ltled 9632 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 11172 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
11 pntrlog2bnd.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1211pntrf 22944 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1312ffvelrni 5950 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1410, 13syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  RR )
1514recnd 9522 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  CC )
1615abscld 13039 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
1716recnd 9522 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  CC )
1810relogcld 22204 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
1918recnd 9522 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
2017, 19mulcld 9516 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
21 2cnd 10504 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  CC )
222, 8rplogcld 22210 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
2322rpne0d 11142 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
2421, 19, 23divcld 10217 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
25 fzfid 11911 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
2610adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
27 elfznn 11594 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2827adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
2928nnrpd 11136 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
3026, 29rpdivcld 11154 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3112ffvelrni 5950 . . . . . . . . . . . . 13  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
3230, 31syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
3332recnd 9522 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
3433abscld 13039 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
3529relogcld 22204 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
36 1red 9511 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
3735, 36readdcld 9523 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  RR )
3834, 37remulcld 9524 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  RR )
3938recnd 9522 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  CC )
4025, 39fsumcl 13327 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  CC )
4124, 40mulcld 9516 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )  e.  CC )
4220, 41subcld 9829 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  e.  CC )
4334recnd 9522 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  CC )
4425, 43fsumcl 13327 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  CC )
4524, 44mulcld 9516 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  CC )
462recnd 9522 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
4710rpne0d 11142 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
4842, 45, 46, 47divdird 10255 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )  /  x )  =  ( ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x )  +  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x ) ) )
4916, 18remulcld 9524 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
5049recnd 9522 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
5150, 41, 45subsubd 9857 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) ) )  =  ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) ) )
5224, 40, 44subdid 9910 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )  =  ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) ) )
5325, 39, 43fsumsub 13372 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  x.  (
( log `  n
)  +  1 ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )
5437recnd 9522 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  CC )
55 1cnd 9512 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
5643, 54, 55subdid 9910 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( ( log `  n )  +  1 )  -  1 ) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  (
( abs `  ( R `  ( x  /  n ) ) )  x.  1 ) ) )
5735recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
5857, 55pncand 9830 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  n
)  +  1 )  -  1 )  =  ( log `  n
) )
5958oveq2d 6215 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( ( log `  n )  +  1 )  -  1 ) )  =  ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) )
6043mulid1d 9513 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  1 )  =  ( abs `  ( R `
 ( x  /  n ) ) ) )
6160oveq2d 6215 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  (
( abs `  ( R `  ( x  /  n ) ) )  x.  1 ) )  =  ( ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  ( abs `  ( R `  ( x  /  n
) ) ) ) )
6256, 59, 613eqtr3rd 2504 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  ( abs `  ( R `  ( x  /  n
) ) ) )  =  ( ( abs `  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) )
6362sumeq2dv 13297 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  x.  (
( log `  n
)  +  1 ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) )
6453, 63eqtr3d 2497 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) )
6564oveq2d 6215 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )
6652, 65eqtr3d 2497 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )
6766oveq2d 6215 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) ) )  =  ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) ) )
6851, 67eqtr3d 2497 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( abs `  ( R `  x
) )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )  =  ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) ) ) )
6968oveq1d 6214 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) ) )  /  x )  =  ( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x ) )
7048, 69eqtr3d 2497 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x )  +  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x ) )  =  ( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x ) )
7170mpteq2dva 4485 . 2  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x )  +  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x ) ) )  =  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x ) ) )
72 2re 10501 . . . . . . . 8  |-  2  e.  RR
7372a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
7473, 22rerpdivcld 11164 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
7525, 38fsumrecl 13328 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  RR )
7674, 75remulcld 9524 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )  e.  RR )
7749, 76resubcld 9886 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  e.  RR )
7877, 10rerpdivcld 11164 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( abs `  ( R `  x
) )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x )  e.  RR )
7925, 34fsumrecl 13328 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  RR )
8074, 79remulcld 9524 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  RR )
8180, 10rerpdivcld 11164 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  e.  RR )
82 1red 9511 . . . 4  |-  ( ph  ->  1  e.  RR )
83 pntsval.1 . . . . . 6  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
84 pntrlog2bnd.t . . . . . 6  |-  T  =  ( a  e.  RR  |->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 ) )
8583, 11, 84pntrlog2bndlem4 22961 . . . . 5  |-  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  /  x ) )  e.  <_O(1)
8685a1i 11 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  /  x ) )  e.  <_O(1) )
8728nnred 10447 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
88 simpl 457 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
a  e.  RR )
89 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
a  e.  RR+ )
9089relogcld 22204 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( log `  a
)  e.  RR )
9188, 90remulcld 9524 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
92 0red 9497 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
9391, 92ifclda 3928 . . . . . . . . . . . . 13  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
9484, 93fmpti 5974 . . . . . . . . . . . 12  |-  T : RR
--> RR
9594ffvelrni 5950 . . . . . . . . . . 11  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
9687, 95syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
9787, 36resubcld 9886 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
9894ffvelrni 5950 . . . . . . . . . . 11  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
9997, 98syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
10096, 99resubcld 9886 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
10134, 100remulcld 9524 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
10225, 101fsumrecl 13328 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
10374, 102remulcld 9524 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) )  e.  RR )
10449, 103resubcld 9886 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  e.  RR )
105104, 10rerpdivcld 11164 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( abs `  ( R `  x
) )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  /  x )  e.  RR )
106 2rp 11106 . . . . . . . . . . 11  |-  2  e.  RR+
107106a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR+ )
108107rpge0d 11141 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  2 )
10973, 22, 108divge0d 11173 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( 2  /  ( log `  x ) ) )
11033absge0d 13047 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( R `
 ( x  /  n ) ) ) )
11129adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  n  e.  RR+ )
112111rpcnd 11139 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  n  e.  CC )
11357adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  n )  e.  CC )
114112, 113mulcld 9516 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( log `  n ) )  e.  CC )
115 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  1  <  n )
116 1re 9495 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR
117111rpred 11137 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  n  e.  RR )
118 difrp 11134 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  RR  /\  n  e.  RR )  ->  ( 1  <  n  <->  ( n  -  1 )  e.  RR+ ) )
119116, 117, 118sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
1  <  n  <->  ( n  -  1 )  e.  RR+ ) )
120115, 119mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  -  1 )  e.  RR+ )
121120relogcld 22204 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  ( n  - 
1 ) )  e.  RR )
122121recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  ( n  - 
1 ) )  e.  CC )
123112, 122mulcld 9516 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( log `  ( n  -  1 ) ) )  e.  CC )
124114, 123, 122subsubd 9857 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  ( log `  n ) )  -  ( ( n  x.  ( log `  (
n  -  1 ) ) )  -  ( log `  ( n  - 
1 ) ) ) )  =  ( ( ( n  x.  ( log `  n ) )  -  ( n  x.  ( log `  (
n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) ) )
125 rpre 11107 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR+  ->  n  e.  RR )
126 eleq1 2526 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
127 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  a  =  n )
128 fveq2 5798 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
129127, 128oveq12d 6217 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
130126, 129ifbieq1d 3919 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
131 ovex 6224 . . . . . . . . . . . . . . . . . . 19  |-  ( n  x.  ( log `  n
) )  e.  _V
132 c0ex 9490 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  _V
133131, 132ifex 3965 . . . . . . . . . . . . . . . . . 18  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
134130, 84, 133fvmpt 5882 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
135125, 134syl 16 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  ( T `
 n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
136 iftrue 3904 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
137135, 136eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( n  e.  RR+  ->  ( T `
 n )  =  ( n  x.  ( log `  n ) ) )
138111, 137syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( T `  n )  =  ( n  x.  ( log `  n
) ) )
139 rpre 11107 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR+  ->  ( n  -  1 )  e.  RR )
140 eleq1 2526 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  e.  RR+  <->  ( n  -  1 )  e.  RR+ ) )
141 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  a  =  ( n  - 
1 ) )
142 fveq2 5798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  ( log `  a )  =  ( log `  (
n  -  1 ) ) )
143141, 142oveq12d 6217 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  x.  ( log `  a ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
144140, 143ifbieq1d 3919 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( n  - 
1 )  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
145 ovex 6224 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) )  e.  _V
146145, 132ifex 3965 . . . . . . . . . . . . . . . . . . 19  |-  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) ,  0 )  e.  _V
147144, 84, 146fvmpt 5882 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
148139, 147syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  ( T `
 ( n  - 
1 ) )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
149 iftrue 3904 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) ,  0 )  =  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) )
150148, 149eqtrd 2495 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR+  ->  ( T `
 ( n  - 
1 ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
151120, 150syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( T `  ( n  -  1 ) )  =  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) )
152 1cnd 9512 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  1  e.  CC )
153112, 152, 122subdird 9911 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  -  1 )  x.  ( log `  ( n  -  1 ) ) )  =  ( ( n  x.  ( log `  (
n  -  1 ) ) )  -  (
1  x.  ( log `  ( n  -  1 ) ) ) ) )
154122mulid2d 9514 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
1  x.  ( log `  ( n  -  1 ) ) )  =  ( log `  (
n  -  1 ) ) )
155154oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  ( log `  ( n  - 
1 ) ) )  -  ( 1  x.  ( log `  (
n  -  1 ) ) ) )  =  ( ( n  x.  ( log `  (
n  -  1 ) ) )  -  ( log `  ( n  - 
1 ) ) ) )
156151, 153, 1553eqtrd 2499 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( T `  ( n  -  1 ) )  =  ( ( n  x.  ( log `  (
n  -  1 ) ) )  -  ( log `  ( n  - 
1 ) ) ) )
157138, 156oveq12d 6217 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  ( ( n  x.  ( log `  n
) )  -  (
( n  x.  ( log `  ( n  - 
1 ) ) )  -  ( log `  (
n  -  1 ) ) ) ) )
158112, 113, 122subdid 9910 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  =  ( ( n  x.  ( log `  n
) )  -  (
n  x.  ( log `  ( n  -  1 ) ) ) ) )
159158oveq1d 6214 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  =  ( ( ( n  x.  ( log `  n
) )  -  (
n  x.  ( log `  ( n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) ) )
160124, 157, 1593eqtr4d 2505 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  ( ( n  x.  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  +  ( log `  ( n  -  1 ) ) ) )
161111relogcld 22204 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  n )  e.  RR )
162161, 121resubcld 9886 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) )  e.  RR )
163162recnd 9522 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) )  e.  CC )
164112, 152, 163subdird 9911 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  -  1 )  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  =  ( ( n  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  -  ( 1  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) ) ) )
165163mulid2d 9514 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
1  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  =  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )
166165oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  -  ( 1  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) ) )  =  ( ( n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  -  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) ) )
167117, 162remulcld 9524 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  e.  RR )
168167recnd 9522 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  e.  CC )
169168, 113, 122subsub3d 9859 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  -  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  =  ( ( ( n  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  -  ( log `  n ) ) )
170164, 166, 1693eqtrd 2499 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  -  1 )  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  =  ( ( ( n  x.  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  +  ( log `  ( n  -  1 ) ) )  -  ( log `  n ) ) )
171112, 152npcand 9833 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  -  1 )  +  1 )  =  n )
172171fveq2d 5802 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  ( ( n  -  1 )  +  1 ) )  =  ( log `  n
) )
173172oveq1d 6214 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  (
( n  -  1 )  +  1 ) )  -  ( log `  ( n  -  1 ) ) )  =  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )
174 logdifbnd 22519 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  ( ( log `  ( ( n  -  1 )  +  1 ) )  -  ( log `  (
n  -  1 ) ) )  <_  (
1  /  ( n  -  1 ) ) )
175120, 174syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  (
( n  -  1 )  +  1 ) )  -  ( log `  ( n  -  1 ) ) )  <_ 
( 1  /  (
n  -  1 ) ) )
176173, 175eqbrtrrd 4421 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) )  <_ 
( 1  /  (
n  -  1 ) ) )
177 1red 9511 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  1  e.  RR )
178162, 177, 120lemuldiv2d 11183 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( ( n  - 
1 )  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  <_  1  <->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  <_  ( 1  /  ( n  - 
1 ) ) ) )
179176, 178mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  -  1 )  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  <_ 
1 )
180170, 179eqbrtrrd 4421 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( ( n  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  -  ( log `  n ) )  <_  1 )
181167, 121readdcld 9523 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  e.  RR )
182181, 161, 177lesubadd2d 10048 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( ( ( n  x.  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  +  ( log `  ( n  -  1 ) ) )  -  ( log `  n ) )  <_  1  <->  ( (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  <_  (
( log `  n
)  +  1 ) ) )
183180, 182mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  x.  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  <_  (
( log `  n
)  +  1 ) )
184160, 183eqbrtrd 4419 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  <_  ( ( log `  n )  +  1 ) )
185 fveq2 5798 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  n )  =  ( T ` 
1 ) )
186 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  a  =  1 )
187186, 3syl6eqel 2550 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  a  e.  RR+ )
188 iftrue 3904 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
189187, 188syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
190 fveq2 5798 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  1  ->  ( log `  a )  =  ( log `  1
) )
191 log1 22166 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( log `  1 )  =  0
192190, 191syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  ( log `  a )  =  0 )
193186, 192oveq12d 6217 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  ( 1  x.  0 ) )
194 ax-1cn 9450 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
195194mul01i 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  x.  0 )  =  0
196193, 195syl6eq 2511 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  0 )
197189, 196eqtrd 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
198197, 84, 132fvmpt 5882 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  RR  ->  ( T `  1 )  =  0 )
199116, 198ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 1 )  =  0
200185, 199syl6eq 2511 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  n )  =  0 )
201 oveq1 6206 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
202 1m1e0 10500 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  -  1 )  =  0
203201, 202syl6eq 2511 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
204203fveq2d 5802 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  ( T ` 
0 ) )
205 0re 9496 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
206 rpne0 11116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
207206necon2bi 2688 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
208 iffalse 3906 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
209207, 208syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
210209, 84, 132fvmpt 5882 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
211205, 210ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
212204, 211syl6eq 2511 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  0 )
213200, 212oveq12d 6217 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  ( 0  -  0 ) )
214 0m0e0 10541 . . . . . . . . . . . . . . 15  |-  ( 0  -  0 )  =  0
215213, 214syl6eq 2511 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
216215eqcoms 2466 . . . . . . . . . . . . 13  |-  ( 1  =  n  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
217216adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  =  n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
218 0red 9497 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  e.  RR )
21928nnge1d 10474 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
22087, 219logge0d 22211 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  n ) )
22135lep1d 10374 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  <_  (
( log `  n
)  +  1 ) )
222218, 35, 37, 220, 221letrd 9638 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  n
)  +  1 ) )
223222adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  =  n )  ->  0  <_  ( ( log `  n
)  +  1 ) )
224217, 223eqbrtrd 4419 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  =  n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  <_  ( ( log `  n )  +  1 ) )
225 elfzle1 11570 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  1  <_  n )
226225adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
22736, 87leloed 9627 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  n  <->  ( 1  <  n  \/  1  =  n ) ) )
228226, 227mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <  n  \/  1  =  n ) )
229184, 224, 228mpjaodan 784 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
230100, 37, 34, 110, 229lemul2ad 10383 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  <_  (
( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )
23125, 101, 38, 230fsumle 13379 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) )
232102, 75, 74, 109, 231lemul2ad 10383 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) )  <_ 
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )
233103, 76, 49, 232lesub2dd 10066 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  <_  ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) ) )
23477, 104, 10, 233lediv1dd 11191 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( abs `  ( R `  x
) )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x )  <_ 
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  /  x ) )
235234adantrr 716 . . . 4  |-  ( (
ph  /\  ( x  e.  ( 1 (,) +oo )  /\  1  <_  x
) )  ->  (
( ( ( abs `  ( R `  x
) )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x )  <_ 
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  /  x ) )
23682, 86, 105, 78, 235lo1le 13246 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) ) ) )  /  x ) )  e.  <_O(1) )
237106a1i 11 . . . . . . . 8  |-  ( ph  ->  2  e.  RR+ )
238 pntrlog2bndlem5.1 . . . . . . . 8  |-  ( ph  ->  B  e.  RR+ )
239237, 238rpmulcld 11153 . . . . . . 7  |-  ( ph  ->  ( 2  x.  B
)  e.  RR+ )
240239rpred 11137 . . . . . 6  |-  ( ph  ->  ( 2  x.  B
)  e.  RR )
241240adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  B )  e.  RR )
2425, 22rerpdivcld 11164 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
2435, 242readdcld 9523 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
244 ioossre 11467 . . . . . 6  |-  ( 1 (,) +oo )  C_  RR
245 lo1const 13215 . . . . . 6  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  (
2  x.  B )  e.  RR )  -> 
( x  e.  ( 1 (,) +oo )  |->  ( 2  x.  B
) )  e.  <_O(1) )
246244, 240, 245sylancr 663 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 2  x.  B
) )  e.  <_O(1) )
247 lo1const 13215 . . . . . . 7  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  1  e.  RR )  ->  (
x  e.  ( 1 (,) +oo )  |->  1 )  e.  <_O(1) )
248244, 82, 247sylancr 663 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  1 )  e.  <_O(1) )
249 divlogrlim 22212 . . . . . . . 8  |-  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
250 rlimo1 13211 . . . . . . . 8  |-  ( ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  ~~> r  0  ->  (
x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
251249, 250mp1i 12 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
252242, 251o1lo1d 13134 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  <_O(1) )
2535, 242, 248, 252lo1add 13221 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  <_O(1) )
254239adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  B )  e.  RR+ )
255254rpge0d 11141 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( 2  x.  B
) )
256241, 243, 246, 253, 255lo1mul 13222 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( 2  x.  B )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  <_O(1) )
257241, 243remulcld 9524 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
25879, 10rerpdivcld 11164 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  e.  RR )
25918, 5readdcld 9523 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
260238adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  B  e.  RR+ )
261260rpred 11137 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  B  e.  RR )
262259, 261remulcld 9524 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  +  1 )  x.  B )  e.  RR )
26328nnrecred 10477 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
26425, 263fsumrecl 13328 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
265264, 261remulcld 9524 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  e.  RR )
26634, 26rerpdivcld 11164 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  e.  RR )
267261adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  RR )
268263, 267remulcld 9524 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  /  n )  x.  B )  e.  RR )
26930rpcnd 11139 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
27030rpne0d 11142 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  =/=  0
)
27133, 269, 270absdivd 13058 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( abs `  (
x  /  n ) ) ) )
2722adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
273272, 28nndivred 10480 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
27430rpge0d 11141 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  n ) )
275273, 274absidd 13026 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  /  n
) )  =  ( x  /  n ) )
276275oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  / 
( abs `  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
277271, 276eqtrd 2495 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
27846adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
27987recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
28047adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
28128nnne0d 10476 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
28243, 278, 279, 280, 281divdiv2d 10249 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  / 
( x  /  n
) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  x.  n )  /  x ) )
28343, 279, 278, 280div23d 10254 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  x.  n )  /  x )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n ) )
284277, 282, 2833eqtrd 2499 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n ) )
285 pntrlog2bndlem5.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y ) )  <_  B )
286285ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  ( abs `  (
( R `  y
)  /  y ) )  <_  B )
287 fveq2 5798 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  ( R `  y )  =  ( R `  ( x  /  n
) ) )
288 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
289287, 288oveq12d 6217 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  /  n )  ->  (
( R `  y
)  /  y )  =  ( ( R `
 ( x  /  n ) )  / 
( x  /  n
) ) )
290289fveq2d 5802 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  /  n )  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
291290breq1d 4409 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  /  n )  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  B  <->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
) )
292291rspcv 3173 . . . . . . . . . . . . . 14  |-  ( ( x  /  n )  e.  RR+  ->  ( A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y
) )  <_  B  ->  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) )  <_  B )
)
29330, 286, 292sylc 60 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
)
294284, 293eqbrtrrd 4421 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n )  <_  B
)
295266, 267, 29lemuldivd 11182 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n )  <_  B  <->  ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  <_ 
( B  /  n
) ) )
296294, 295mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  ( B  /  n ) )
297267recnd 9522 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  CC )
298297, 279, 281divrec2d 10221 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( B  /  n )  =  ( ( 1  /  n
)  x.  B ) )
299296, 298breqtrd 4423 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  (
( 1  /  n
)  x.  B ) )
30025, 266, 268, 299fsumle 13379 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  /  n
)  x.  B ) )
30125, 46, 43, 47fsumdivc 13370 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  /  x ) )
302260rpcnd 11139 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  B  e.  CC )
303263recnd 9522 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
30425, 302, 303fsummulc1 13369 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  /  n
)  x.  B ) )
305300, 301, 3043brtr4d 4429 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  <_ 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  n
)  x.  B ) )
306260rpge0d 11141 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  B )
307 harmonicubnd 22535 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
3082, 9, 307syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
309264, 259, 261, 306, 308lemul1ad 10382 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  <_ 
( ( ( log `  x )  +  1 )  x.  B ) )
310258, 265, 262, 305, 309letrd 9638 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  <_ 
( ( ( log `  x )  +  1 )  x.  B ) )
311258, 262, 74, 109, 310lemul2ad 10383 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  /  x ) )  <_  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
31224, 44, 46, 47divassd 10252 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  =  ( ( 2  /  ( log `  x ) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  /  x ) ) )
313243recnd 9522 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  CC )
31421, 302, 313mul32d 9689 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) )  x.  B
) )
315 1cnd 9512 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
31619, 315, 19, 23divdird 10255 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
31719, 23dividd 10215 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
318317oveq1d 6214 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
319316, 318eqtr2d 2496 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
320319oveq2d 6215 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( 2  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
32119, 315addcld 9515 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
32221, 19, 321, 23div32d 10240 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( ( log `  x )  +  1 ) )  =  ( 2  x.  ( ( ( log `  x
)  +  1 )  /  ( log `  x
) ) ) )
323320, 322eqtr4d 2498 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) ) )
324323oveq1d 6214 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  (
1  +  ( 1  /  ( log `  x
) ) ) )  x.  B )  =  ( ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) )  x.  B ) )
32524, 321, 302mulassd 9519 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  (
( log `  x
)  +  1 ) )  x.  B )  =  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
326314, 324, 3253eqtrd 2499 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
327311, 312, 3263brtr4d 4429 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  <_  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) ) )
328327adantrr 716 . . . 4  |-  ( (
ph  /\  ( x  e.  ( 1 (,) +oo )  /\  1  <_  x
) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  <_  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) ) )
32982, 256, 257, 81, 328lo1le 13246 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x ) )  e. 
<_O(1) )
33078, 81, 236, 329lo1add 13221 . 2  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs