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

Theorem pntrlog2bndlem5 23892
Description: Lemma for pntrlog2bnd 23895. 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 11584 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
21adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
3 1rp 11249 . . . . . . . . . . . . 13  |-  1  e.  RR+
43a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
5 1red 9628 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
6 eliooord 11609 . . . . . . . . . . . . . . 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 9750 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 11316 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
11 pntrlog2bnd.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1211pntrf 23874 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1312ffvelrni 6031 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1410, 13syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  RR )
1514recnd 9639 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  CC )
1615abscld 13279 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
1716recnd 9639 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  CC )
1810relogcld 23134 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
1918recnd 9639 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
2017, 19mulcld 9633 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
21 2cnd 10629 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  CC )
222, 8rplogcld 23140 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
2322rpne0d 11286 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
2421, 19, 23divcld 10341 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
25 fzfid 12086 . . . . . . . 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 11739 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2827adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
2928nnrpd 11280 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
3026, 29rpdivcld 11298 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3112ffvelrni 6031 . . . . . . . . . . . . 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 9639 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
3433abscld 13279 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
3529relogcld 23134 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
36 1red 9628 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
3735, 36readdcld 9640 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  RR )
3834, 37remulcld 9641 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  RR )
3938recnd 9639 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  CC )
4025, 39fsumcl 13567 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  CC )
4124, 40mulcld 9633 . . . . . 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 9950 . . . . 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 9639 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  CC )
4425, 43fsumcl 13567 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  CC )
4524, 44mulcld 9633 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  CC )
462recnd 9639 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
4710rpne0d 11286 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
4842, 45, 46, 47divdird 10379 . . . 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 9641 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
5049recnd 9639 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
5150, 41, 45subsubd 9978 . . . . . 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 10033 . . . . . . . 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 13615 . . . . . . . . . 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 9639 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  CC )
55 1cnd 9629 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
5643, 54, 55subdid 10033 . . . . . . . . . . . 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 9639 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
5857, 55pncand 9951 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  n
)  +  1 )  -  1 )  =  ( log `  n
) )
5958oveq2d 6312 . . . . . . . . . . . 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 9630 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  1 )  =  ( abs `  ( R `
 ( x  /  n ) ) ) )
6160oveq2d 6312 . . . . . . . . . . . 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 2507 . . . . . . . . . . 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 13537 . . . . . . . . . 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 2500 . . . . . . . . 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 6312 . . . . . . . 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 2500 . . . . . . 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 6312 . . . . . 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 2500 . . . . 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 6311 . . . 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 2500 . . 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 4543 . 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 10626 . . . . . . . 8  |-  2  e.  RR
7372a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
7473, 22rerpdivcld 11308 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
7525, 38fsumrecl 13568 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  RR )
7674, 75remulcld 9641 . . . . 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 10008 . . . 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 11308 . . 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 13568 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  RR )
8074, 79remulcld 9641 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  RR )
8180, 10rerpdivcld 11308 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  e.  RR )
82 1red 9628 . . . 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 23891 . . . . 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 10571 . . . . . . . . . . 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 23134 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( log `  a
)  e.  RR )
9188, 90remulcld 9641 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
92 0red 9614 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
9391, 92ifclda 3976 . . . . . . . . . . . . 13  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
9484, 93fmpti 6055 . . . . . . . . . . . 12  |-  T : RR
--> RR
9594ffvelrni 6031 . . . . . . . . . . 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 10008 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
9894ffvelrni 6031 . . . . . . . . . . 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 10008 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
10134, 100remulcld 9641 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
10225, 101fsumrecl 13568 . . . . . . 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 9641 . . . . . 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 10008 . . . . 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 11308 . . . 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 11250 . . . . . . . . . . 11  |-  2  e.  RR+
107106a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR+ )
108107rpge0d 11285 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  2 )
10973, 22, 108divge0d 11317 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( 2  /  ( log `  x ) ) )
11033absge0d 13287 . . . . . . . . . 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 11283 . . . . . . . . . . . . . . 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 9633 . . . . . . . . . . . . . 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 9612 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR
117111rpred 11281 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  n  e.  RR )
118 difrp 11278 . . . . . . . . . . . . . . . . . . 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 23134 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  ( n  - 
1 ) )  e.  RR )
122121recnd 9639 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  ( n  - 
1 ) )  e.  CC )
123112, 122mulcld 9633 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( log `  ( n  -  1 ) ) )  e.  CC )
124114, 123, 122subsubd 9978 . . . . . . . . . . . . 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 11251 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR+  ->  n  e.  RR )
126 eleq1 2529 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
127 id 22 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  a  =  n )
128 fveq2 5872 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
129127, 128oveq12d 6314 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
130126, 129ifbieq1d 3967 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
131 ovex 6324 . . . . . . . . . . . . . . . . . . 19  |-  ( n  x.  ( log `  n
) )  e.  _V
132 c0ex 9607 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  _V
133131, 132ifex 4013 . . . . . . . . . . . . . . . . . 18  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
134130, 84, 133fvmpt 5956 . . . . . . . . . . . . . . . . 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 3950 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
137135, 136eqtrd 2498 . . . . . . . . . . . . . . 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 11251 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR+  ->  ( n  -  1 )  e.  RR )
140 eleq1 2529 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  e.  RR+  <->  ( n  -  1 )  e.  RR+ ) )
141 id 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  a  =  ( n  - 
1 ) )
142 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  ( log `  a )  =  ( log `  (
n  -  1 ) ) )
143141, 142oveq12d 6314 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  x.  ( log `  a ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
144140, 143ifbieq1d 3967 . . . . . . . . . . . . . . . . . . 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 6324 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) )  e.  _V
146145, 132ifex 4013 . . . . . . . . . . . . . . . . . . 19  |-  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) ,  0 )  e.  _V
147144, 84, 146fvmpt 5956 . . . . . . . . . . . . . . . . . 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 3950 . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . 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 9629 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  1  e.  CC )
153112, 152, 122subdird 10034 . . . . . . . . . . . . . . 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 9631 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
1  x.  ( log `  ( n  -  1 ) ) )  =  ( log `  (
n  -  1 ) ) )
155154oveq2d 6312 . . . . . . . . . . . . . . 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 2502 . . . . . . . . . . . . . 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 6314 . . . . . . . . . . . . 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 10033 . . . . . . . . . . . . . 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 6311 . . . . . . . . . . . . 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 2508 . . . . . . . . . . . 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 23134 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  n )  e.  RR )
162161, 121resubcld 10008 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) )  e.  RR )
163162recnd 9639 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) )  e.  CC )
164112, 152, 163subdird 10034 . . . . . . . . . . . . . . 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 9631 . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . 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 9641 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  e.  RR )
168167recnd 9639 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  e.  CC )
169168, 113, 122subsub3d 9980 . . . . . . . . . . . . . . 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 2502 . . . . . . . . . . . . . 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 9954 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( n  -  1 )  +  1 )  =  n )
172171fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  ( log `  ( ( n  -  1 )  +  1 ) )  =  ( log `  n
) )
173172oveq1d 6311 . . . . . . . . . . . . . . . 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 23449 . . . . . . . . . . . . . . . . 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 4478 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( log `  n
)  -  ( log `  ( n  -  1 ) ) )  <_ 
( 1  /  (
n  -  1 ) ) )
177 1red 9628 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  1  e.  RR )
178162, 177, 120lemuldiv2d 11327 . . . . . . . . . . . . . . 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 4478 . . . . . . . . . . . . 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 9640 . . . . . . . . . . . . . 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 10172 . . . . . . . . . . . . 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 4476 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  < 
n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  <_  ( ( log `  n )  +  1 ) )
185 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  n )  =  ( T ` 
1 ) )
186 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  a  =  1 )
187186, 3syl6eqel 2553 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  a  e.  RR+ )
188187iftrued 3952 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
189 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  1  ->  ( log `  a )  =  ( log `  1
) )
190 log1 23096 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( log `  1 )  =  0
191189, 190syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  ( log `  a )  =  0 )
192186, 191oveq12d 6314 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  ( 1  x.  0 ) )
193 ax-1cn 9567 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
194193mul01i 9787 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  x.  0 )  =  0
195192, 194syl6eq 2514 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  0 )
196188, 195eqtrd 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
197196, 84, 132fvmpt 5956 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  RR  ->  ( T `  1 )  =  0 )
198116, 197ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 1 )  =  0
199185, 198syl6eq 2514 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  n )  =  0 )
200 oveq1 6303 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
201 1m1e0 10625 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  -  1 )  =  0
202200, 201syl6eq 2514 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
203202fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  ( T ` 
0 ) )
204 0re 9613 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
205 rpne0 11260 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
206205necon2bi 2694 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
207206iffalsed 3955 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
208207, 84, 132fvmpt 5956 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
209204, 208ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
210203, 209syl6eq 2514 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  0 )
211199, 210oveq12d 6314 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  ( 0  -  0 ) )
212 0m0e0 10666 . . . . . . . . . . . . . . 15  |-  ( 0  -  0 )  =  0
213211, 212syl6eq 2514 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
214213eqcoms 2469 . . . . . . . . . . . . 13  |-  ( 1  =  n  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
215214adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  =  n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
216 0red 9614 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  e.  RR )
21728nnge1d 10599 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
21887, 217logge0d 23141 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  n ) )
21935lep1d 10497 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  <_  (
( log `  n
)  +  1 ) )
220216, 35, 37, 218, 219letrd 9756 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  n
)  +  1 ) )
221220adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  =  n )  ->  0  <_  ( ( log `  n
)  +  1 ) )
222215, 221eqbrtrd 4476 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  1  =  n )  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  <_  ( ( log `  n )  +  1 ) )
223 elfzle1 11714 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  1  <_  n )
224223adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
22536, 87leloed 9745 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  n  <->  ( 1  <  n  \/  1  =  n ) ) )
226224, 225mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <  n  \/  1  =  n ) )
227184, 222, 226mpjaodan 786 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
228100, 37, 34, 110, 227lemul2ad 10506 . . . . . . . . 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 ) ) )
22925, 101, 38, 228fsumle 13625 . . . . . . . 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 ) ) )
230102, 75, 74, 109, 229lemul2ad 10506 . . . . . . 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 ) ) ) )
231103, 76, 49, 230lesub2dd 10190 . . . . . 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 ) ) ) ) ) ) )
23277, 104, 10, 231lediv1dd 11335 . . . . 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 ) )
233232adantrr 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 ) )
23482, 86, 105, 78, 233lo1le 13486 . . 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) )
235106a1i 11 . . . . . . . 8  |-  ( ph  ->  2  e.  RR+ )
236 pntrlog2bndlem5.1 . . . . . . . 8  |-  ( ph  ->  B  e.  RR+ )
237235, 236rpmulcld 11297 . . . . . . 7  |-  ( ph  ->  ( 2  x.  B
)  e.  RR+ )
238237rpred 11281 . . . . . 6  |-  ( ph  ->  ( 2  x.  B
)  e.  RR )
239238adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  B )  e.  RR )
2405, 22rerpdivcld 11308 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
2415, 240readdcld 9640 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
242 ioossre 11611 . . . . . 6  |-  ( 1 (,) +oo )  C_  RR
243 lo1const 13455 . . . . . 6  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  (
2  x.  B )  e.  RR )  -> 
( x  e.  ( 1 (,) +oo )  |->  ( 2  x.  B
) )  e.  <_O(1) )
244242, 238, 243sylancr 663 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 2  x.  B
) )  e.  <_O(1) )
245 lo1const 13455 . . . . . . 7  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  1  e.  RR )  ->  (
x  e.  ( 1 (,) +oo )  |->  1 )  e.  <_O(1) )
246242, 82, 245sylancr 663 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  1 )  e.  <_O(1) )
247 divlogrlim 23142 . . . . . . . 8  |-  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
248 rlimo1 13451 . . . . . . . 8  |-  ( ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  ~~> r  0  ->  (
x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
249247, 248mp1i 12 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
250240, 249o1lo1d 13374 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  <_O(1) )
2515, 240, 246, 250lo1add 13461 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  <_O(1) )
252237adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  B )  e.  RR+ )
253252rpge0d 11285 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( 2  x.  B
) )
254239, 241, 244, 251, 253lo1mul 13462 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( 2  x.  B )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  <_O(1) )
255239, 241remulcld 9641 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
25679, 10rerpdivcld 11308 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  e.  RR )
25718, 5readdcld 9640 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
258236adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  B  e.  RR+ )
259258rpred 11281 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  B  e.  RR )
260257, 259remulcld 9641 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  +  1 )  x.  B )  e.  RR )
26128nnrecred 10602 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
26225, 261fsumrecl 13568 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
263262, 259remulcld 9641 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  e.  RR )
26434, 26rerpdivcld 11308 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  e.  RR )
265259adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  RR )
266261, 265remulcld 9641 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  /  n )  x.  B )  e.  RR )
26730rpcnd 11283 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
26830rpne0d 11286 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  =/=  0
)
26933, 267, 268absdivd 13298 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( abs `  (
x  /  n ) ) ) )
2702adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
271270, 28nndivred 10605 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
27230rpge0d 11285 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  n ) )
273271, 272absidd 13266 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  /  n
) )  =  ( x  /  n ) )
274273oveq2d 6312 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  / 
( abs `  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
275269, 274eqtrd 2498 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
27646adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
27787recnd 9639 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
27847adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
27928nnne0d 10601 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
28043, 276, 277, 278, 279divdiv2d 10373 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  / 
( x  /  n
) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  x.  n )  /  x ) )
28143, 277, 276, 278div23d 10378 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  x.  n )  /  x )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n ) )
282275, 280, 2813eqtrd 2502 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n ) )
283 pntrlog2bndlem5.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y ) )  <_  B )
284283ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  ( abs `  (
( R `  y
)  /  y ) )  <_  B )
285 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  ( R `  y )  =  ( R `  ( x  /  n
) ) )
286 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
287285, 286oveq12d 6314 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  /  n )  ->  (
( R `  y
)  /  y )  =  ( ( R `
 ( x  /  n ) )  / 
( x  /  n
) ) )
288287fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  /  n )  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
289288breq1d 4466 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  /  n )  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  B  <->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
) )
290289rspcv 3206 . . . . . . . . . . . . . 14  |-  ( ( x  /  n )  e.  RR+  ->  ( A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y
) )  <_  B  ->  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) )  <_  B )
)
29130, 284, 290sylc 60 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
)
292282, 291eqbrtrrd 4478 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n )  <_  B
)
293264, 265, 29lemuldivd 11326 . . . . . . . . . . . 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
) ) )
294292, 293mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  ( B  /  n ) )
295265recnd 9639 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  CC )
296295, 277, 279divrec2d 10345 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( B  /  n )  =  ( ( 1  /  n
)  x.  B ) )
297294, 296breqtrd 4480 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  (
( 1  /  n
)  x.  B ) )
29825, 264, 266, 297fsumle 13625 . . . . . . . . 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 ) )
29925, 46, 43, 47fsumdivc 13613 . . . . . . . . 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 ) )
300258rpcnd 11283 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  B  e.  CC )
301261recnd 9639 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
30225, 300, 301fsummulc1 13612 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  /  n
)  x.  B ) )
303298, 299, 3023brtr4d 4486 . . . . . . . 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 ) )
304258rpge0d 11285 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  B )
305 harmonicubnd 23465 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
3062, 9, 305syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
307262, 257, 259, 304, 306lemul1ad 10505 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  <_ 
( ( ( log `  x )  +  1 )  x.  B ) )
308256, 263, 260, 303, 307letrd 9756 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  <_ 
( ( ( log `  x )  +  1 )  x.  B ) )
309256, 260, 74, 109, 308lemul2ad 10506 . . . . . 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 ) ) )
31024, 44, 46, 47divassd 10376 . . . . . 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 ) ) )
311241recnd 9639 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  CC )
31221, 300, 311mul32d 9807 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) )  x.  B
) )
313 1cnd 9629 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
31419, 313, 19, 23divdird 10379 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
31519, 23dividd 10339 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
316315oveq1d 6311 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
317314, 316eqtr2d 2499 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
318317oveq2d 6312 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( 2  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
31919, 313addcld 9632 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
32021, 19, 319, 23div32d 10364 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( ( log `  x )  +  1 ) )  =  ( 2  x.  ( ( ( log `  x
)  +  1 )  /  ( log `  x
) ) ) )
321318, 320eqtr4d 2501 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) ) )
322321oveq1d 6311 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  (
1  +  ( 1  /  ( log `  x
) ) ) )  x.  B )  =  ( ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) )  x.  B ) )
32324, 319, 300mulassd 9636 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  (
( log `  x
)  +  1 ) )  x.  B )  =  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
324312, 322, 3233eqtrd 2502 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
325309, 310, 3243brtr4d 4486 . . . . 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
) ) ) ) )
326325adantrr 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
) ) ) ) )
32782, 254, 255, 81, 326lo1le 13486 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x ) )  e. 
<_O(1) )
32878, 81, 234, 327lo1add 13461 . 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 ) ) )  e.  <_O