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

Theorem pntrlog2bndlem5 20746
Description: Lemma for pntrlog2bnd 20749. 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 10702 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
21adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
3 1rp 10374 . . . . . . . . . . . . 13  |-  1  e.  RR+
43a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
54rpred 10406 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
6 eliooord 10726 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
76adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
87simpld 445 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
95, 2, 8ltled 8983 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 10441 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
11 pntrlog2bnd.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1211pntrf 20728 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1312ffvelrni 5680 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1410, 13syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  RR )
1514recnd 8877 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  CC )
1615abscld 11934 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
1716recnd 8877 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  x ) )  e.  CC )
1810relogcld 19990 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
1918recnd 8877 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
2017, 19mulcld 8871 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
21 2cn 9832 . . . . . . . . 9  |-  2  e.  CC
2221a1i 10 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
232, 8rplogcld 19996 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2423rpne0d 10411 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
2522, 19, 24divcld 9552 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
26 fzfid 11051 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
2710adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
28 elfznn 10835 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2928adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
3029nnrpd 10405 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
3127, 30rpdivcld 10423 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3212ffvelrni 5680 . . . . . . . . . . . . 13  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
3331, 32syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
3433recnd 8877 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
3534abscld 11934 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
3630relogcld 19990 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
37 1re 8853 . . . . . . . . . . . 12  |-  1  e.  RR
3837a1i 10 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
3936, 38readdcld 8878 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  RR )
4035, 39remulcld 8879 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  RR )
4140recnd 8877 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( log `  n
)  +  1 ) )  e.  CC )
4226, 41fsumcl 12222 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  CC )
4325, 42mulcld 8871 . . . . . 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 9173 . . . . 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 8877 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  CC )
4626, 45fsumcl 12222 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  CC )
4725, 46mulcld 8871 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  CC )
482recnd 8877 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
4910rpne0d 10411 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
5044, 47, 48, 49divdird 9590 . . . 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 8879 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
5251recnd 8877 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
5352, 43, 47subsubd 9201 . . . . . 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 9251 . . . . . . . 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 12266 . . . . . . . . . 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 8877 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  n )  +  1 )  e.  CC )
57 ax-1cn 8811 . . . . . . . . . . . . . 14  |-  1  e.  CC
5857a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
5945, 56, 58subdid 9251 . . . . . . . . . . . 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 8877 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
6160, 58pncand 9174 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  n
)  +  1 )  -  1 )  =  ( log `  n
) )
6261oveq2d 5890 . . . . . . . . . . . 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 8868 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  1 )  =  ( abs `  ( R `
 ( x  /  n ) ) ) )
6463oveq2d 5890 . . . . . . . . . . . 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 2337 . . . . . . . . . . 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 12192 . . . . . . . . . 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 2330 . . . . . . . . 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 5890 . . . . . . . 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 2330 . . . . . . 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 5890 . . . . . 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 2330 . . . . 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 5889 . . . 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 2330 . . 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 4122 . 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 9831 . . . . . . . 8  |-  2  e.  RR
7675a1i 10 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
7776, 23rerpdivcld 10433 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
7826, 40fsumrecl 12223 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( log `  n )  +  1 ) )  e.  RR )
7977, 78remulcld 8879 . . . . 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 9227 . . . 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 10433 . . 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 12223 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `  ( x  /  n ) ) )  e.  RR )
8377, 82remulcld 8879 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  ( R `  ( x  /  n ) ) ) )  e.  RR )
8483, 10rerpdivcld 10433 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( abs `  ( R `  (
x  /  n ) ) ) )  /  x )  e.  RR )
8537a1i 10 . . . 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 20745 . . . . 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 10 . . . 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 9777 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
91 simpl 443 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
a  e.  RR )
92 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
a  e.  RR+ )
9392relogcld 19990 . . . . . . . . . . . . . . 15  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( log `  a
)  e.  RR )
9491, 93remulcld 8879 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
95 0re 8854 . . . . . . . . . . . . . . 15  |-  0  e.  RR
9695a1i 10 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
9794, 96ifclda 3605 . . . . . . . . . . . . 13  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
9887, 97fmpti 5699 . . . . . . . . . . . 12  |-  T : RR
--> RR
9998ffvelrni 5680 . . . . . . . . . . 11  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
10090, 99syl 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
10190, 38resubcld 9227 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
10298ffvelrni 5680 . . . . . . . . . . 11  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
103101, 102syl 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
104100, 103resubcld 9227 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
10535, 104remulcld 8879 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
10626, 105fsumrecl 12223 . . . . . . 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 8879 . . . . . 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 9227 . . . . 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 10433 . . . 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 10375 . . . . . . . . . . 11  |-  2  e.  RR+
111110a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR+ )
112111rpge0d 10410 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  2 )
11376, 23, 112divge0d 10442 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( 2  /  ( log `  x ) ) )
11434absge0d 11942 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( R `
 ( x  /  n ) ) ) )
