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

Theorem pntrlog2bndlem5 21228
Description: Lemma for pntrlog2bnd 21231. 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 10902 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
21adantl 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
3 1rp 10572 . . . . . . . . . . . . 13  |-  1  e.  RR+
43a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
54rpred 10604 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
6 eliooord 10926 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
76adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
87simpld 446 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
95, 2, 8ltled 9177 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 10639 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
11 pntrlog2bnd.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1211pntrf 21210 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1312ffvelrni 5828 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1410, 13syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  RR )
1514recnd 9070 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  CC )
1615abscld 12193 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
1716recnd 9070 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  x ) )  e.  CC )
1810relogcld 20471 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
1918recnd 9070 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
2017, 19mulcld 9064 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
21 2cn 10026 . . . . . . . . 9  |-  2  e.  CC
2221a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
232, 8rplogcld 20477 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2423rpne0d 10609 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
2522, 19, 24divcld 9746 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
26 fzfid 11267 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
2710adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
28 elfznn 11036 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2928adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
3029nnrpd 10603 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
3127, 30rpdivcld 10621 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3212ffvelrni 5828 . . . . . . . . . . . . 13  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
3331, 32syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
3433recnd 9070 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
3534abscld 12193 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
3630relogcld 20471 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
37 1re 9046 . . . . . . . . . . . 12  |-  1  e.  RR
3837a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
3936, 38readdcld 9071 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  RR )
4035, 39remulcld 9072 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  RR )
4140recnd 9070 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  CC )
4226, 41fsumcl 12482 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  CC )
4325, 42mulcld 9064 . . . . . 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 )
4420, 43subcld 9367 . . . . 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 )
4535recnd 9070 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  CC )
4626, 45fsumcl 12482 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  CC )
4725, 46mulcld 9064 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  CC )
482recnd 9070 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
4910rpne0d 10609 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
5044, 47, 48, 49divdird 9784 . . . 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 ) ) )
5116, 18remulcld 9072 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
5251recnd 9070 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
5352, 43, 47subsubd 9395 . . . . . 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 ) ) ) ) ) )
5425, 42, 46subdid 9445 . . . . . . . 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 ) ) ) ) ) )
5526, 41, 45fsumsub 12526 . . . . . . . . . 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 ) ) ) ) )
5639recnd 9070 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  CC )
57 ax-1cn 9004 . . . . . . . . . . . . . 14  |-  1  e.  CC
5857a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
5945, 56, 58subdid 9445 . . . . . . . . . . . 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 ) ) )
6036recnd 9070 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
6160, 58pncand 9368 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  n
)  +  1 )  -  1 )  =  ( log `  n
) )
6261oveq2d 6056 . . . . . . . . . . . 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
) ) )
6345mulid1d 9061 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  1 )  =  ( abs `  ( R `
 ( x  /  n ) ) ) )
6463oveq2d 6056 . . . . . . . . . . . 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
) ) ) ) )
6559, 62, 643eqtr3rd 2445 . . . . . . . . . . 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 ) ) )
6665sumeq2dv 12452 . . . . . . . . . 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
) ) )
6755, 66eqtr3d 2438 . . . . . . . . 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
) ) )
6867oveq2d 6056 . . . . . . . 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
) ) ) )
6954, 68eqtr3d 2438 . . . . . . 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
) ) ) )
7069oveq2d 6056 . . . . . 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
) ) ) ) )
7153, 70eqtr3d 2438 . . . . 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
) ) ) ) )
7271oveq1d 6055 . . . 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 ) )
7350, 72eqtr3d 2438 . . 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 ) )
7473mpteq2dva 4255 . 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 ) ) )
75 2re 10025 . . . . . . . 8  |-  2  e.  RR
7675a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
7776, 23rerpdivcld 10631 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
7826, 40fsumrecl 12483 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  RR )
7977, 78remulcld 9072 . . . . 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 )
8051, 79resubcld 9421 . . . 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 )
8180, 10rerpdivcld 10631 . . 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 )
8226, 35fsumrecl 12483 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  RR )
8377, 82remulcld 9072 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  RR )
8483, 10rerpdivcld 10631 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  e.  RR )
8537a1i 11 . . . 4  |-  ( ph  ->  1  e.  RR )
86 pntsval.1 . . . . . 6  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
87 pntrlog2bnd.t . . . . . 6  |-  T  =  ( a  e.  RR  |->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 ) )
8886, 11, 87pntrlog2bndlem4 21227 . . . . 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 )
8988a1i 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 ) )
9029nnred 9971 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
91 simpl 444 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
a  e.  RR )
92 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
a  e.  RR+ )
9392relogcld 20471 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( log `  a
)  e.  RR )
9491, 93remulcld 9072 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
95 0re 9047 . . . . . . . . . . . . . . 15  |-  0  e.  RR
9695a1i 11 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
9794, 96ifclda 3726 . . . . . . . . . . . . 13  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
9887, 97fmpti 5851 . . . . . . . . . . . 12  |-  T : RR
--> RR
9998ffvelrni 5828 . . . . . . . . . . 11  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
10090, 99syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
10190, 38resubcld 9421 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
10298ffvelrni 5828 . . . . . . . . . . 11  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
103101, 102syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
104100, 103resubcld 9421 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
10535, 104remulcld 9072 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
10626, 105fsumrecl 12483 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
10777, 106remulcld 9072 . . . . . 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 )
10851, 107resubcld 9421 . . . . 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 )
109108, 10rerpdivcld 10631 . . . 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 )
110 2rp 10573 . . . . . . . . . . 11  |-  2  e.  RR+
111110a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR+ )
112111rpge0d 10608 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  2 )
11376, 23, 112divge0d 10640 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( 2  /  ( log `  x ) ) )
11434absge0d 12201 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( R `
 ( x  /  n ) ) ) )
