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

Theorem mulog2sumlem2 22753
Description: Lemma for mulog2sum 22755. (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 9393 . 2  |-  ( ph  ->  1  e.  RR )
2 2re 10383 . . . 4  |-  2  e.  RR
3 fzfid 11787 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
4 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR+ )
5 elfznn 11470 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
65nnrpd 11018 . . . . . . . 8  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
7 rpdivcl 11005 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
84, 6, 7syl2an 477 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
98relogcld 22041 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
10 simplr 754 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
119, 10rerpdivcld 11046 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  RR )
123, 11fsumrecl 13203 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )
13 remulcl 9359 . . . 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 663 . . 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 10532 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
17 emre 22368 . . . . . . . . 9  |-  gamma  e.  RR
18 mulog2sumlem.1 . . . . . . . . . . 11  |-  ( ph  ->  F  ~~> r  L )
19 rlimcl 12973 . . . . . . . . . . 11  |-  ( F  ~~> r  L  ->  L  e.  CC )
2018, 19syl 16 . . . . . . . . . 10  |-  ( ph  ->  L  e.  CC )
2120abscld 12914 . . . . . . . . 9  |-  ( ph  ->  ( abs `  L
)  e.  RR )
22 readdcl 9357 . . . . . . . . 9  |-  ( (
gamma  e.  RR  /\  ( abs `  L )  e.  RR )  ->  ( gamma  +  ( abs `  L
) )  e.  RR )
2317, 21, 22sylancr 663 . . . . . . . 8  |-  ( ph  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
24 readdcl 9357 . . . . . . . 8  |-  ( ( ( 1  /  2
)  e.  RR  /\  ( gamma  +  ( abs `  L ) )  e.  RR )  ->  (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  e.  RR )
2516, 23, 24sylancr 663 . . . . . . 7  |-  ( ph  ->  ( ( 1  / 
2 )  +  (
gamma  +  ( abs `  L
) ) )  e.  RR )
26 fzfid 11787 . . . . . . . 8  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
27 epr 13482 . . . . . . . . . . 11  |-  _e  e.  RR+
28 elfznn 11470 . . . . . . . . . . . . 13  |-  ( m  e.  ( 1 ... 2 )  ->  m  e.  NN )
2928adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  NN )
3029nnrpd 11018 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
31 rpdivcl 11005 . . . . . . . . . . 11  |-  ( ( _e  e.  RR+  /\  m  e.  RR+ )  ->  (
_e  /  m )  e.  RR+ )
3227, 30, 31sylancr 663 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
_e  /  m )  e.  RR+ )
3332relogcld 22041 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  ( _e  /  m ) )  e.  RR )
3433, 29nndivred 10362 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( log `  (
_e  /  m )
)  /  m )  e.  RR )
3526, 34fsumrecl 13203 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
3625, 35readdcld 9405 . . . . . 6  |-  ( ph  ->  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )  e.  RR )
3715, 36syl5eqel 2521 . . . . 5  |-  ( ph  ->  R  e.  RR )
38 remulcl 9359 . . . . 5  |-  ( ( R  e.  RR  /\  2  e.  RR )  ->  ( R  x.  2 )  e.  RR )
3937, 2, 38sylancl 662 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  RR )
4039adantr 465 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  x.  2 )  e.  RR )
412a1i 11 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  RR )
42 rpssre 10993 . . . . 5  |-  RR+  C_  RR
43 2cnd 10386 . . . . 5  |-  ( ph  ->  2  e.  CC )
44 o1const 13089 . . . . 5  |-  ( (
RR+  C_  RR  /\  2  e.  CC )  ->  (
x  e.  RR+  |->  2 )  e.  O(1) )
4542, 43, 44sylancr 663 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  2 )  e.  O(1) )
46 logfacrlim2 22534 . . . . 5  |-  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1
47 rlimo1 13086 . . . . 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 12 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  O(1) )
4941, 12, 45, 48o1mul2 13094 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) ) )  e.  O(1) )
5039recnd 9404 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  CC )
51 o1const 13089 . . . 4  |-  ( (
RR+  C_  RR  /\  ( R  x.  2 )  e.  CC )  -> 
( x  e.  RR+  |->  ( R  x.  2
) )  e.  O(1) )
5242, 50, 51sylancr 663 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( R  x.  2
) )  e.  O(1) )
5314, 40, 49, 52o1add2 13093 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  O(1) )
5414, 40readdcld 9405 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
555adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
56 mucl 22448 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
mmu `  n )  e.  ZZ )
5755, 56syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  ZZ )
5857zred 10739 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  RR )
5958, 55nndivred 10362 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  RR )
6059recnd 9404 . . . . 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 9404 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
6362sqcld 11998 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  CC )
6463halfcld 10561 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  CC )
65 remulcl 9359 . . . . . . . . . 10  |-  ( (
gamma  e.  RR  /\  ( log `  ( x  /  n ) )  e.  RR )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6617, 9, 65sylancr 663 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6766recnd 9404 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  CC )
6820ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  L  e.  CC )
6967, 68subcld 9711 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
7064, 69addcld 9397 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )  e.  CC )
7161, 70syl5eqel 2521 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
7260, 71mulcld 9398 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  T )  e.  CC )
733, 72fsumcl 13202 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  e.  CC )
74 relogcl 21996 . . . . 5  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
7574adantl 466 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
7675recnd 9404 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
7773, 76subcld 9711 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) )  e.  CC )
7877abscld 12914 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
7978adantrr 716 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8054adantrr 716 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
8154recnd 9404 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  CC )
8281abscld 12914 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8382adantrr 716 . . 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 10740 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  CC )
85 fzfid 11787 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
86 elfznn 11470 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
87 nnrp 10992 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN  ->  m  e.  RR+ )
88 rpdivcl 11005 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  /  n
)  e.  RR+  /\  m  e.  RR+ )  ->  (
( x  /  n
)  /  m )  e.  RR+ )
898, 87, 88syl2an 477 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  e.  RR+ )
9089relogcld 22041 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  RR )
91 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  NN )
9290, 91nndivred 10362 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  RR )
9392recnd 9404 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  CC )
9486, 93sylan2 474 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  e.  CC )
9585, 94fsumcl 13202 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
9671, 95subcld 9711 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
9755nncnd 10330 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
9855nnne0d 10358 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
9984, 96, 97, 98div23d 10136 . . . . . . . . . 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 9792 . . . . . . . . . 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 2469 . . . . . . . . 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 13172 . . . . . . . 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 9398 . . . . . . . . 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 13247 . . . . . . . 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 2469 . . . . . . 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 716 . . . . . 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 13243 . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( mmu `  n )  e.  CC )
10997, 98jca 532 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
110109adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
111 div23 10005 . . . . . . . . . . . . . . . . 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 10004 . . . . . . . . . . . . . . . . 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 2471 . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . 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 9404 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  CC )
11691nnrpd 11018 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  RR+ )
117 rpcnne0 11000 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
118116, 117syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  e.  CC  /\  m  =/=  0 ) )
119 divdiv1 10034 . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . 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 10989 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR+  ->  x  e.  RR )
122121adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
123122adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
124123recnd 9404 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
125124adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  x  e.  CC )
126 divdiv1 10034 . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  =  ( x  /  ( n  x.  m ) ) )
128127fveq2d 5688 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  =  ( log `  ( x  /  (
n  x.  m ) ) ) )
12991nncnd 10330 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  CC )
13097adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  n  e.  CC )
131129, 130mulcomd 9399 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  x.  n )  =  ( n  x.  m ) )
132128, 131oveq12d 6104 . . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . 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 13172 . . . . . . . . . . . 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 2469 . . . . . . . . . . 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 13172 . . . . . . . . . 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 6094 . . . . . . . . . . . . . 14  |-  ( k  =  ( n  x.  m )  ->  (
x  /  k )  =  ( x  / 
( n  x.  m
) ) )
141140fveq2d 5688 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  ( n  x.  m ) ) ) )
142 id 22 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  k  =  ( n  x.  m ) )
143141, 142oveq12d 6104 . . . . . . . . . . . 12  |-  ( k  =  ( n  x.  m )  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) )
144143oveq2d 6102 . . . . . . . . . . 11  |-  ( k  =  ( n  x.  m )  ->  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
1454rpred 11019 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
146 ssrab2 3430 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  k }  C_  NN
147 simprr 756 . . . . . . . . . . . . . . . 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 3347 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  NN )
149148, 56syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  ZZ )
150149zred 10739 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  RR )
151 elfznn 11470 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  NN )
152151adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  NN )
153152nnrpd 11018 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  RR+ )
154 rpdivcl 11005 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  k  e.  RR+ )  ->  (
x  /  k )  e.  RR+ )
1554, 153, 154syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( x  /  k
)  e.  RR+ )
156155relogcld 22041 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( log `  (
x  /  k ) )  e.  RR )
157151ad2antrl 727 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  NN )
158156, 157nndivred 10362 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( log `  (
x  /  k ) )  /  k )  e.  RR )
159150, 158remulcld 9406 . . . . . . . . . . . 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 9404 . . . . . . . . . . 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 22497 . . . . . . . . . 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 2472 . . . . . . . . 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 716 . . . . . . . 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 6094 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
x  /  k )  =  ( x  / 
1 ) )
165164fveq2d 5688 . . . . . . . . . 10  |-  ( k  =  1  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  1 ) ) )
166 id 22 . . . . . . . . . 10  |-  ( k  =  1  ->  k  =  1 )
167165, 166oveq12d 6104 . . . . . . . . 9  |-  ( k  =  1  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  1
) )  /  1
) )
168 fzfid 11787 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
1695ssriv 3353 . . . . . . . . . 10  |-  ( 1 ... ( |_ `  x ) )  C_  NN
170169a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) ) 
C_  NN )
171122adantrr 716 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
172 simprr 756 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
173 flge1nn 11659 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  1  <_  x )  -> 
( |_ `  x
)  e.  NN )
174171, 172, 173syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN )
175 nnuz 10888 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
176174, 175syl6eleq 2527 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  ( ZZ>= ` 
1 ) )
177 eluzfz1 11450 . . . . . . . . . 10  |-  ( ( |_ `  x )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( |_ `  x ) ) )
178176, 177syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ( 1 ... ( |_ `  x ) ) )
179151nnrpd 11018 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  RR+ )
1804, 179, 154syl2an 477 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  k )  e.  RR+ )
181180relogcld 22041 . . . . . . . . . . . 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 3349 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  NN )
184181, 183nndivred 10362 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  RR )
185184recnd 9404 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  CC )
186185adantlrr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  k
) )  /  k
)  e.  CC )
187167, 168, 170, 178, 186musumsum 22501 . . . . . . . 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 11021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
189188div1d 10091 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  1 )  =  x )
190189fveq2d 5688 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  ( x  /  1
) )  =  ( log `  x ) )
191190oveq1d 6101 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( ( log `  x
)  /  1 ) )
19276div1d 10091 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  / 
1 )  =  ( log `  x ) )
193191, 192eqtrd 2469 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( log `  x ) )
194193adantrr 716 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  (
x  /  1 ) )  /  1 )  =  ( log `  x
) )
195163, 187, 1943eqtrd 2473 . . . . . . 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 6102 . . . . . 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 2469 . . . . 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 5688 . . . 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 13366 . . . . . . . . 9  |-  _e  e.  RR
200199a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  _e  e.  RR )
201 1re 9377 . . . . . . . . 9  |-  1  e.  RR
202 1lt2 10480 . . . . . . . . . 10  |-  1  <  2
203 egt2lt3 13480 . . . . . . . . . . 11  |-  ( 2  <  _e  /\  _e  <  3 )
204203simpli 458 . . . . . . . . . 10  |-  2  <  _e
205201, 2, 199lttri 9492 . . . . . . . . . 10  |-  ( ( 1  <  2  /\  2  <  _e )  ->  1  <  _e )
206202, 204, 205mp2an 672 . . . . . . . . 9  |-  1  <  _e
207201, 199, 206ltleii 9489 . . . . . . . 8  |-  1  <_  _e
208200, 207jctir 538 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( _e  e.  RR  /\  1  <_  _e ) )
20937adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  R  e.  RR )
21016a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
211 1rp 10987 . . . . . . . . . . . . . 14  |-  1  e.  RR+
212 rphalfcl 11007 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
213211, 212ax-mp 5 . . . . . . . . . . . . 13  |-  ( 1  /  2 )  e.  RR+
214 rpge0 10995 . . . . . . . . . . . . 13  |-  ( ( 1  /  2 )  e.  RR+  ->  0  <_ 
( 1  /  2
) )
215213, 214mp1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( 1  /  2 ) )
21617a1i 11 . . . . . . . . . . . . 13  |-  ( ph  -> 
gamma  e.  RR )
217 0re 9378 . . . . . . . . . . . . . . 15  |-  0  e.  RR
218 emgt0 22369 . . . . . . . . . . . . . . 15  |-  0  <  gamma
219217, 17, 218ltleii 9489 . . . . . . . . . . . . . 14  |-  0  <_ 
gamma
220219a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  gamma )
22120absge0d 12922 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  ( abs `  L ) )
222216, 21, 220, 221addge0d 9907 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( gamma  +  ( abs `  L
) ) )
223210, 23, 215, 222addge0d 9907 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( (
1  /  2 )  +  ( gamma  +  ( abs `  L ) ) ) )
224 log1 22003 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
22529nncnd 10330 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  CC )
226225mulid2d 9396 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  =  m )
22730rpred 11019 . . . . . . . . . . . . . . . . . 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 11447 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... 2 )  ->  m  <_  2 )
231230adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  2 )
2322, 199, 204ltleii 9489 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  _e
233232a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  <_  _e )
234227, 228, 229, 231, 233letrd 9520 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  _e )
235226, 234eqbrtrd 4305 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  <_  _e )
236 1red 9393 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  e.  RR )
237236, 229, 30lemuldivd 11064 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( 1  x.  m
)  <_  _e  <->  1  <_  ( _e  /  m ) ) )
238235, 237mpbid 210 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  <_  ( _e  /  m
) )
239 logleb 22021 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR+  /\  (
_e  /  m )  e.  RR+ )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
240211, 32, 239sylancr 663 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
241238, 240mpbid 210 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  (
_e  /  m )
) )
242224, 241syl5eqbrr 4319 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  (
_e  /  m )
) )
24333, 30, 242divge0d 11055 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  (
_e  /  m )
)  /  m ) )
24426, 34, 243fsumge0 13250 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
24525, 35, 223, 244addge0d 9907 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  + 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m ) ) )
246245, 15syl6breqr 4325 . . . . . . . . 9  |-  ( ph  ->  0  <_  R )
247246adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <_  R )
248209, 247jca 532 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  e.  RR  /\  0  <_  R ) )
24984, 96mulcld 9398 . . . . . . 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 9359 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  (
( log `  (
x  /  n ) )  /  x ) )  e.  RR )
2512, 11, 250sylancr 663 . . . . . . 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 10404 . . . . . . . . 9  |-  0  <_  2
254253a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  2 )
25597mulid2d 9396 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
256 fznnfl 11693 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
257122, 256syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( n  e.  ( 1 ... ( |_ `  x ) )  <-> 
( n  e.  NN  /\  n  <_  x )
) )
258257simplbda 624 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
259255, 258eqbrtrd 4305 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
260 1red 9393 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
26155nnrpd 11018 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
262260, 123, 261lemuldivd 11064 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
263259, 262mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
264 logleb 22021 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
265211, 8, 264sylancr 663 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
266263, 265mpbid 210 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) )
267224, 266syl5eqbrr 4319 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  ( x  /  n ) ) )
268 rpregt0 10996 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <  x ) )
269268ad2antlr 726 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  RR  /\  0  < 
x ) )
270 divge0 10190 . . . . . . . . 9  |-  ( ( ( ( log `  (
x  /  n ) )  e.  RR  /\  0  <_  ( log `  (
x  /  n ) ) )  /\  (
x  e.  RR  /\  0  <  x ) )  ->  0  <_  (
( log `  (
x  /  n ) )  /  x ) )
2719, 267, 269, 270syl21anc 1217 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) )  /  x ) )
272252, 11, 254, 271mulge0d 9908 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( 2  x.  ( ( log `  ( x  /  n ) )  /  x ) ) )
273249abscld 12914 . . . . . . . . 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 465 . . . . . . . 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 465 . . . . . . . . 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 12914 . . . . . . . 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 11019 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
278251, 277remulcld 9406 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
279278adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
28084, 96absmuld 12932 . . . . . . . . . 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 12914 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  e.  RR )
28296abscld 12914 . . . . . . . . . . . 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 12922 . . . . . . . . . . . 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 22455 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  ( abs `  ( mmu `  n ) )  <_ 
1 )
28555, 284syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  <_  1
)
286281, 260, 282, 283, 285lemul1ad 10264 . . . . . . . . . . 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 9404 . . . . . . . . . . . 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 9396 . . . . . . . . . . 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 4309 . . . . . . . . . 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 4305 . . . . . . . . 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 465 . . . . . . . 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 729 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  F  ~~> r  L
)
2948adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( x  /  n )  e.  RR+ )
295 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  _e  <_  ( x  /  n ) )
296292, 293, 294, 295mulog2sumlem1 22752 . . . . . . . . 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 12931 . . . . . . . . . . 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 465 . . . . . . . . . 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 6097 . . . . . . . . . . 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 5687 . . . . . . . . . 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 2485 . . . . . . . . 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 10386 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
30311recnd 9404 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  CC )
304302, 303, 97mulassd 9401 . . . . . . . . . . 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 11000 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
306305ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
307 divdiv2 10035 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  x.  n )  /  x ) )
309 div23 10005 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  ( x  /  n
) )  /  x
)  x.  n ) )
311308, 310eqtrd 2469 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
312311oveq2d 6102 . . . . . . . . . . 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 2472 . . . . . . . . . 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 465 . . . . . . . . 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 4315 . . . . . . . 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 9520 . . . . . . 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 465 . . . . . . . 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 465 . . . . . . . 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 729 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  R  e.  RR )
320290adantr 465 . . . . . . . 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 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  T  e.  CC )
322321abscld 12914 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  T
)  e.  RR )
32395adantr 465 . . . . . . . . . . 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 12914 . . . . . . . . . 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 9405 . . . . . . . . 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 12936 . . . . . . . . 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 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  e.  RR )
32835ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
32961fveq2i 5687 . . . . . . . . . . . 12  |-  ( abs `  T )  =  ( abs `  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
330329, 322syl5eqelr 2522 . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  e.  CC )
332331abscld 12914 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  e.  RR )
33369adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
334333abscld 12914 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) )  e.  RR )
335332, 334readdcld 9405 . . . . . . . . . . . . 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 12934 . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
3399resqcld 12026 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  RR )
340339rehalfcld 10563 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  RR )
3419sqge0d 12027 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) ) ^ 2 ) )
342 2pos 10405 . . . . . . . . . . . . . . . . . . . 20  |-  0  <  2
3432, 342pm3.2i 455 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  e.  RR  /\  0  <  2 )
344343a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
345 divge0 10190 . . . . . . . . . . . . . . . . . 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 1217 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
347340, 346absidd 12901 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
348347adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 ) )
3498rpred 11019 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
350 ltle 9455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  /  n
)  e.  RR  /\  _e  e.  RR )  -> 
( ( x  /  n )  <  _e  ->  ( x  /  n
)  <_  _e )
)
351349, 199, 350sylancl 662 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  n )  <  _e  ->  (
x  /  n )  <_  _e ) )
352351imp 429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( x  /  n )  <_  _e )
3538adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <