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

Theorem mulog2sumlem2 20700
Description: Lemma for mulog2sum 20702. (Contributed by Mario Carneiro, 19-May-2016.)
Hypotheses
Ref Expression
logdivsum.1  |-  F  =  ( y  e.  RR+  |->  ( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( ( log `  i
)  /  i )  -  ( ( ( log `  y ) ^ 2 )  / 
2 ) ) )
mulog2sumlem.1  |-  ( ph  ->  F  ~~> r  L )
mulog2sumlem2.t  |-  T  =  ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )
mulog2sumlem2.r  |-  R  =  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
Assertion
Ref Expression
mulog2sumlem2  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  O ( 1 ) )
Distinct variable groups:    i, m, n, x, y    x, F   
n, L, x    ph, m, n, x    R, n, x
Allowed substitution hints:    ph( y, i)    R( y, i, m)    T( x, y, i, m, n)    F( y, i, m, n)    L( y, i, m)

Proof of Theorem mulog2sumlem2
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 1re 8853 . . 3  |-  1  e.  RR
21a1i 10 . 2  |-  ( ph  ->  1  e.  RR )
3 2re 9831 . . . 4  |-  2  e.  RR
4 fzfid 11051 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
5 simpr 447 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR+ )
6 elfznn 10835 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76nnrpd 10405 . . . . . . . 8  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
8 rpdivcl 10392 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
95, 7, 8syl2an 463 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
109relogcld 19990 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
11 simplr 731 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
1210, 11rerpdivcld 10433 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  RR )
134, 12fsumrecl 12223 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )
14 remulcl 8838 . . . 4  |-  ( ( 2  e.  RR  /\  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) )  e.  RR )
153, 13, 14sylancr 644 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  RR )
16 mulog2sumlem2.r . . . . . 6  |-  R  =  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
17 2ne0 9845 . . . . . . . . 9  |-  2  =/=  0
183, 17rereccli 9541 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
19 emre 20315 . . . . . . . . 9  |-  gamma  e.  RR
20 mulog2sumlem.1 . . . . . . . . . . 11  |-  ( ph  ->  F  ~~> r  L )
21 rlimcl 11993 . . . . . . . . . . 11  |-  ( F  ~~> r  L  ->  L  e.  CC )
2220, 21syl 15 . . . . . . . . . 10  |-  ( ph  ->  L  e.  CC )
2322abscld 11934 . . . . . . . . 9  |-  ( ph  ->  ( abs `  L
)  e.  RR )
24 readdcl 8836 . . . . . . . . 9  |-  ( (
gamma  e.  RR  /\  ( abs `  L )  e.  RR )  ->  ( gamma  +  ( abs `  L
) )  e.  RR )
2519, 23, 24sylancr 644 . . . . . . . 8  |-  ( ph  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
26 readdcl 8836 . . . . . . . 8  |-  ( ( ( 1  /  2
)  e.  RR  /\  ( gamma  +  ( abs `  L ) )  e.  RR )  ->  (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  e.  RR )
2718, 25, 26sylancr 644 . . . . . . 7  |-  ( ph  ->  ( ( 1  / 
2 )  +  (
gamma  +  ( abs `  L
) ) )  e.  RR )
28 fzfid 11051 . . . . . . . 8  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
29 epr 12502 . . . . . . . . . . 11  |-  _e  e.  RR+
30 elfznn 10835 . . . . . . . . . . . . 13  |-  ( m  e.  ( 1 ... 2 )  ->  m  e.  NN )
3130adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  NN )
3231nnrpd 10405 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
33 rpdivcl 10392 . . . . . . . . . . 11  |-  ( ( _e  e.  RR+  /\  m  e.  RR+ )  ->  (
_e  /  m )  e.  RR+ )
3429, 32, 33sylancr 644 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
_e  /  m )  e.  RR+ )
3534relogcld 19990 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  ( _e  /  m ) )  e.  RR )
3635, 31nndivred 9810 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( log `  (
_e  /  m )
)  /  m )  e.  RR )
3728, 36fsumrecl 12223 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
3827, 37readdcld 8878 . . . . . 6  |-  ( ph  ->  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )  e.  RR )
3916, 38syl5eqel 2380 . . . . 5  |-  ( ph  ->  R  e.  RR )
40 remulcl 8838 . . . . 5  |-  ( ( R  e.  RR  /\  2  e.  RR )  ->  ( R  x.  2 )  e.  RR )
4139, 3, 40sylancl 643 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  RR )
4241adantr 451 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  x.  2 )  e.  RR )
433a1i 10 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  RR )
44 rpssre 10380 . . . . 5  |-  RR+  C_  RR
45 2cn 9832 . . . . . 6  |-  2  e.  CC
4645a1i 10 . . . . 5  |-  ( ph  ->  2  e.  CC )
47 o1const 12109 . . . . 5  |-  ( (
RR+  C_  RR  /\  2  e.  CC )  ->  (
x  e.  RR+  |->  2 )  e.  O ( 1 ) )
4844, 46, 47sylancr 644 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  2 )  e.  O
( 1 ) )
49 logfacrlim2 20481 . . . . 5  |-  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1
50 rlimo1 12106 . . . . 5  |-  ( ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1  -> 
( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  O ( 1 ) )
5149, 50mp1i 11 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  O ( 1 ) )
5243, 13, 48, 51o1mul2 12114 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) ) )  e.  O ( 1 ) )
5341recnd 8877 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  CC )
54 o1const 12109 . . . 4  |-  ( (
RR+  C_  RR  /\  ( R  x.  2 )  e.  CC )  -> 
( x  e.  RR+  |->  ( R  x.  2
) )  e.  O
( 1 ) )
5544, 53, 54sylancr 644 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( R  x.  2
) )  e.  O
( 1 ) )
5615, 42, 52, 55o1add2 12113 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  O ( 1 ) )
5715, 42readdcld 8878 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
586adantl 452 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
59 mucl 20395 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
mmu `  n )  e.  ZZ )
6058, 59syl 15 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  ZZ )
6160zred 10133 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  RR )
6261, 58nndivred 9810 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  RR )
6362recnd 8877 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  CC )
64 mulog2sumlem2.t . . . . . 6  |-  T  =  ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )
6510recnd 8877 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
6665sqcld 11259 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  CC )
6766halfcld 9972 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  CC )
68 remulcl 8838 . . . . . . . . . 10  |-  ( (
gamma  e.  RR  /\  ( log `  ( x  /  n ) )  e.  RR )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6919, 10, 68sylancr 644 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
7069recnd 8877 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  CC )
7122ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  L  e.  CC )
7270, 71subcld 9173 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
7367, 72addcld 8870 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )  e.  CC )
7464, 73syl5eqel 2380 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
7563, 74mulcld 8871 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  T )  e.  CC )
764, 75fsumcl 12222 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  e.  CC )
77 relogcl 19948 . . . . 5  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
7877adantl 452 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
7978recnd 8877 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
8076, 79subcld 9173 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) )  e.  CC )
8180abscld 11934 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8281adantrr 697 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8357adantrr 697 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
8457recnd 8877 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  CC )
8584abscld 11934 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8685adantrr 697 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8760zcnd 10134 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  CC )
88 fzfid 11051 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
89 elfznn 10835 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
90 nnrp 10379 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN  ->  m  e.  RR+ )
91 rpdivcl 10392 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  /  n
)  e.  RR+  /\  m  e.  RR+ )  ->  (
( x  /  n
)  /  m )  e.  RR+ )
929, 90, 91syl2an 463 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  e.  RR+ )
9392relogcld 19990 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  RR )
94 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  NN )
9593, 94nndivred 9810 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  RR )
9695recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  CC )
9789, 96sylan2 460 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  e.  CC )
9888, 97fsumcl 12222 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
9974, 98subcld 9173 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
10058nncnd 9778 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
10158nnne0d 9806 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
10287, 99, 100, 101div23d 9589 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( ( ( mmu `  n
)  /  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
10363, 74, 98subdid 9251 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  =  ( ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( ( ( mmu `  n )  /  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
104102, 103eqtrd 2328 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( ( ( mmu `  n )  /  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
105104sumeq2dv 12192 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( mmu `  n )  /  n )  x.  T )  -  (
( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
10663, 98mulcld 8871 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
1074, 75, 106fsumsub 12266 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( mmu `  n )  /  n )  x.  T )  -  (
( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
108105, 107eqtrd 2328 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
109108adantrr 697 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
11088, 63, 97fsummulc2 12262 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( ( mmu `  n )  /  n
)  x.  ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )
11187adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( mmu `  n )  e.  CC )
112100, 101jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
113112adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
114 div23 9459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( mmu `  n
)  e.  CC  /\  ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( ( mmu `  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) )  /  n
)  =  ( ( ( mmu `  n
)  /  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) ) )
115 divass 9458 . . . . . . . . . . . . . . . . 17  |-  ( ( ( mmu `  n
)  e.  CC  /\  ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( ( mmu `  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) )  /  n
)  =  ( ( mmu `  n )  x.  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n ) ) )
116114, 115eqtr3d 2330 . . . . . . . . . . . . . . . 16  |-  ( ( ( mmu `  n
)  e.  CC  /\  ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( ( mmu `  n )  /  n )  x.  ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( ( mmu `  n )  x.  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n ) ) )
117111, 96, 113, 116syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( mmu `  n )  /  n )  x.  ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( ( mmu `  n )  x.  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n ) ) )
11893recnd 8877 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  CC )
11994nnrpd 10405 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  RR+ )
120 rpcnne0 10387 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
121119, 120syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  e.  CC  /\  m  =/=  0 ) )
122 divdiv1 9487 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( log `  (
( x  /  n
)  /  m ) )  e.  CC  /\  ( m  e.  CC  /\  m  =/=  0 )  /\  ( n  e.  CC  /\  n  =/=  0 ) )  -> 
( ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  /  n )  =  ( ( log `  ( ( x  /  n )  /  m
) )  /  (
m  x.  n ) ) )
123118, 121, 113, 122syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n )  =  ( ( log `  (
( x  /  n
)  /  m ) )  /  ( m  x.  n ) ) )
124 rpre 10376 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR+  ->  x  e.  RR )
125124adantl 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
126125adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
127126recnd 8877 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
128127adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  x  e.  CC )
129 divdiv1 9487 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  CC  /\  ( n  e.  CC  /\  n  =/=  0 )  /\  ( m  e.  CC  /\  m  =/=  0 ) )  -> 
( ( x  /  n )  /  m
)  =  ( x  /  ( n  x.  m ) ) )
130128, 113, 121, 129syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  =  ( x  /  ( n  x.  m ) ) )
131130fveq2d 5545 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  =  ( log `  ( x  /  (
n  x.  m ) ) ) )
13294nncnd 9778 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  CC )
133100adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  n  e.  CC )
134132, 133mulcomd 8872 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  x.  n )  =  ( n  x.  m ) )
135131, 134oveq12d 5892 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  (
m  x.  n ) )  =  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) )
136123, 135eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n )  =  ( ( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) )
137136oveq2d 5890 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( mmu `  n )  x.  (
( ( log `  (
( x  /  n
)  /  m ) )  /  m )  /  n ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
138117, 137eqtrd 2328 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( mmu `  n )  /  n )  x.  ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( ( mmu `  n )  x.  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) ) )
13989, 138sylan2 460 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) )  =  ( ( mmu `  n
)  x.  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
140139sumeq2dv 12192 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( ( mmu `  n )  /  n
)  x.  ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
141110, 140eqtrd 2328 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
142141sumeq2dv 12192 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
143 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( k  =  ( n  x.  m )  ->  (
x  /  k )  =  ( x  / 
( n  x.  m
) ) )
144143fveq2d 5545 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  ( n  x.  m ) ) ) )
145 id 19 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  k  =  ( n  x.  m ) )
146144, 145oveq12d 5892 . . . . . . . . . . . 12  |-  ( k  =  ( n  x.  m )  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) )
147146oveq2d 5890 . . . . . . . . . . 11  |-  ( k  =  ( n  x.  m )  ->  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
1485rpred 10406 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
149 ssrab2 3271 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  k }  C_  NN
150 simprr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  { y  e.  NN  |  y  ||  k } )
151149, 150sseldi 3191 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  NN )
152151, 59syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  ZZ )
153152zred 10133 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  RR )
154 elfznn 10835 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  NN )
155154adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  NN )
156155nnrpd 10405 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  RR+ )
157 rpdivcl 10392 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  k  e.  RR+ )  ->  (
x  /  k )  e.  RR+ )
1585, 156, 157syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( x  /  k
)  e.  RR+ )
159158relogcld 19990 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( log `  (
x  /  k ) )  e.  RR )
160154ad2antrl 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  NN )
161159, 160nndivred 9810 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( log `  (
x  /  k ) )  /  k )  e.  RR )
162153, 161remulcld 8879 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( mmu `  n )  x.  (
( log `  (
x  /  k ) )  /  k ) )  e.  RR )
163162recnd 8877 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( mmu `  n )  x.  (
( log `  (
x  /  k ) )  /  k ) )  e.  CC )
164147, 148, 163dvdsflsumcom 20444 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
165142, 164eqtr4d 2331 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) ) )
166165adantrr 697 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) ) )
167 oveq2 5882 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
x  /  k )  =  ( x  / 
1 ) )
168167fveq2d 5545 . . . . . . . . . 10  |-  ( k  =  1  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  1 ) ) )
169 id 19 . . . . . . . . . 10  |-  ( k  =  1  ->  k  =  1 )
170168, 169oveq12d 5892 . . . . . . . . 9  |-  ( k  =  1  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  1
) )  /  1
) )
171 fzfid 11051 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
1726ssriv 3197 . . . . . . . . . 10  |-  ( 1 ... ( |_ `  x ) )  C_  NN
173172a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) ) 
C_  NN )
174125adantrr 697 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
175 simprr 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
176 flge1nn 10965 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  1  <_  x )  -> 
( |_ `  x
)  e.  NN )
177174, 175, 176syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN )
178 nnuz 10279 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
179177, 178syl6eleq 2386 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  ( ZZ>= ` 
1 ) )
180 eluzfz1 10819 . . . . . . . . . 10  |-  ( ( |_ `  x )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( |_ `  x ) ) )
181179, 180syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ( 1 ... ( |_ `  x ) ) )
182154nnrpd 10405 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  RR+ )
1835, 182, 157syl2an 463 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  k )  e.  RR+ )
184183relogcld 19990 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  k
) )  e.  RR )
185172a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  C_  NN )
186185sselda 3193 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  NN )
187184, 186nndivred 9810 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  RR )
188187recnd 8877 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  CC )
189188adantlrr 701 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  k
) )  /  k
)  e.  CC )
190170, 171, 173, 181, 189musumsum 20448 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) ) sum_ n  e.  { y  e.  NN  |  y  ||  k }  ( (
mmu `  n )  x.  ( ( log `  (
x  /  k ) )  /  k ) )  =  ( ( log `  ( x  /  1 ) )  /  1 ) )
1915rpcnd 10408 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
192191div1d 9544 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  1 )  =  x )
193192fveq2d 5545 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  ( x  /  1
) )  =  ( log `  x ) )
194193oveq1d 5889 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( ( log `  x
)  /  1 ) )
19579div1d 9544 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  / 
1 )  =  ( log `  x ) )
196194, 195eqtrd 2328 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( log `  x ) )
197196adantrr 697 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  (
x  /  1 ) )  /  1 )  =  ( log `  x
) )
198166, 190, 1973eqtrd 2332 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( log `  x ) )
199198oveq2d 5890 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )
200109, 199eqtrd 2328 . . . . 5  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) ) )
201200fveq2d 5545 . . . 4  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
) )  =  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) ) ) )
202 ere 12386 . . . . . . . . 9  |-  _e  e.  RR
203202a1i 10 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  _e  e.  RR )
204 1lt2 9902 . . . . . . . . . 10  |-  1  <  2
205 egt2lt3 12500 . . . . . . . . . . 11  |-  ( 2  <  _e  /\  _e  <  3 )
206205simpli 444 . . . . . . . . . 10  |-  2  <  _e
2071, 3, 202lttri 8961 . . . . . . . . . 10  |-  ( ( 1  <  2  /\  2  <  _e )  ->  1  <  _e )
208204, 206, 207mp2an 653 . . . . . . . . 9  |-  1  <  _e
2091, 202, 208ltleii 8957 . . . . . . . 8  |-  1  <_  _e
210203, 209jctir 524 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( _e  e.  RR  /\  1  <_  _e ) )
21139adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  R  e.  RR )
21218a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
213 1rp 10374 . . . . . . . . . . . . . 14  |-  1  e.  RR+
214 rphalfcl 10394 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
215213, 214ax-mp 8 . . . . . . . . . . . . 13  |-  ( 1  /  2 )  e.  RR+
216 rpge0 10382 . . . . . . . . . . . . 13  |-  ( ( 1  /  2 )  e.  RR+  ->  0  <_ 
( 1  /  2
) )
217215, 216mp1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( 1  /  2 ) )
21819a1i 10 . . . . . . . . . . . . 13  |-  ( ph  -> 
gamma  e.  RR )
219 0re 8854 . . . . . . . . . . . . . . 15  |-  0  e.  RR
220 emgt0 20316 . . . . . . . . . . . . . . 15  |-  0  <  gamma
221219, 19, 220ltleii 8957 . . . . . . . . . . . . . 14  |-  0  <_ 
gamma
222221a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  gamma )
22322absge0d 11942 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  ( abs `  L ) )
224218, 23, 222, 223addge0d 9364 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( gamma  +  ( abs `  L
) ) )
225212, 25, 217, 224addge0d 9364 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( (
1  /  2 )  +  ( gamma  +  ( abs `  L ) ) ) )
226 log1 19955 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
22731nncnd 9778 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  CC )
228227mulid2d 8869 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  =  m )
22932rpred 10406 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR )
2303a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  e.  RR )
231202a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  _e  e.  RR )
232 elfzle2 10816 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... 2 )  ->  m  <_  2 )
233232adantl 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  2 )
2343, 202, 206ltleii 8957 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  _e
235234a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  <_  _e )
236229, 230, 231, 233, 235letrd 8989 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  _e )
237228, 236eqbrtrd 4059 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  <_  _e )
2381a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  e.  RR )
239238, 231, 32lemuldivd 10451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( 1  x.  m
)  <_  _e  <->  1  <_  ( _e  /  m ) ) )
240237, 239mpbid 201 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  <_  ( _e  /  m
) )
241 logleb 19973 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR+  /\  (
_e  /  m )  e.  RR+ )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
242213, 34, 241sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
243240, 242mpbid 201 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  (
_e  /  m )
) )
244226, 243syl5eqbrr 4073 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  (
_e  /  m )
) )
24535, 32, 244divge0d 10442 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  (
_e  /  m )
)  /  m ) )
24628, 36, 245fsumge0 12269 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
24727, 37, 225, 246addge0d 9364 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  + 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m ) ) )
248247, 16syl6breqr 4079 . . . . . . . . 9  |-  ( ph  ->  0  <_  R )
249248adantr 451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <_  R )
250211, 249jca 518 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  e.  RR  /\  0  <_  R ) )
25187, 99mulcld 8871 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  CC )
252 remulcl 8838 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  (
( log `  (
x  /  n ) )  /  x ) )  e.  RR )
2533, 12, 252sylancr 644 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  x
) )  e.  RR )
2543a1i 10 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
255 2pos 9844 . . . . . . . . . 10  |-  0  <  2
256219, 3, 255ltleii 8957 . . . . . . . . 9  |-  0  <_  2
257256a1i 10 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  2 )
258100mulid2d 8869 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
259 fznnfl 10982 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
260125, 259syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( n  e.  ( 1 ... ( |_ `  x ) )  <-> 
( n  e.  NN  /\  n  <_  x )
) )
261260simplbda 607 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
262258, 261eqbrtrd 4059 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
2631a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
26458nnrpd 10405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
265263, 126, 264lemuldivd 10451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
266262, 265mpbid 201 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
267 logleb 19973 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
268213, 9, 267sylancr 644 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
269266, 268mpbid 201 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) )
270226, 269syl5eqbrr 4073 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  ( x  /  n ) ) )
271 rpregt0 10383 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <  x ) )
272271ad2antlr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  RR  /\  0  < 
x ) )
273 divge0 9641 . . . . . . . . 9  |-  ( ( ( ( log `  (
x  /  n ) )  e.  RR  /\  0  <_  ( log `  (
x  /  n ) ) )  /\  (
x  e.  RR  /\  0  <  x ) )  ->  0  <_  (
( log `  (
x  /  n ) )  /  x ) )
27410, 270, 272, 273syl21anc 1181 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) )  /  x ) )
275254, 12, 257, 274mulge0d 9365 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( 2  x.  ( ( log `  ( x  /  n ) )  /  x ) ) )
276251abscld 11934 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  e.  RR )
277276adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  e.  RR )
27899adantr 451 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
279278abscld 11934 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  RR )
280264rpred 10406 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
281253, 280remulcld 8879 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
282281adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
28387, 99absmuld 11952 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  =  ( ( abs `  (
mmu `  n )
)  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) ) ) )
28487abscld 11934 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  e.  RR )
28599abscld 11934 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  RR )
28699absge0d 11942 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
287 mule1 20402 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  ( abs `  ( mmu `  n ) )  <_ 
1 )
28858, 287syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  <_  1
)
289284, 263, 285, 286, 288lemul1ad 9712 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  n ) )  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( 1  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) ) )
290285recnd 8877 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  CC )
291290mulid2d 8869 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  =  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
292289, 291breqtrd 4063 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  n ) )  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
293283, 292eqbrtrd 4059 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
294293adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
295 logdivsum.1 . . . . . . . . . 10  |-  F  =  ( y  e.  RR+  |->  ( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( ( log `  i
)  /  i )  -  ( ( ( log `  y ) ^ 2 )  / 
2 ) ) )
29620ad3antrrr 710 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  F  ~~> r  L
)
2979adantr 451 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( x  /  n )  e.  RR+ )
298 simpr 447 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  _e  <_  ( x  /  n ) )
299295, 296, 297, 298mulog2sumlem1 20699 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) ) )  <_  (
2  x.  ( ( log `  ( x  /  n ) )  /  ( x  /  n ) ) ) )
30074, 98abssubd 11951 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  T ) ) )
301300adantr 451 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  T ) ) )
30264oveq2i 5885 . . . . . . . . . . 11  |-  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  -  T )  =  (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
303302fveq2i 5544 . . . . . . . . . 10  |-  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  T ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) ) )
304301, 303syl6eq 2344 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) ) ) )
30545a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
30612recnd 8877 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  CC )
307305, 306, 100mulassd 8874 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( ( log `  (
x  /  n ) )  /  x )  x.  n ) ) )
308 rpcnne0 10387 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
309308ad2antlr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
310 divdiv2 9488 . . . . . . . . . . . . . 14  |-  ( ( ( log `  (
x  /  n ) )  e.  CC  /\  ( x  e.  CC  /\  x  =/=  0 )  /\  ( n  e.  CC  /\  n  =/=  0 ) )  -> 
( ( log `  (
x  /  n ) )  /  ( x  /  n ) )  =  ( ( ( log `  ( x  /  n ) )  x.  n )  /  x ) )
31165, 309, 112, 310syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  x.  n )  /  x ) )
312 div23 9459 . . . . . . . . . . . . . 14  |-  ( ( ( log `  (
x  /  n ) )  e.  CC  /\  n  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( ( log `  ( x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
31365, 100, 309, 312syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  ( x  /  n
) )  /  x
)  x.  n ) )
314311, 313eqtrd 2328 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
315314oveq2d 5890 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( 2  x.  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) ) )
316307, 315eqtr4d 2331 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( log `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
317316adantr 451 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( log `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
318299, 304, 3173brtr4d 4069 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  <_  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n ) )
319277, 279, 282, 294, 318letrd 8989 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( ( 2  x.  ( ( log `  (
x  /  n ) )  /  x ) )  x.  n ) )
320276adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  e.  RR )
321285adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  e.  RR )
32239ad3antrrr 710 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  R  e.  RR )
323293adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
32474adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  T  e.  CC )
325324abscld 11934 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  T
)  e.  RR )
32698adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
327326abscld 11934 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) )  e.  RR )
328325, 327readdcld 8878 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( abs `  T )  +  ( abs `  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  e.  RR )
329324, 326abs2dif2d 11956 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  <_  (
( abs `  T
)  +  ( abs `  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
33027ad3antrrr 710 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  e.  RR )
33137ad3antrrr 710 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
33264fveq2i 5544 . . . . . . . . . . . 12  |-  ( abs `  T )  =  ( abs `  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
333332, 325syl5eqelr 2381 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
) ) )  e.  RR )
33467adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  e.  CC )
335334abscld 11934 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  e.  RR )
33672adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
337336abscld 11934 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) )  e.  RR )
338335, 337readdcld 8878 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  +  ( abs `  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )  e.  RR )
339334, 336abstrid 11954 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
) ) )  <_ 
( ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  +  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) ) ) )
34018a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( 1  / 
2 )  e.  RR )
34125ad3antrrr 710 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
34210resqcld 11287 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  RR )
343342rehalfcld 9974 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  RR )
34410sqge0d 11288 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) ) ^ 2 ) )
3453, 255pm3.2i 441 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  e.  RR  /\  0  <  2 )
346345a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
347 divge0 9641 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( log `  ( x  /  n
) ) ^ 2 )  e.  RR  /\  0  <_  ( ( log `  ( x  /  n
) ) ^ 2 ) )  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  0  <_  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
348342, 344, 346, 347syl21anc 1181 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
349343, 348absidd 11921 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
350349adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 ) )
3519rpred 10406 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
352 ltle 8926 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  /  n
)  e.  RR  /\  _e  e.  RR )  -> 
( ( x  /  n )  <  _e  ->  ( x  /  n
)  <_  _e )
)
353351, 202, 352sylancl 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  n )  <  _e  ->  (
x  /  n )  <_  _e ) )
354353imp 418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_