11530adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  n  e.  RR+ )
116115rpcnd 10606 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  n  e.  CC )
11760adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  n )  e.  CC )
118116, 117mulcld 9064 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( log `  n
) )  e.  CC )
119 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  1  <  n )
120115rpred 10604 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  n  e.  RR )
121 difrp 10601 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  RR  /\  n  e.  RR )  ->  ( 1  <  n  <->  ( n  -  1 )  e.  RR+ ) )
12237, 120, 121sylancr 645 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( 1  <  n  <->  ( n  -  1 )  e.  RR+ ) )
123119, 122mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  -  1 )  e.  RR+ )
124123relogcld 20471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  ( n  -  1 ) )  e.  RR )
125124recnd 9070 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  ( n  -  1 ) )  e.  CC )
126116, 125mulcld 9064 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( log `  (
n  -  1 ) ) )  e.  CC )
127118, 126, 125subsubd 9395 . . . . . . . . . . . . 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 ) ) ) )
128 rpre 10574 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR+  ->  n  e.  RR )
129 eleq1 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
130 id 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  a  =  n )
131 fveq2 5687 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
132130, 131oveq12d 6058 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
133 eqidd 2405 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  0  =  0 )
134129, 132, 133ifbieq12d 3721 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
135 ovex 6065 . . . . . . . . . . . . . . . . . . 19  |-  ( n  x.  ( log `  n
) )  e.  _V
136 c0ex 9041 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  _V
137135, 136ifex 3757 . . . . . . . . . . . . . . . . . 18  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
138134, 87, 137fvmpt 5765 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
139128, 138syl 16 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  ( T `
 n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
140 iftrue 3705 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
141139, 140eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( n  e.  RR+  ->  ( T `
 n )  =  ( n  x.  ( log `  n ) ) )
142115, 141syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( T `  n )  =  ( n  x.  ( log `  n ) ) )
143 rpre 10574 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR+  ->  ( n  -  1 )  e.  RR )
144 eleq1 2464 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  e.  RR+  <->  ( n  -  1 )  e.  RR+ ) )
145 id 20 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  a  =  ( n  - 
1 ) )
146 fveq2 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  ( log `  a )  =  ( log `  (
n  -  1 ) ) )
147145, 146oveq12d 6058 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  x.  ( log `  a ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
148 eqidd 2405 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  0  =  0 )
149144, 147, 148ifbieq12d 3721 . . . . . . . . . . . . . . . . . . 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 ) )
150 ovex 6065 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) )  e.  _V
151150, 136ifex 3757 . . . . . . . . . . . . . . . . . . 19  |-  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) ,  0 )  e.  _V
152149, 87, 151fvmpt 5765 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
153143, 152syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  ( T `
 ( n  - 
1 ) )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
154 iftrue 3705 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) ,  0 )  =  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) )
155153, 154eqtrd 2436 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR+  ->  ( T `
 ( n  - 
1 ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
156123, 155syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( T `  ( n  -  1 ) )  =  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) )
15757a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  1  e.  CC )
158116, 157, 125subdird 9446 . . . . . . . . . . . . . . 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 ) ) ) ) )
159125mulid2d 9062 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( 1  x.  ( log `  (
n  -  1 ) ) )  =  ( log `  ( n  -  1 ) ) )
160159oveq2d 6056 . . . . . . . . . . . . . . 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 ) ) ) )
161156, 158, 1603eqtrd 2440 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( T `  ( n  -  1 ) )  =  ( ( n  x.  ( log `  ( n  - 
1 ) ) )  -  ( log `  (
n  -  1 ) ) ) )
162142, 161oveq12d 6058 . . . . . . . . . . . . 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 ) ) ) ) )
163116, 117, 125subdid 9445 . . . . . . . . . . . . . 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 ) ) ) ) )
164163oveq1d 6055 . . . . . . . . . . . . 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 ) ) ) )
165127, 162, 1643eqtr4d 2446 . . . . . . . . . . . 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 ) ) ) )
166115relogcld 20471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  n )  e.  RR )
167166, 124resubcld 9421 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  e.  RR )
168167recnd 9070 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  e.  CC )
169116, 157, 168subdird 9446 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
170168mulid2d 9062 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( 1  x.  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  =  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )
171170oveq2d 6056 . . . . . . . . . . . . . . 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 ) ) ) ) )
172120, 167remulcld 9072 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  e.  RR )
173172recnd 9070 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  e.  CC )
174173, 117, 125subsub3d 9397 . . . . . . . . . . . . . . 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 ) ) )
175169, 171, 1743eqtrd 2440 . . . . . . . . . . . . . 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 ) ) )
176116, 157npcand 9371 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( (
n  -  1 )  +  1 )  =  n )
177176fveq2d 5691 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  ( ( n  - 
1 )  +  1 ) )  =  ( log `  n ) )
178177oveq1d 6055 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  ( ( n  -  1 )  +  1 ) )  -  ( log `  ( n  -  1 ) ) )  =  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )
179 logdifbnd 20785 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  ( ( log `  ( ( n  -  1 )  +  1 ) )  -  ( log `  (
n  -  1 ) ) )  <_  (
1  /  ( n  -  1 ) ) )
180123, 179syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  ( ( n  -  1 )  +  1 ) )  -  ( log `  ( n  -  1 ) ) )  <_  ( 1  /  ( n  - 
1 ) ) )
181178, 180eqbrtrrd 4194 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  <_  ( 1  /  ( n  - 
1 ) ) )
18237a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  1  e.  RR )
183167, 182, 123lemuldiv2d 10650 . . . . . . . . . . . . . . 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 ) ) ) )
184181, 183mpbird 224 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( (
n  -  1 )  x.  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  <_  1 )
185175, 184eqbrtrrd 4194 . . . . . . . . . . . . 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 )
186172, 124readdcld 9071 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( (
n  x.  ( ( log `  n )  -  ( log `  (
n  -  1 ) ) ) )  +  ( log `  (
n  -  1 ) ) )  e.  RR )
187186, 166, 182lesubadd2d 9581 . . . . . . . . . . . . 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 ) ) )
188185, 187mpbid 202 . . . . . . . . . . . 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 ) )
189165, 188eqbrtrd 4192 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
190 fveq2 5687 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  n )  =  ( T ` 
1 ) )
191 id 20 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  a  =  1 )
192191, 3syl6eqel 2492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  a  e.  RR+ )
193 iftrue 3705 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
194192, 193syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
195 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  1  ->  ( log `  a )  =  ( log `  1
) )
196 log1 20433 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( log `  1 )  =  0
197195, 196syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  ( log `  a )  =  0 )
198191, 197oveq12d 6058 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  ( 1  x.  0 ) )
19957mul01i 9212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  x.  0 )  =  0
200198, 199syl6eq 2452 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  0 )
201194, 200eqtrd 2436 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
202201, 87, 136fvmpt 5765 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  RR  ->  ( T `  1 )  =  0 )
20337, 202ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( T `
 1 )  =  0