11530adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  n  e.  RR+ )
116115rpcnd 10408 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  n  e.  CC )
11760adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  n )  e.  CC )
118116, 117mulcld 8871 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( log `  n
) )  e.  CC )
119 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  1  <  n )
120115rpred 10406 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  n  e.  RR )
121 difrp 10403 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  RR  /\  n  e.  RR )  ->  ( 1  <  n  <->  ( n  -  1 )  e.  RR+ ) )
12237, 120, 121sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( 1  <  n  <->  ( n  -  1 )  e.  RR+ ) )
123119, 122mpbid 201 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  -  1 )  e.  RR+ )
124123relogcld 19990 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  ( n  -  1 ) )  e.  RR )
125124recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  ( n  -  1 ) )  e.  CC )
126116, 125mulcld 8871 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( log `  (
n  -  1 ) ) )  e.  CC )
127118, 126, 125subsubd 9201 . . . . . . . . . . . . 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 10376 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR+  ->  n  e.  RR )
129 eleq1 2356 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
130 id 19 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  a  =  n )
131 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
132130, 131oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
133 eqidd 2297 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  n  ->  0  =  0 )
134129, 132, 133ifbieq12d 3600 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
135 ovex 5899 . . . . . . . . . . . . . . . . . . 19  |-  ( n  x.  ( log `  n
) )  e.  _V
136 c0ex 8848 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  _V
137135, 136ifex 3636 . . . . . . . . . . . . . . . . . 18  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
138134, 87, 137fvmpt 5618 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
139128, 138syl 15 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  ( T `
 n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
140 iftrue 3584 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
141139, 140eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( n  e.  RR+  ->  ( T `
 n )  =  ( n  x.  ( log `  n ) ) )
142115, 141syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( T `  n )  =  ( n  x.  ( log `  n ) ) )
143 rpre 10376 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR+  ->  ( n  -  1 )  e.  RR )
144 eleq1 2356 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  e.  RR+  <->  ( n  -  1 )  e.  RR+ ) )
145 id 19 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  a  =  ( n  - 
1 ) )
146 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( n  - 
1 )  ->  ( log `  a )  =  ( log `  (
n  -  1 ) ) )
147145, 146oveq12d 5892 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  (
a  x.  ( log `  a ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
148 eqidd 2297 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( n  - 
1 )  ->  0  =  0 )
149144, 147, 148ifbieq12d 3600 . . . . . . . . . . . . . . . . . . 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 5899 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) )  e.  _V
151150, 136ifex 3636 . . . . . . . . . . . . . . . . . . 19  |-  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) ,  0 )  e.  _V
152149, 87, 151fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
153143, 152syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  ( T `
 ( n  - 
1 ) )  =  if ( ( n  -  1 )  e.  RR+ ,  ( ( n  -  1 )  x.  ( log `  (
n  -  1 ) ) ) ,  0 ) )
154 iftrue 3584 . . . . . . . . . . . . . . . . 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 2328 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR+  ->  ( T `
 ( n  - 
1 ) )  =  ( ( n  - 
1 )  x.  ( log `  ( n  - 
1 ) ) ) )
156123, 155syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( T `  ( n  -  1 ) )  =  ( ( n  -  1 )  x.  ( log `  ( n  -  1 ) ) ) )
15757a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  1  e.  CC )
158116, 157, 125subdird 9252 . . . . . . . . . . . . . . 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 8869 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( 1  x.  ( log `  (
n  -  1 ) ) )  =  ( log `  ( n  -  1 ) ) )
160159oveq2d 5890 . . . . . . . . . . . . . . 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 2332 . . . . . . . . . . . . . 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 5892 . . . . . . . . . . . . 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 9251 . . . . . . . . . . . . . 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 5889 . . . . . . . . . . . . 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 2338 . . . . . . . . . . . 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 19990 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  n )  e.  RR )
167166, 124resubcld 9227 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  e.  RR )
168167recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  e.  CC )
169116, 157, 168subdird 9252 . . . . . . . . . . . . . . 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 8869 . . . . . . . . . . . . . . . 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 5890 . . . . . . . . . . . . . . 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 8879 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  e.  RR )
173172recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( n  x.  ( ( log `  n
)  -  ( log `  ( n  -  1 ) ) ) )  e.  CC )
174173, 117, 125subsub3d 9203 . . . . . . . . . . . . . . 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 2332 . . . . . . . . . . . . . 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 9177 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( (
n  -  1 )  +  1 )  =  n )
177176fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( log `  ( ( n  - 
1 )  +  1 ) )  =  ( log `  n ) )
178177oveq1d 5889 . . . . . . . . . . . . . . . 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 20304 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR+  ->  ( ( log `  ( ( n  -  1 )  +  1 ) )  -  ( log `  (
n  -  1 ) ) )  <_  (
1  /  ( n  -  1 ) ) )
180123, 179syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  ( ( n  -  1 )  +  1 ) )  -  ( log `  ( n  -  1 ) ) )  <_  ( 1  /  ( n  - 
1 ) ) )
181178, 180eqbrtrrd 4061 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( log `  n )  -  ( log `  ( n  -  1 ) ) )  <_  ( 1  /  ( n  - 
1 ) ) )
18237a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  1  e.  RR )
183167, 182, 123lemuldiv2d 10452 . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( (
n  -  1 )  x.  ( ( log `  n )  -  ( log `  ( n  - 
1 ) ) ) )  <_  1 )
185175, 184eqbrtrrd 4061 . . . . . . . . . . . . 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 8878 . . . . . . . . . . . . . 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 9387 . . . . . . . . . . . . 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 201 . . . . . . . . . . . 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 4059 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  <  n
)  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
190 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  n )  =  ( T ` 
1 ) )
191 id 19 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  a  =  1 )
192191, 3syl6eqel 2384 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  a  e.  RR+ )
193 iftrue 3584 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
194192, 193syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  ( a  x.  ( log `  a ) ) )
195 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  1  ->  ( log `  a )  =  ( log `  1
) )
196 log1 19955 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( log `  1 )  =  0
197195, 196syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  1  ->  ( log `  a )  =  0 )
198191, 197oveq12d 5892 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  ( 1  x.  0 ) )
19957mul01i 9018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1  x.  0 )  =  0
200198, 199syl6eq 2344 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  1  ->  (
a  x.  ( log `  a ) )  =  0 )
201194, 200eqtrd 2328 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  1  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
202201, 87, 136fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  RR  ->  ( T `  1 )  =  0 )
20337, 202ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( T `
 1 )  =  0
204190, 203syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  n )  =  0 )
205 oveq1 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
20657subidi 9133 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  -  1 )  =  0
207205, 206syl6eq 2344 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
208207fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  ( T ` 
0 ) )
209 rpne0 10385 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
210209necon2bi 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
211 iffalse 3585 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
212210, 211syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
213212, 87, 136fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
21495, 213ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
215208, 214syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( T `  ( n  -  1 ) )  =  0 )
216204, 215oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  ( 0  -  0 ) )
217 0cn 8847 . . . . . . . . . . . . . . . 16  |-  0  e.  CC
218217subidi 9133 . . . . . . . . . . . . . . 15  |-  ( 0  -  0 )  =  0
219216, 218syl6eq 2344 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
220219eqcoms 2299 . . . . . . . . . . . . 13  |-  ( 1  =  n  ->  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) )  =  0 )
221220adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  =  n )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  =  0 )
22295a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  e.  RR )
22329nnge1d 9804 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
22490, 223logge0d 19997 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  n ) )
22536lep1d 9704 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  <_  (
( log `  n
)  +  1 ) )
226222, 36, 39, 224, 225letrd 8989 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  n
)  +  1 ) )
227226adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  =  n )  ->  0  <_  ( ( log `  n
)  +  1 ) )
228221, 227eqbrtrd 4059 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  1  =  n )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
229 elfzle1 10815 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  1  <_  n )
230229adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  n )
23138, 90leloed 8978 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  n  <->  ( 1  <  n  \/  1  =  n ) ) )
232230, 231mpbid 201 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <  n  \/  1  =  n ) )
233189, 228, 232mpjaodan 761 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  <_ 
( ( log `  n
)  +  1 ) )
234104, 39, 35, 114, 233lemul2ad 9713 . . . . . . . . 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 12273 . . . . . . . 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 9713 . . . . . . 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 9405 . . . . . 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 10460 . . . . 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 697 . . . 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 12141 . . 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 10 . . . . . . . 8  |-  ( ph  ->  2  e.  RR+ )
242 pntrlog2bndlem5.1 . . . . . . . 8  |-  ( ph  ->  B  e.  RR+ )
243241, 242rpmulcld 10422 . . . . . . 7  |-  ( ph  ->  ( 2  x.  B
)  e.  RR+ )
244243rpred 10406 . . . . . 6  |-  ( ph  ->  ( 2  x.  B
)  e.  RR )
245244adantr 451 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  B )  e.  RR )
2465, 23rerpdivcld 10433 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
2475, 246readdcld 8878 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
248 ioossre 10728 . . . . . 6  |-  ( 1 (,)  +oo )  C_  RR
249 lo1const 12110 . . . . . 6  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  (
2  x.  B )  e.  RR )  -> 
( x  e.  ( 1 (,)  +oo )  |->  ( 2  x.  B
) )  e.  <_ O ( 1 ) )
250248, 244, 249sylancr 644 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 2  x.  B
) )  e.  <_ O ( 1 ) )
251 lo1const 12110 . . . . . . 7  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  1  e.  RR )  ->  (
x  e.  ( 1 (,)  +oo )  |->  1 )  e.  <_ O ( 1 ) )
252248, 85, 251sylancr 644 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  <_ O ( 1 ) )
253 divlogrlim 19998 . . . . . . . 8  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
254 rlimo1 12106 . . . . . . . 8  |-  ( ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  / 
( log `  x
) ) )  e.  O ( 1 ) )
255253, 254mp1i 11 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O ( 1 ) )
256246, 255o1lo1d 12029 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  <_ O
( 1 ) )
2575, 246, 252, 256lo1add 12116 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  <_ O
( 1 ) )
258243adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  B )  e.  RR+ )
259258rpge0d 10410 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( 2  x.  B
) )
260245, 247, 250, 257, 259lo1mul 12117 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( 2  x.  B )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  <_ O
( 1 ) )
261245, 247remulcld 8879 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
26282, 10rerpdivcld 10433 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( R `
 ( x  /  n ) ) )  /  x )  e.  RR )
26318, 5readdcld 8878 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
264242adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  B  e.  RR+ )
265264rpred 10406 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  B  e.  RR )
266263, 265remulcld 8879 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  +  1 )  x.  B )  e.  RR )
26729nnrecred 9807 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
26826, 267fsumrecl 12223 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
269268, 265remulcld 8879 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  x.  B )  e.  RR )
27035, 27rerpdivcld 10433 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  e.  RR )
271265adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  RR )
272267, 271remulcld 8879 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  /  n )  x.  B )  e.  RR )
27331rpcnd 10408 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
27431rpne0d 10411 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  =/=  0
)
27534, 273, 274absdivd 11953 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( abs `  (
x  /  n ) ) ) )
2762adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
277276, 29nndivred 9810 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
27831rpge0d 10410 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  n ) )
279277, 278absidd 11921 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  /  n
) )  =  ( x  /  n ) )
280279oveq2d 5890 . . . . . . . . . . . . . . 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 2328 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  /  ( x  /  n ) ) )
28248adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
28390recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
28449adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
28529nnne0d 9806 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
28645, 282, 283, 284, 285divdiv2d 9584 . . . . . . . . . . . . . 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 9589 . . . . . . . . . . . . . 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 2332 . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  ( abs `  (
( R `  y
)  /  y ) )  <_  B )
291 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  ( R `  y )  =  ( R `  ( x  /  n
) ) )
292 id 19 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
293291, 292oveq12d 5892 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  /  n )  ->  (
( R `  y
)  /  y )  =  ( ( R `
 ( x  /  n ) )  / 
( x  /  n
) ) )
294293fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  /  n )  ->  ( abs `  ( ( R `
 y )  / 
y ) )  =  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
295294breq1d 4049 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  /  n )  ->  (
( abs `  (
( R `  y
)  /  y ) )  <_  B  <->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
) )
296295rspcv 2893 . . . . . . . . . . . . . 14  |-  ( ( x  /  n )  e.  RR+  ->  ( A. y  e.  RR+  ( abs `  ( ( R `  y )  /  y
) )  <_  B  ->  ( abs `  (
( R `  (
x  /  n ) )  /  ( x  /  n ) ) )  <_  B )
)
29731, 290, 296sylc 56 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  n
) )  /  (
x  /  n ) ) )  <_  B
)
298288, 297eqbrtrrd 4061 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  /  x )  x.  n )  <_  B
)
299270, 271, 30lemuldivd 10451 . . . . . . . . . . . 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 201 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  ( B  /  n ) )
301271recnd 8877 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  B  e.  CC )
302301, 283, 285divrec2d 9556 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( B  /  n )  =  ( ( 1  /  n
)  x.  B ) )
303300, 302breqtrd 4063 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  /  x )  <_  (
( 1  /  n
)  x.  B ) )
30426, 270, 272, 303fsumle 12273 . . . . . . . . 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 12264 . . . . . . . . 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 10408 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  B  e.  CC )
307267recnd 8877 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
30826, 306, 307fsummulc1 12263 . . . . . . . . 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 4069 . . . . . . . 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 10410 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  B )
311 harmonicubnd 20319 . . . . . . . . . 10  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
3122, 9, 311syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
313268, 263, 265, 310, 312lemul1ad 9712 . . . . . . . 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 8989 . . . . . . 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 9713 . . . . . 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 9587 . . . . . 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 8877 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  CC )
31822, 306, 317mul32d 9038 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  B
)  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) )  x.  B
) )
31957a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
32019, 319, 19, 24divdird 9590 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
32119, 24dividd 9550 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
322321oveq1d 5889 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
323320, 322eqtr2d 2329 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
324323oveq2d 5890 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( 2  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
32519, 319addcld 8870 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
32622, 19, 325, 24div32d 9575 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( ( log `  x )  +  1 ) )  =  ( 2  x.  ( ( ( log `  x
)  +  1 )  /  ( log `  x
) ) ) )
327324, 326eqtr4d 2331 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( 2  /  ( log `  x
) )  x.  (
( log `  x
)  +  1 ) ) )
328327oveq1d 5889 . . . . . . 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 8874 . . . . . . 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 2332 . . . . . 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 4069 . . . . 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 697 . . . 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 12141 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ...