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

Theorem mulog2sumlem2 24099
Description: Lemma for mulog2sum 24101. (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 9640 . 2  |-  ( ph  ->  1  e.  RR )
2 2re 10645 . . . 4  |-  2  e.  RR
3 fzfid 12122 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
4 simpr 459 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR+ )
5 elfznn 11766 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
65nnrpd 11301 . . . . . . . 8  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
7 rpdivcl 11287 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
84, 6, 7syl2an 475 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
98relogcld 23300 . . . . . 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 11330 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  RR )
123, 11fsumrecl 13703 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )
13 remulcl 9606 . . . 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 661 . . 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 10794 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
17 emre 23659 . . . . . . . . 9  |-  gamma  e.  RR
18 mulog2sumlem.1 . . . . . . . . . . 11  |-  ( ph  ->  F  ~~> r  L )
19 rlimcl 13473 . . . . . . . . . . 11  |-  ( F  ~~> r  L  ->  L  e.  CC )
2018, 19syl 17 . . . . . . . . . 10  |-  ( ph  ->  L  e.  CC )
2120abscld 13414 . . . . . . . . 9  |-  ( ph  ->  ( abs `  L
)  e.  RR )
22 readdcl 9604 . . . . . . . . 9  |-  ( (
gamma  e.  RR  /\  ( abs `  L )  e.  RR )  ->  ( gamma  +  ( abs `  L
) )  e.  RR )
2317, 21, 22sylancr 661 . . . . . . . 8  |-  ( ph  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
24 readdcl 9604 . . . . . . . 8  |-  ( ( ( 1  /  2
)  e.  RR  /\  ( gamma  +  ( abs `  L ) )  e.  RR )  ->  (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  e.  RR )
2516, 23, 24sylancr 661 . . . . . . 7  |-  ( ph  ->  ( ( 1  / 
2 )  +  (
gamma  +  ( abs `  L
) ) )  e.  RR )
26 fzfid 12122 . . . . . . . 8  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
27 epr 14148 . . . . . . . . . . 11  |-  _e  e.  RR+
28 elfznn 11766 . . . . . . . . . . . . 13  |-  ( m  e.  ( 1 ... 2 )  ->  m  e.  NN )
2928adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  NN )
3029nnrpd 11301 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
31 rpdivcl 11287 . . . . . . . . . . 11  |-  ( ( _e  e.  RR+  /\  m  e.  RR+ )  ->  (
_e  /  m )  e.  RR+ )
3227, 30, 31sylancr 661 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
_e  /  m )  e.  RR+ )
3332relogcld 23300 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  ( _e  /  m ) )  e.  RR )
3433, 29nndivred 10624 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( log `  (
_e  /  m )
)  /  m )  e.  RR )
3526, 34fsumrecl 13703 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
3625, 35readdcld 9652 . . . . . 6  |-  ( ph  ->  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )  e.  RR )
3715, 36syl5eqel 2494 . . . . 5  |-  ( ph  ->  R  e.  RR )
38 remulcl 9606 . . . . 5  |-  ( ( R  e.  RR  /\  2  e.  RR )  ->  ( R  x.  2 )  e.  RR )
3937, 2, 38sylancl 660 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  RR )
4039adantr 463 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  x.  2 )  e.  RR )
412a1i 11 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  RR )
42 rpssre 11274 . . . . 5  |-  RR+  C_  RR
43 2cnd 10648 . . . . 5  |-  ( ph  ->  2  e.  CC )
44 o1const 13589 . . . . 5  |-  ( (
RR+  C_  RR  /\  2  e.  CC )  ->  (
x  e.  RR+  |->  2 )  e.  O(1) )
4542, 43, 44sylancr 661 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  2 )  e.  O(1) )
46 logfacrlim2 23880 . . . . 5  |-  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1
47 rlimo1 13586 . . . . 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 13594 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) ) )  e.  O(1) )
5039recnd 9651 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  CC )
51 o1const 13589 . . . 4  |-  ( (
RR+  C_  RR  /\  ( R  x.  2 )  e.  CC )  -> 
( x  e.  RR+  |->  ( R  x.  2
) )  e.  O(1) )
5242, 50, 51sylancr 661 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( R  x.  2
) )  e.  O(1) )
5314, 40, 49, 52o1add2 13593 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  O(1) )
5414, 40readdcld 9652 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
555adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
56 mucl 23794 . . . . . . . . 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 11007 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  RR )
5958, 55nndivred 10624 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  RR )
6059recnd 9651 . . . . 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 9651 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
6362sqcld 12350 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  CC )
6463halfcld 10823 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  CC )
65 remulcl 9606 . . . . . . . . . 10  |-  ( (
gamma  e.  RR  /\  ( log `  ( x  /  n ) )  e.  RR )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6617, 9, 65sylancr 661 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6766recnd 9651 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  CC )
6820ad2antrr 724 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  L  e.  CC )
6967, 68subcld 9966 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
7064, 69addcld 9644 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )  e.  CC )
7161, 70syl5eqel 2494 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
7260, 71mulcld 9645 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  T )  e.  CC )
733, 72fsumcl 13702 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  e.  CC )
74 relogcl 23253 . . . . 5  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
7574adantl 464 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
7675recnd 9651 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
7773, 76subcld 9966 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) )  e.  CC )
7877abscld 13414 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
7978adantrr 715 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8054adantrr 715 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
8154recnd 9651 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  CC )
8281abscld 13414 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8382adantrr 715 . . 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 11008 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  CC )
85 fzfid 12122 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
86 elfznn 11766 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
87 nnrp 11273 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN  ->  m  e.  RR+ )
88 rpdivcl 11287 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  /  n
)  e.  RR+  /\  m  e.  RR+ )  ->  (
( x  /  n
)  /  m )  e.  RR+ )
898, 87, 88syl2an 475 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  e.  RR+ )
9089relogcld 23300 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  RR )
91 simpr 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  NN )
9290, 91nndivred 10624 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  RR )
9392recnd 9651 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  CC )
9486, 93sylan2 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  e.  CC )
9585, 94fsumcl 13702 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
9671, 95subcld 9966 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
9755nncnd 10591 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
9855nnne0d 10620 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
9984, 96, 97, 98div23d 10397 . . . . . . . . . 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 10052 . . . . . . . . . 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 2443 . . . . . . . . 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 13672 . . . . . . . 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 9645 . . . . . . . . 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 13752 . . . . . . . 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 2443 . . . . . . 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 715 . . . . . 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 13748 . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( mmu `  n )  e.  CC )
10997, 98jca 530 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
110109adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
111 div23 10266 . . . . . . . . . . . . . . . . 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 10265 . . . . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . 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 9651 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  CC )
11691nnrpd 11301 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  RR+ )
117 rpcnne0 11281 . . . . . . . . . . . . . . . . . . 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 10295 . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . 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 11270 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR+  ->  x  e.  RR )
122121adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
123122adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
124123recnd 9651 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
125124adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  x  e.  CC )
126 divdiv1 10295 . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  =  ( x  /  ( n  x.  m ) ) )
128127fveq2d 5852 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  =  ( log `  ( x  /  (
n  x.  m ) ) ) )
12991nncnd 10591 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  CC )
13097adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  n  e.  CC )
131129, 130mulcomd 9646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  x.  n )  =  ( n  x.  m ) )
132128, 131oveq12d 6295 . . . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . 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 6293 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . 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 13672 . . . . . . . . . . . 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 2443 . . . . . . . . . . 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 13672 . . . . . . . . . 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 6285 . . . . . . . . . . . . . 14  |-  ( k  =  ( n  x.  m )  ->  (
x  /  k )  =  ( x  / 
( n  x.  m
) ) )
141140fveq2d 5852 . . . . . . . . . . . . 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 6295 . . . . . . . . . . . 12  |-  ( k  =  ( n  x.  m )  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) )
144143oveq2d 6293 . . . . . . . . . . 11  |-  ( k  =  ( n  x.  m )  ->  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
1454rpred 11303 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
146 ssrab2 3523 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  k }  C_  NN
147 simprr 758 . . . . . . . . . . . . . . . 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 3439 . . . . . . . . . . . . . . 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 11007 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  RR )
151 elfznn 11766 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  NN )
152151adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  NN )
153152nnrpd 11301 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  RR+ )
154 rpdivcl 11287 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  k  e.  RR+ )  ->  (
x  /  k )  e.  RR+ )
1554, 153, 154syl2an 475 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( x  /  k
)  e.  RR+ )
156155relogcld 23300 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( log `  (
x  /  k ) )  e.  RR )
157151ad2antrl 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  NN )
158156, 157nndivred 10624 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( log `  (
x  /  k ) )  /  k )  e.  RR )
159150, 158remulcld 9653 . . . . . . . . . . . 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 9651 . . . . . . . . . . 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 23843 . . . . . . . . . 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 2446 . . . . . . . . 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 715 . . . . . . . 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 6285 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
x  /  k )  =  ( x  / 
1 ) )
165164fveq2d 5852 . . . . . . . . . 10  |-  ( k  =  1  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  1 ) ) )
166 id 22 . . . . . . . . . 10  |-  ( k  =  1  ->  k  =  1 )
167165, 166oveq12d 6295 . . . . . . . . 9  |-  ( k  =  1  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  1
) )  /  1
) )
168 fzfid 12122 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
1695ssriv 3445 . . . . . . . . . 10  |-  ( 1 ... ( |_ `  x ) )  C_  NN
170169a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) ) 
C_  NN )
171122adantrr 715 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
172 simprr 758 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
173 flge1nn 11991 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  1  <_  x )  -> 
( |_ `  x
)  e.  NN )
174171, 172, 173syl2anc 659 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN )
175 nnuz 11161 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
176174, 175syl6eleq 2500 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  ( ZZ>= ` 
1 ) )
177 eluzfz1 11745 . . . . . . . . . 10  |-  ( ( |_ `  x )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( |_ `  x ) ) )
178176, 177syl 17 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ( 1 ... ( |_ `  x ) ) )
179151nnrpd 11301 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  RR+ )
1804, 179, 154syl2an 475 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  k )  e.  RR+ )
181180relogcld 23300 . . . . . . . . . . . 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 3441 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  NN )
184181, 183nndivred 10624 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  RR )
185184recnd 9651 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  CC )
186185adantlrr 719 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  k
) )  /  k
)  e.  CC )
187167, 168, 170, 178, 186musumsum 23847 . . . . . . . 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 11305 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
189188div1d 10352 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  1 )  =  x )
190189fveq2d 5852 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  ( x  /  1
) )  =  ( log `  x ) )
191190oveq1d 6292 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( ( log `  x
)  /  1 ) )
19276div1d 10352 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  / 
1 )  =  ( log `  x ) )
193191, 192eqtrd 2443 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( log `  x ) )
194193adantrr 715 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  (
x  /  1 ) )  /  1 )  =  ( log `  x
) )
195163, 187, 1943eqtrd 2447 . . . . . . 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 6293 . . . . . 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 2443 . . . . 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 5852 . . . 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 14031 . . . . . . . . 9  |-  _e  e.  RR
200199a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  _e  e.  RR )
201 1re 9624 . . . . . . . . 9  |-  1  e.  RR
202 1lt2 10742 . . . . . . . . . 10  |-  1  <  2
203 egt2lt3 14146 . . . . . . . . . . 11  |-  ( 2  <  _e  /\  _e  <  3 )
204203simpli 456 . . . . . . . . . 10  |-  2  <  _e
205201, 2, 199lttri 9741 . . . . . . . . . 10  |-  ( ( 1  <  2  /\  2  <  _e )  ->  1  <  _e )
206202, 204, 205mp2an 670 . . . . . . . . 9  |-  1  <  _e
207201, 199, 206ltleii 9738 . . . . . . . 8  |-  1  <_  _e
208200, 207jctir 536 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( _e  e.  RR  /\  1  <_  _e ) )
20937adantr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  R  e.  RR )
21016a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
211 1rp 11268 . . . . . . . . . . . . . 14  |-  1  e.  RR+
212 rphalfcl 11289 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
213211, 212ax-mp 5 . . . . . . . . . . . . 13  |-  ( 1  /  2 )  e.  RR+
214 rpge0 11276 . . . . . . . . . . . . 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 9625 . . . . . . . . . . . . . . 15  |-  0  e.  RR
218 emgt0 23660 . . . . . . . . . . . . . . 15  |-  0  <  gamma
219217, 17, 218ltleii 9738 . . . . . . . . . . . . . 14  |-  0  <_ 
gamma
220219a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  gamma )
22120absge0d 13422 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  ( abs `  L ) )
222216, 21, 220, 221addge0d 10167 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( gamma  +  ( abs `  L
) ) )
223210, 23, 215, 222addge0d 10167 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( (
1  /  2 )  +  ( gamma  +  ( abs `  L ) ) ) )
224 log1 23263 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
22529nncnd 10591 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  CC )
226225mulid2d 9643 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  =  m )
22730rpred 11303 . . . . . . . . . . . . . . . . . 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 11742 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... 2 )  ->  m  <_  2 )
231230adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  2 )
2322, 199, 204ltleii 9738 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  _e
233232a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  <_  _e )
234227, 228, 229, 231, 233letrd 9772 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  _e )
235226, 234eqbrtrd 4414 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  <_  _e )
236 1red 9640 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  e.  RR )
237236, 229, 30lemuldivd 11348 . . . . . . . . . . . . . . . 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 23280 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR+  /\  (
_e  /  m )  e.  RR+ )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
240211, 32, 239sylancr 661 . . . . . . . . . . . . . . 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 4428 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  (
_e  /  m )
) )
24333, 30, 242divge0d 11339 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  (
_e  /  m )
)  /  m ) )
24426, 34, 243fsumge0 13758 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
24525, 35, 223, 244addge0d 10167 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  + 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m ) ) )
246245, 15syl6breqr 4434 . . . . . . . . 9  |-  ( ph  ->  0  <_  R )
247246adantr 463 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <_  R )
248209, 247jca 530 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  e.  RR  /\  0  <_  R ) )
24984, 96mulcld 9645 . . . . . . 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 9606 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  (
( log `  (
x  /  n ) )  /  x ) )  e.  RR )
2512, 11, 250sylancr 661 . . . . . . 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 10666 . . . . . . . . 9  |-  0  <_  2
254253a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  2 )
25597mulid2d 9643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
256 fznnfl 12025 . . . . . . . . . . . . . . 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 622 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
259255, 258eqbrtrd 4414 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
260 1red 9640 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
26155nnrpd 11301 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
262260, 123, 261lemuldivd 11348 . . . . . . . . . . . 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 23280 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
265211, 8, 264sylancr 661 . . . . . . . . . . 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 4428 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  ( x  /  n ) ) )
268 rpregt0 11277 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <  x ) )
269268ad2antlr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  RR  /\  0  < 
x ) )
270 divge0 10451 . . . . . . . . 9  |-  ( ( ( ( log `  (
x  /  n ) )  e.  RR  /\  0  <_  ( log `  (
x  /  n ) ) )  /\  (
x  e.  RR  /\  0  <  x ) )  ->  0  <_  (
( log `  (
x  /  n ) )  /  x ) )
2719, 267, 269, 270syl21anc 1229 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) )  /  x ) )
272252, 11, 254, 271mulge0d 10168 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( 2  x.  ( ( log `  ( x  /  n ) )  /  x ) ) )
273249abscld 13414 . . . . . . . . 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 463 . . . . . . . 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 463 . . . . . . . . 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 13414 . . . . . . . 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 11303 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
278251, 277remulcld 9653 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
279278adantr 463 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
28084, 96absmuld 13432 . . . . . . . . . 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 13414 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  e.  RR )
28296abscld 13414 . . . . . . . . . . . 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 13422 . . . . . . . . . . . 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 23801 . . . . . . . . . . . . 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 10524 . . . . . . . . . . 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 9651 . . . . . . . . . . . 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 9643 . . . . . . . . . . 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 4418 . . . . . . . . . 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 4414 . . . . . . . . 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 463 . . . . . . . 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 728 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  F  ~~> r  L
)
2948adantr 463 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( x  /  n )  e.  RR+ )
295 simpr 459 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  _e  <_  ( x  /  n ) )
296292, 293, 294, 295mulog2sumlem1 24098 . . . . . . . . 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 13431 . . . . . . . . . . 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 463 . . . . . . . . . 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 6288 . . . . . . . . . . 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 5851 . . . . . . . . . 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 2459 . . . . . . . . 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 10648 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
30311recnd 9651 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  CC )
304302, 303, 97mulassd 9648 . . . . . . . . . . 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 11281 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
306305ad2antlr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
307 divdiv2 10296 . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  x.  n )  /  x ) )
309 div23 10266 . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  ( x  /  n
) )  /  x
)  x.  n ) )
311308, 310eqtrd 2443 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
312311oveq2d 6293 . . . . . . . . . . 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 2446 . . . . . . . . . 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 463 . . . . . . . . 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 4424 . . . . . . . 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 9772 . . . . . . 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 463 . . . . . . . 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 463 . . . . . . . 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 728 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  R  e.  RR )
320290adantr 463 . . . . . . . 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 463 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  T  e.  CC )
322321abscld 13414 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  T
)  e.  RR )
32395adantr 463 . . . . . . . . . . 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 13414 . . . . . . . . . 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 9652 . . . . . . . . 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 13436 . . . . . . . . 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 728 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  e.  RR )
32835ad3antrrr 728 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
32961fveq2i 5851 . . . . . . . . . . . 12  |-  ( abs `  T )  =  ( abs `  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
330329, 322syl5eqelr 2495 . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  e.  CC )
332331abscld 13414 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  e.  RR )
33369adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
334333abscld 13414 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) )  e.  RR )
335332, 334readdcld 9652 . . . . . . . . . . . . 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 13434 . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
3399resqcld 12378 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  RR )
340339rehalfcld 10825 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  RR )
3419sqge0d 12379 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) ) ^ 2 ) )
342 2pos 10667 . . . . . . . . . . . . . . . . . . . 20  |-  0  <  2
3432, 342pm3.2i 453 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  e.  RR  /\  0  <  2 )
344343a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
345 divge0 10451 . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
347340, 346absidd 13401 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
348347adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 ) )
3498rpred 11303 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
350 ltle 9703 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  /  n
)  e.  RR  /\  _e  e.  RR )  -> 
( ( x  /  n )  <  _e  ->  ( x  /  n
)  <_  _e )
)
351349, 199, 350sylancl 660 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  n )  <  _e  ->  (
x  /  n )  <_  _e ) )
352351imp 427 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( x  /  n )  <_  _e )
3538adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )