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

Theorem mulog2sumlem2 24350
Description: Lemma for mulog2sum 24352. (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 1red 9654 . 2  |-  ( ph  ->  1  e.  RR )
2 2re 10675 . . . 4  |-  2  e.  RR
3 fzfid 12179 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
4 simpr 462 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR+ )
5 elfznn 11822 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
65nnrpd 11335 . . . . . . . 8  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
7 rpdivcl 11321 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
84, 6, 7syl2an 479 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
98relogcld 23549 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
10 simplr 760 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
119, 10rerpdivcld 11365 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  RR )
123, 11fsumrecl 13778 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )
13 remulcl 9620 . . . 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 )
142, 12, 13sylancr 667 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  RR )
15 mulog2sumlem2.r . . . . . 6  |-  R  =  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
16 halfre 10824 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
17 emre 23908 . . . . . . . . 9  |-  gamma  e.  RR
18 mulog2sumlem.1 . . . . . . . . . . 11  |-  ( ph  ->  F  ~~> r  L )
19 rlimcl 13545 . . . . . . . . . . 11  |-  ( F  ~~> r  L  ->  L  e.  CC )
2018, 19syl 17 . . . . . . . . . 10  |-  ( ph  ->  L  e.  CC )
2120abscld 13476 . . . . . . . . 9  |-  ( ph  ->  ( abs `  L
)  e.  RR )
22 readdcl 9618 . . . . . . . . 9  |-  ( (
gamma  e.  RR  /\  ( abs `  L )  e.  RR )  ->  ( gamma  +  ( abs `  L
) )  e.  RR )
2317, 21, 22sylancr 667 . . . . . . . 8  |-  ( ph  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
24 readdcl 9618 . . . . . . . 8  |-  ( ( ( 1  /  2
)  e.  RR  /\  ( gamma  +  ( abs `  L ) )  e.  RR )  ->  (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  e.  RR )
2516, 23, 24sylancr 667 . . . . . . 7  |-  ( ph  ->  ( ( 1  / 
2 )  +  (
gamma  +  ( abs `  L
) ) )  e.  RR )
26 fzfid 12179 . . . . . . . 8  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
27 epr 14238 . . . . . . . . . . 11  |-  _e  e.  RR+
28 elfznn 11822 . . . . . . . . . . . . 13  |-  ( m  e.  ( 1 ... 2 )  ->  m  e.  NN )
2928adantl 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  NN )
3029nnrpd 11335 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
31 rpdivcl 11321 . . . . . . . . . . 11  |-  ( ( _e  e.  RR+  /\  m  e.  RR+ )  ->  (
_e  /  m )  e.  RR+ )
3227, 30, 31sylancr 667 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
_e  /  m )  e.  RR+ )
3332relogcld 23549 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  ( _e  /  m ) )  e.  RR )
3433, 29nndivred 10654 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( log `  (
_e  /  m )
)  /  m )  e.  RR )
3526, 34fsumrecl 13778 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
3625, 35readdcld 9666 . . . . . 6  |-  ( ph  ->  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )  e.  RR )
3715, 36syl5eqel 2512 . . . . 5  |-  ( ph  ->  R  e.  RR )
38 remulcl 9620 . . . . 5  |-  ( ( R  e.  RR  /\  2  e.  RR )  ->  ( R  x.  2 )  e.  RR )
3937, 2, 38sylancl 666 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  RR )
4039adantr 466 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  x.  2 )  e.  RR )
412a1i 11 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  RR )
42 rpssre 11308 . . . . 5  |-  RR+  C_  RR
43 2cnd 10678 . . . . 5  |-  ( ph  ->  2  e.  CC )
44 o1const 13661 . . . . 5  |-  ( (
RR+  C_  RR  /\  2  e.  CC )  ->  (
x  e.  RR+  |->  2 )  e.  O(1) )
4542, 43, 44sylancr 667 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  2 )  e.  O(1) )
46 logfacrlim2 24131 . . . . 5  |-  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1
47 rlimo1 13658 . . . . 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) )
4846, 47mp1i 13 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  O(1) )
4941, 12, 45, 48o1mul2 13666 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) ) )  e.  O(1) )
5039recnd 9665 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  CC )
51 o1const 13661 . . . 4  |-  ( (
RR+  C_  RR  /\  ( R  x.  2 )  e.  CC )  -> 
( x  e.  RR+  |->  ( R  x.  2
) )  e.  O(1) )
5242, 50, 51sylancr 667 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( R  x.  2
) )  e.  O(1) )
5314, 40, 49, 52o1add2 13665 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  O(1) )
5414, 40readdcld 9666 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
555adantl 467 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
56 mucl 24045 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
mmu `  n )  e.  ZZ )
5755, 56syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  ZZ )
5857zred 11036 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  RR )
5958, 55nndivred 10654 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  RR )
6059recnd 9665 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  CC )
61 mulog2sumlem2.t . . . . . 6  |-  T  =  ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )
629recnd 9665 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
6362sqcld 12407 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  CC )
6463halfcld 10853 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  CC )
65 remulcl 9620 . . . . . . . . . 10  |-  ( (
gamma  e.  RR  /\  ( log `  ( x  /  n ) )  e.  RR )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6617, 9, 65sylancr 667 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6766recnd 9665 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  CC )
6820ad2antrr 730 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  L  e.  CC )
6967, 68subcld 9982 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
7064, 69addcld 9658 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )  e.  CC )
7161, 70syl5eqel 2512 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
7260, 71mulcld 9659 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  T )  e.  CC )
733, 72fsumcl 13777 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  e.  CC )
74 relogcl 23502 . . . . 5  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
7574adantl 467 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
7675recnd 9665 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
7773, 76subcld 9982 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) )  e.  CC )
7877abscld 13476 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
7978adantrr 721 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8054adantrr 721 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
8154recnd 9665 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  CC )
8281abscld 13476 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8382adantrr 721 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8457zcnd 11037 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  CC )
85 fzfid 12179 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
86 elfznn 11822 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
87 nnrp 11307 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN  ->  m  e.  RR+ )
88 rpdivcl 11321 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  /  n
)  e.  RR+  /\  m  e.  RR+ )  ->  (
( x  /  n
)  /  m )  e.  RR+ )
898, 87, 88syl2an 479 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  e.  RR+ )
9089relogcld 23549 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  RR )
91 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  NN )
9290, 91nndivred 10654 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  RR )
9392recnd 9665 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  CC )
9486, 93sylan2 476 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  e.  CC )
9585, 94fsumcl 13777 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
9671, 95subcld 9982 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
9755nncnd 10621 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
9855nnne0d 10650 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
9984, 96, 97, 98div23d 10416 . . . . . . . . . 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 ) ) ) )
10060, 71, 95subdid 10070 . . . . . . . . . 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 ) ) ) )
10199, 100eqtrd 2461 . . . . . . . . 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 ) ) ) )
102101sumeq2dv 13747 . . . . . . . 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 ) ) ) )
10360, 95mulcld 9659 . . . . . . . . 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 )
1043, 72, 103fsumsub 13827 . . . . . . . 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 ) ) ) )
105102, 104eqtrd 2461 . . . . . . 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 ) ) ) )
106105adantrr 721 . . . . . 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 ) ) ) )
10785, 60, 94fsummulc2 13823 . . . . . . . . . . . 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 ) ) )
10884adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( mmu `  n )  e.  CC )
10997, 98jca 534 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
110109adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
111 div23 10285 . . . . . . . . . . . . . . . . 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
) ) )
112 divass 10284 . . . . . . . . . . . . . . . . 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 ) ) )
113111, 112eqtr3d 2463 . . . . . . . . . . . . . . . 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 ) ) )
114108, 93, 110, 113syl3anc 1264 . . . . . . . . . . . . . . 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 ) ) )
11590recnd 9665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  CC )
11691nnrpd 11335 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  RR+ )
117 rpcnne0 11315 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
118116, 117syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  e.  CC  /\  m  =/=  0 ) )
119 divdiv1 10314 . . . . . . . . . . . . . . . . . 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 ) ) )
120115, 118, 110, 119syl3anc 1264 . . . . . . . . . . . . . . . . 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 ) ) )
121 rpre 11304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR+  ->  x  e.  RR )
122121adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
123122adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
124123recnd 9665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
125124adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  x  e.  CC )
126 divdiv1 10314 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  CC  /\  ( n  e.  CC  /\  n  =/=  0 )  /\  ( m  e.  CC  /\  m  =/=  0 ) )  -> 
( ( x  /  n )  /  m
)  =  ( x  /  ( n  x.  m ) ) )
127125, 110, 118, 126syl3anc 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  =  ( x  /  ( n  x.  m ) ) )
128127fveq2d 5877 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  =  ( log `  ( x  /  (
n  x.  m ) ) ) )
12991nncnd 10621 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  CC )
13097adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  n  e.  CC )
131129, 130mulcomd 9660 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  x.  n )  =  ( n  x.  m ) )
132128, 131oveq12d 6315 . . . . . . . . . . . . . . . . 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 ) ) )
133120, 132eqtrd 2461 . . . . . . . . . . . . . . . 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 ) ) )
134133oveq2d 6313 . . . . . . . . . . . . . . 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 ) ) ) )
135114, 134eqtrd 2461 . . . . . . . . . . . . . 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 ) ) ) )
13686, 135sylan2 476 . . . . . . . . . . . . 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 ) ) ) )
137136sumeq2dv 13747 . . . . . . . . . . . 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 ) ) ) )
138107, 137eqtrd 2461 . . . . . . . . . . 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 ) ) ) )
139138sumeq2dv 13747 . . . . . . . . . 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 ) ) ) )
140 oveq2 6305 . . . . . . . . . . . . . 14  |-  ( k  =  ( n  x.  m )  ->  (
x  /  k )  =  ( x  / 
( n  x.  m
) ) )
141140fveq2d 5877 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  ( n  x.  m ) ) ) )
142 id 23 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  k  =  ( n  x.  m ) )
143141, 142oveq12d 6315 . . . . . . . . . . . 12  |-  ( k  =  ( n  x.  m )  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) )
144143oveq2d 6313 . . . . . . . . . . 11  |-  ( k  =  ( n  x.  m )  ->  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
1454rpred 11337 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
146 ssrab2 3543 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  k }  C_  NN
147 simprr 764 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  { y  e.  NN  |  y  ||  k } )
148146, 147sseldi 3459 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  NN )
149148, 56syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  ZZ )
150149zred 11036 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  RR )
151 elfznn 11822 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  NN )
152151adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  NN )
153152nnrpd 11335 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  RR+ )
154 rpdivcl 11321 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  k  e.  RR+ )  ->  (
x  /  k )  e.  RR+ )
1554, 153, 154syl2an 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( x  /  k
)  e.  RR+ )
156155relogcld 23549 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( log `  (
x  /  k ) )  e.  RR )
157151ad2antrl 732 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  NN )
158156, 157nndivred 10654 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( log `  (
x  /  k ) )  /  k )  e.  RR )
159150, 158remulcld 9667 . . . . . . . . . . . 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 )
160159recnd 9665 . . . . . . . . . . 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 )
161144, 145, 160dvdsflsumcom 24094 . . . . . . . . . 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 ) ) ) )
162139, 161eqtr4d 2464 . . . . . . . . 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 ) ) )
163162adantrr 721 . . . . . . . 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 ) ) )
164 oveq2 6305 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
x  /  k )  =  ( x  / 
1 ) )
165164fveq2d 5877 . . . . . . . . . 10  |-  ( k  =  1  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  1 ) ) )
166 id 23 . . . . . . . . . 10  |-  ( k  =  1  ->  k  =  1 )
167165, 166oveq12d 6315 . . . . . . . . 9  |-  ( k  =  1  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  1
) )  /  1
) )
168 fzfid 12179 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
1695ssriv 3465 . . . . . . . . . 10  |-  ( 1 ... ( |_ `  x ) )  C_  NN
170169a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) ) 
C_  NN )
171122adantrr 721 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
172 simprr 764 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
173 flge1nn 12048 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  1  <_  x )  -> 
( |_ `  x
)  e.  NN )
174171, 172, 173syl2anc 665 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN )
175 nnuz 11190 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
176174, 175syl6eleq 2518 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  ( ZZ>= ` 
1 ) )
177 eluzfz1 11800 . . . . . . . . . 10  |-  ( ( |_ `  x )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( |_ `  x ) ) )
178176, 177syl 17 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ( 1 ... ( |_ `  x ) ) )
179151nnrpd 11335 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  RR+ )
1804, 179, 154syl2an 479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  k )  e.  RR+ )
181180relogcld 23549 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  k
) )  e.  RR )
182169a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  C_  NN )
183182sselda 3461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  NN )
184181, 183nndivred 10654 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  RR )
185184recnd 9665 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  CC )
186185adantlrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  k
) )  /  k
)  e.  CC )
187167, 168, 170, 178, 186musumsum 24098 . . . . . . . 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 ) )
1884rpcnd 11339 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
189188div1d 10371 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  1 )  =  x )
190189fveq2d 5877 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  ( x  /  1
) )  =  ( log `  x ) )
191190oveq1d 6312 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( ( log `  x
)  /  1 ) )
19276div1d 10371 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  / 
1 )  =  ( log `  x ) )
193191, 192eqtrd 2461 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( log `  x ) )
194193adantrr 721 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  (
x  /  1 ) )  /  1 )  =  ( log `  x
) )
195163, 187, 1943eqtrd 2465 . . . . . . 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 ) )
196195oveq2d 6313 . . . . . 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
) ) )
197106, 196eqtrd 2461 . . . . 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 ) ) )
198197fveq2d 5877 . . . 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 ) ) ) )
199 ere 14121 . . . . . . . . 9  |-  _e  e.  RR
200199a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  _e  e.  RR )
201 1re 9638 . . . . . . . . 9  |-  1  e.  RR
202 1lt2 10772 . . . . . . . . . 10  |-  1  <  2
203 egt2lt3 14236 . . . . . . . . . . 11  |-  ( 2  <  _e  /\  _e  <  3 )
204203simpli 459 . . . . . . . . . 10  |-  2  <  _e
205201, 2, 199lttri 9756 . . . . . . . . . 10  |-  ( ( 1  <  2  /\  2  <  _e )  ->  1  <  _e )
206202, 204, 205mp2an 676 . . . . . . . . 9  |-  1  <  _e
207201, 199, 206ltleii 9753 . . . . . . . 8  |-  1  <_  _e
208200, 207jctir 540 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( _e  e.  RR  /\  1  <_  _e ) )
20937adantr 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  R  e.  RR )
21016a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
211 1rp 11302 . . . . . . . . . . . . . 14  |-  1  e.  RR+
212 rphalfcl 11323 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
213211, 212ax-mp 5 . . . . . . . . . . . . 13  |-  ( 1  /  2 )  e.  RR+
214 rpge0 11310 . . . . . . . . . . . . 13  |-  ( ( 1  /  2 )  e.  RR+  ->  0  <_ 
( 1  /  2
) )
215213, 214mp1i 13 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( 1  /  2 ) )
21617a1i 11 . . . . . . . . . . . . 13  |-  ( ph  -> 
gamma  e.  RR )
217 0re 9639 . . . . . . . . . . . . . . 15  |-  0  e.  RR
218 emgt0 23909 . . . . . . . . . . . . . . 15  |-  0  <  gamma
219217, 17, 218ltleii 9753 . . . . . . . . . . . . . 14  |-  0  <_ 
gamma
220219a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  gamma )
22120absge0d 13484 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  ( abs `  L ) )
222216, 21, 220, 221addge0d 10185 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( gamma  +  ( abs `  L
) ) )
223210, 23, 215, 222addge0d 10185 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( (
1  /  2 )  +  ( gamma  +  ( abs `  L ) ) ) )
224 log1 23512 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
22529nncnd 10621 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  CC )
226225mulid2d 9657 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  =  m )
22730rpred 11337 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR )
2282a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  e.  RR )
229199a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  _e  e.  RR )
230 elfzle2 11797 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... 2 )  ->  m  <_  2 )
231230adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  2 )
2322, 199, 204ltleii 9753 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  _e
233232a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  <_  _e )
234227, 228, 229, 231, 233letrd 9788 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  _e )
235226, 234eqbrtrd 4438 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  <_  _e )
236 1red 9654 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  e.  RR )
237236, 229, 30lemuldivd 11383 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( 1  x.  m
)  <_  _e  <->  1  <_  ( _e  /  m ) ) )
238235, 237mpbid 213 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  <_  ( _e  /  m
) )
239 logleb 23529 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR+  /\  (
_e  /  m )  e.  RR+ )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
240211, 32, 239sylancr 667 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
241238, 240mpbid 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  (
_e  /  m )
) )
242224, 241syl5eqbrr 4452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  (
_e  /  m )
) )
24333, 30, 242divge0d 11374 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  (
_e  /  m )
)  /  m ) )
24426, 34, 243fsumge0 13833 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
24525, 35, 223, 244addge0d 10185 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  + 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m ) ) )
246245, 15syl6breqr 4458 . . . . . . . . 9  |-  ( ph  ->  0  <_  R )
247246adantr 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <_  R )
248209, 247jca 534 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  e.  RR  /\  0  <_  R ) )
24984, 96mulcld 9659 . . . . . . 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 )
250 remulcl 9620 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  (
( log `  (
x  /  n ) )  /  x ) )  e.  RR )
2512, 11, 250sylancr 667 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  x
) )  e.  RR )
2522a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
253 0le2 10696 . . . . . . . . 9  |-  0  <_  2
254253a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  2 )
25597mulid2d 9657 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
256 fznnfl 12082 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
257122, 256syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( n  e.  ( 1 ... ( |_ `  x ) )  <-> 
( n  e.  NN  /\  n  <_  x )
) )
258257simplbda 628 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
259255, 258eqbrtrd 4438 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
260 1red 9654 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
26155nnrpd 11335 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
262260, 123, 261lemuldivd 11383 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
263259, 262mpbid 213 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
264 logleb 23529 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
265211, 8, 264sylancr 667 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
266263, 265mpbid 213 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) )
267224, 266syl5eqbrr 4452 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  ( x  /  n ) ) )
268 rpregt0 11311 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <  x ) )
269268ad2antlr 731 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  RR  /\  0  < 
x ) )
270 divge0 10470 . . . . . . . . 9  |-  ( ( ( ( log `  (
x  /  n ) )  e.  RR  /\  0  <_  ( log `  (
x  /  n ) ) )  /\  (
x  e.  RR  /\  0  <  x ) )  ->  0  <_  (
( log `  (
x  /  n ) )  /  x ) )
2719, 267, 269, 270syl21anc 1263 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) )  /  x ) )
272252, 11, 254, 271mulge0d 10186 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( 2  x.  ( ( log `  ( x  /  n ) )  /  x ) ) )
273249abscld 13476 . . . . . . . . 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 )
274273adantr 466 . . . . . . . 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 )
27596adantr 466 . . . . . . . . 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 )
276275abscld 13476 . . . . . . . 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 )
277261rpred 11337 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
278251, 277remulcld 9667 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
279278adantr 466 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
28084, 96absmuld 13494 . . . . . . . . . 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 ) ) ) ) )
28184abscld 13476 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  e.  RR )
28296abscld 13476 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  RR )
28396absge0d 13484 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
284 mule1 24052 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  ( abs `  ( mmu `  n ) )  <_ 
1 )
28555, 284syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  <_  1
)
286281, 260, 282, 283, 285lemul1ad 10542 . . . . . . . . . . 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 ) ) ) ) )
287282recnd 9665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  CC )
288287mulid2d 9657 . . . . . . . . . . 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 ) ) ) )
289286, 288breqtrd 4442 . . . . . . . . . 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 ) ) ) )
290280, 289eqbrtrd 4438 . . . . . . . . 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 ) ) ) )
291290adantr 466 . . . . . . . 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 ) ) ) )
292 logdivsum.1 . . . . . . . . . 10  |-  F  =  ( y  e.  RR+  |->  ( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( ( log `  i
)  /  i )  -  ( ( ( log `  y ) ^ 2 )  / 
2 ) ) )
29318ad3antrrr 734 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  F  ~~> r  L
)
2948adantr 466 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( x  /  n )  e.  RR+ )
295 simpr 462 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  _e  <_  ( x  /  n ) )
296292, 293, 294, 295mulog2sumlem1 24349 . . . . . . . . 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 ) ) ) )
29771, 95abssubd 13493 . . . . . . . . . . 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 ) ) )
298297adantr 466 . . . . . . . . . 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 ) ) )
29961oveq2i 6308 . . . . . . . . . . 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 ) ) )
300299fveq2i 5876 . . . . . . . . . 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 ) ) ) )
301298, 300syl6eq 2477 . . . . . . . . 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 ) ) ) ) )
302 2cnd 10678 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
30311recnd 9665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  CC )
304302, 303, 97mulassd 9662 . . . . . . . . . . 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 ) ) )
305 rpcnne0 11315 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
306305ad2antlr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
307 divdiv2 10315 . . . . . . . . . . . . . 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 ) )
30862, 306, 109, 307syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  x.  n )  /  x ) )
309 div23 10285 . . . . . . . . . . . . . 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 ) )
31062, 97, 306, 309syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  ( x  /  n
) )  /  x
)  x.  n ) )
311308, 310eqtrd 2461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
312311oveq2d 6313 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( 2  x.  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) ) )
313304, 312eqtr4d 2464 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( log `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
314313adantr 466 . . . . . . . . 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 ) ) ) )
315296, 301, 3143brtr4d 4448 . . . . . . . 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 ) )
316274, 276, 279, 291, 315letrd 9788 . . . . . . 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 ) )
317273adantr 466 . . . . . . . 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 )
318282adantr 466 . . . . . . . 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 )
31937ad3antrrr 734 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  R  e.  RR )
320290adantr 466 . . . . . . . 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 ) ) ) )
32171adantr 466 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  T  e.  CC )
322321abscld 13476 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  T
)  e.  RR )
32395adantr 466 . . . . . . . . . . 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 )
324323abscld 13476 . . . . . . . . . 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 )
325322, 324readdcld 9666 . . . . . . . . 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 )
326321, 323abs2dif2d 13498 . . . . . . . . 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 ) ) ) )
32725ad3antrrr 734 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  e.  RR )
32835ad3antrrr 734 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
32961fveq2i 5876 . . . . . . . . . . . 12  |-  ( abs `  T )  =  ( abs `  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
330329, 322syl5eqelr 2513 . . . . . . . . . . . . 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 )
33164adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  e.  CC )
332331abscld 13476 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  e.  RR )
33369adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
334333abscld 13476 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) )  e.  RR )
335332, 334readdcld 9666 . . . . . . . . . . . . 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 )
336331, 333abstrid 13496 . . . . . . . . . . . . 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 ) ) ) )
33716a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( 1  / 
2 )  e.  RR )
33823ad3antrrr 734 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
3399resqcld 12435 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  RR )
340339rehalfcld 10855 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  RR )
3419sqge0d 12436 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) ) ^ 2 ) )
342 2pos 10697 . . . . . . . . . . . . . . . . . . . 20  |-  0  <  2
3432, 342pm3.2i 456 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  e.  RR  /\  0  <  2 )
344343a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
345 divge0 10470 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( log `  ( x  /  n
) ) ^ 2 )  e.  RR  /\  0  <_  ( ( log `  ( x  /  n
) ) ^ 2 ) )  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  0  <_  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
346339, 341, 344, 345syl21anc 1263 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
347340, 346absidd 13463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
348347adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 ) )
3498rpred 11337 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
350 ltle 9718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  /  n
)  e.  RR  /\  _e  e.  RR )  -> 
( ( x  /  n )  <  _e  ->  ( x  /  n
)  <_  _e )
)
351349, 199, 350sylancl 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  n )  <  _e  ->  (
x  /  n )  <_  _e ) )
352351imp 430 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( x  /  n )  <_  _e )
3538adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e