204190, 203syl6eq 2452 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  n )  =  0 )
205 oveq1 6047 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
20657subidi 9327 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  -  1 )  =  0
207205, 206syl6eq 2452 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
208207fveq2d 5691 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  ( T ` 
0 ) )
209 rpne0 10583 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
210209necon2bi 2613 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
211 iffalse 3706 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
212210, 211syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
213212, 87, 136fvmpt 5765 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
21495, 213ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
215208, 214syl6eq 2452 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  0 )
216204, 215oveq12d 6058 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  ( 0  -  0 ) )
217 0cn 9040 . . . . . . . . . . . . . . . 16  |-  0  e.  CC
218217subidi 9327 . . . . . . . . . . . . . . 15  |-  ( 0  -  0 )  =  0
219216, 218syl6eq 2452 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
220219eqcoms 2407 . . . . . . . . . . . . 13  |-  ( 1  =  n  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
221220adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  =  n )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  =  0 )
22295a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  e.  RR )
22329nnge1d 9998 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
22490, 223logge0d 20478 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  n ) )
22536lep1d 9898 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  <_  (
( log `  n
)  +  1 ) )
226222, 36, 39, 224, 225letrd 9183 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  n
)  +  1 ) )
227226adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  =  n )  ->  0  <_  ( ( log `  n
)  +  1 ) )
228221, 227eqbrtrd 4192 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  =  n )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
229 elfzle1 11016 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  1  <_  n )
230229adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
23138, 90leloed 9172 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  n  <->  ( 1  <  n  \/  1  =  n ) ) )
232230, 231mpbid 202 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <  n  \/  1  =  n ) )
233189, 228, 232mpjaodan 762 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
234104, 39, 35, 114, 233lemul2ad 9907 . . . . . . . . 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 ) ) )
23526, 105, 40, 234fsumle 12533 . . . . . . . 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 ) ) )
236106, 78, 77, 113, 235lemul2ad 9907 . . . . . . 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 ) ) ) )
237107, 79, 51, 236lesub2dd 9599 . . . . . 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 ) ) ) ) ) ) )
23880, 108, 10, 237lediv1dd 10658 . . . . 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 ) )
239238adantrr 698 . . . 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 ) )
24085, 89, 109, 81, 239lo1le 12400 . . 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 ) )
241110a1i 11 . . . . . . . 8  |-  ( ph  ->  2  e.  RR+ )
242 pntrlog2bndlem5.1 . . . . . . . 8  |-  ( ph  ->  B  e.  RR+ )
243241, 242rpmulcld 10620 . . . . . . 7  |-  ( ph  ->  ( 2  x.  B
)  e.  RR+ )
244243rpred 10604 . . . . . 6  |-  ( ph  ->  ( 2  x.  B
)  e.  RR )
245244adantr 452 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  B )  e.  RR )
2465, 23rerpdivcld 10631 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
2475, 246readdcld 9071 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
248 ioossre 10928 . . . . . 6  |-  ( 1 (,)  +oo )  C_  RR
249 lo1const 12369 . . . . . 6  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  (
2  x.  B )  e.  RR )  -> 
( x  e.  ( 1 (,)  +oo )  |->  ( 2  x.  B
) )  e.  <_ O ( 1 ) )
250248, 244, 249sylancr 645 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 2  x.  B
) )  e.  <_ O ( 1 ) )
251 lo1const 12369 . . . . . . 7  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  1  e.  RR )  ->  (
x  e.  ( 1 (,)  +oo )  |->  1 )  e.  <_ O ( 1 ) )
252248, 85, 251sylancr 645 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  <_ O ( 1 ) )
253 divlogrlim 20479 . . . . . . . 8  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
254 rlimo1 12365 . . . . . . . 8  |-  ( ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  / 
( log `  x
) ) )  e.  O ( 1 ) )
255253, 254mp1i 12 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O ( 1 ) )
256246, 255o1lo1d 12288 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  <_ O
( 1 ) )
2575, 246, 252, 256lo1add 12375 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  <_ O
( 1 ) )
258243adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  B )  e.  RR+ )
259258rpge0d 10608 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( 2  x.  B
) )
260245, 247, 250, 257, 259lo1mul 12376 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( 2  x.  B )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  <_ O
( 1 ) )
261245, 247remulcld 9072 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
26282, 10rerpdivcld 10631 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  e.  RR )
26318, 5readdcld 9071 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
264242adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  B  e.  RR+ )
265264rpred 10604 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  B  e.  RR )
266263, 265remulcld 9072 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  +  1 )  x.  B )  e.  RR )
26729nnrecred 10001 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
26826, 267fsumrecl 12483 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
269268, 265remulcld 9072 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  e.  RR )
27035, 27rerpdivcld 10631 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  e.  RR )
271265adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  RR )
272267, 271remulcld 9072 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  /  n )  x.  B )  e.  RR )
27331rpcnd 10606 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
27431rpne0d 10609 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  =/=  0
)
27534, 273, 274absdivd 12212 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( abs `  (
x  /  n ) ) ) )
2762adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
277276, 29nndivred 10004 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
27831rpge0d 10608 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  n ) )
279277, 278absidd 12180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  /  n
) )  =  ( x  /  n ) )
280279oveq2d 6056 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  / 
( abs `  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
281275, 280eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
28248adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
28390recnd 9070 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
28449adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
28529nnne0d 10000 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
28645, 282, 283, 284, 285divdiv2d 9778 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  / 
( x  /  n
) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  x.  n )  /  x ) )
28745, 283, 282, 284div23d 9783 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  x.  n )  /  x )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n ) )
288281, 286, 2873eqtrd 2440 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( ( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n ) )
289 pntrlog2bndlem5.2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y ) )  <_  B )
290289ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  ( abs `  (
( R `  y
)  /  y ) )  <_  B )
291 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  ( R `  y )  =  ( R `  ( x  /  n
) ) )
292 id 20 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
293291, 292oveq12d 6058 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  /  n )  ->  (
( R `  y
)  /  y )  =  ( ( R `
 ( x  /  n ) )  / 
( x  /  n
) ) )
294293fveq2d 5691 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  /  n )  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
295294breq1d 4182 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  /  n )  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  B  <->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
) )
296295rspcv 3008 . . . . . . . . . . . . . 14  |-  ( ( x  /  n )  e.  RR+  ->  ( A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y
) )  <_  B  ->  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) )  <_  B )
)
29731, 290, 296sylc 58 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
)
298288, 297eqbrtrrd 4194 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n )  <_  B
)
299270, 271, 30lemuldivd 10649 . . . . . . . . . . . 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
) ) )
300298, 299mpbid 202 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  ( B  /  n ) )
301271recnd 9070 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  CC )
302301, 283, 285divrec2d 9750 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( B  /  n )  =  ( ( 1  /  n
)  x.  B ) )
303300, 302breqtrd 4196 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  (
( 1  /  n
)  x.  B ) )
30426, 270, 272, 303fsumle 12533 . . . . . . . . 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 ) )
30526, 48, 45, 49fsumdivc 12524 . . . . . . . . 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 ) )
306264rpcnd 10606 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  B  e.  CC )
307267recnd 9070 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
30826, 306, 307fsummulc1 12523 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  /  n
)  x.  B ) )
309304, 305, 3083brtr4d 4202 . . . . . . . 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 ) )
310264rpge0d 10608 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  B )
311 harmonicubnd 20801 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
3122, 9, 311syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
313268, 263, 265, 310, 312lemul1ad 9906 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  <_ 
( ( ( log `  x )  +  1 )  x.  B ) )
314262, 269, 266, 309, 313letrd 9183 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  <_ 
( ( ( log `  x )  +  1 )  x.  B ) )
315262, 266, 77, 113, 314lemul2ad 9907 . . . . . 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 ) ) )
31625, 46, 48, 49divassd 9781 . . . . . 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 ) ) )
317247recnd 9070 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  CC )
31822, 306, 317mul32d 9232 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) )  x.  B
) )
31957a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
32019, 319, 19, 24divdird 9784 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
32119, 24dividd 9744 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
322321oveq1d 6055 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
323320, 322eqtr2d 2437 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
324323oveq2d 6056 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( 2  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
32519, 319addcld 9063 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
32622, 19, 325, 24div32d 9769 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( ( log `  x )  +  1 ) )  =  ( 2  x.  ( ( ( log `  x
)  +  1 )  /  ( log `  x
) ) ) )
327324, 326eqtr4d 2439 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) ) )
328327oveq1d 6055 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
1  +  ( 1  /  ( log `  x
) ) ) )  x.  B )  =  ( ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) )  x.  B ) )
32925, 325, 306mulassd 9067 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  (
( log `  x
)  +  1 ) )  x.  B )  =  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
330318, 328, 3293eqtrd 2440 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( ( log `  x
)  +  1 )  x.  B ) ) )
331315, 316, 3303brtr4d 4202 . . . . 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
) ) ) ) )
332331adantrr 698 . . . 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
) ) ) ) )
33385, 260, 261, 84, 332lo1le 12400 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x ) )  e. 
<_ O ( 1 ) )
33481, 84, 240, 333lo1add 12375 . 2  |-  (