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

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

Proof of Theorem mulog2sumlem2
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 1re 9082 . . 3  |-  1  e.  RR
21a1i 11 . 2  |-  ( ph  ->  1  e.  RR )
3 2re 10061 . . . 4  |-  2  e.  RR
4 fzfid 11304 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
5 simpr 448 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR+ )
6 elfznn 11072 . . . . . . . . 9  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76nnrpd 10639 . . . . . . . 8  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
8 rpdivcl 10626 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
95, 7, 8syl2an 464 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
109relogcld 20510 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
11 simplr 732 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
1210, 11rerpdivcld 10667 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  RR )
134, 12fsumrecl 12520 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )
14 remulcl 9067 . . . 4  |-  ( ( 2  e.  RR  /\  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) )  e.  RR )
153, 13, 14sylancr 645 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  RR )
16 mulog2sumlem2.r . . . . . 6  |-  R  =  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
17 2ne0 10075 . . . . . . . . 9  |-  2  =/=  0
183, 17rereccli 9771 . . . . . . . 8  |-  ( 1  /  2 )  e.  RR
19 emre 20836 . . . . . . . . 9  |-  gamma  e.  RR
20 mulog2sumlem.1 . . . . . . . . . . 11  |-  ( ph  ->  F  ~~> r  L )
21 rlimcl 12289 . . . . . . . . . . 11  |-  ( F  ~~> r  L  ->  L  e.  CC )
2220, 21syl 16 . . . . . . . . . 10  |-  ( ph  ->  L  e.  CC )
2322abscld 12230 . . . . . . . . 9  |-  ( ph  ->  ( abs `  L
)  e.  RR )
24 readdcl 9065 . . . . . . . . 9  |-  ( (
gamma  e.  RR  /\  ( abs `  L )  e.  RR )  ->  ( gamma  +  ( abs `  L
) )  e.  RR )
2519, 23, 24sylancr 645 . . . . . . . 8  |-  ( ph  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
26 readdcl 9065 . . . . . . . 8  |-  ( ( ( 1  /  2
)  e.  RR  /\  ( gamma  +  ( abs `  L ) )  e.  RR )  ->  (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  e.  RR )
2718, 25, 26sylancr 645 . . . . . . 7  |-  ( ph  ->  ( ( 1  / 
2 )  +  (
gamma  +  ( abs `  L
) ) )  e.  RR )
28 fzfid 11304 . . . . . . . 8  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
29 epr 12799 . . . . . . . . . . 11  |-  _e  e.  RR+
30 elfznn 11072 . . . . . . . . . . . . 13  |-  ( m  e.  ( 1 ... 2 )  ->  m  e.  NN )
3130adantl 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  NN )
3231nnrpd 10639 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
33 rpdivcl 10626 . . . . . . . . . . 11  |-  ( ( _e  e.  RR+  /\  m  e.  RR+ )  ->  (
_e  /  m )  e.  RR+ )
3429, 32, 33sylancr 645 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
_e  /  m )  e.  RR+ )
3534relogcld 20510 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  ( _e  /  m ) )  e.  RR )
3635, 31nndivred 10040 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( log `  (
_e  /  m )
)  /  m )  e.  RR )
3728, 36fsumrecl 12520 . . . . . . 7  |-  ( ph  -> 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
3827, 37readdcld 9107 . . . . . 6  |-  ( ph  ->  ( ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  +  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )  e.  RR )
3916, 38syl5eqel 2519 . . . . 5  |-  ( ph  ->  R  e.  RR )
40 remulcl 9067 . . . . 5  |-  ( ( R  e.  RR  /\  2  e.  RR )  ->  ( R  x.  2 )  e.  RR )
4139, 3, 40sylancl 644 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  RR )
4241adantr 452 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  x.  2 )  e.  RR )
433a1i 11 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  RR )
44 rpssre 10614 . . . . 5  |-  RR+  C_  RR
45 2cn 10062 . . . . . 6  |-  2  e.  CC
4645a1i 11 . . . . 5  |-  ( ph  ->  2  e.  CC )
47 o1const 12405 . . . . 5  |-  ( (
RR+  C_  RR  /\  2  e.  CC )  ->  (
x  e.  RR+  |->  2 )  e.  O ( 1 ) )
4844, 46, 47sylancr 645 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  2 )  e.  O
( 1 ) )
49 logfacrlim2 21002 . . . . 5  |-  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1
50 rlimo1 12402 . . . . 5  |-  ( ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  ~~> r  1  -> 
( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  O ( 1 ) )
5149, 50mp1i 12 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  e.  O ( 1 ) )
5243, 13, 48, 51o1mul2 12410 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) ) )  e.  O ( 1 ) )
5341recnd 9106 . . . 4  |-  ( ph  ->  ( R  x.  2 )  e.  CC )
54 o1const 12405 . . . 4  |-  ( (
RR+  C_  RR  /\  ( R  x.  2 )  e.  CC )  -> 
( x  e.  RR+  |->  ( R  x.  2
) )  e.  O
( 1 ) )
5544, 53, 54sylancr 645 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( R  x.  2
) )  e.  O
( 1 ) )
5615, 42, 52, 55o1add2 12409 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  O ( 1 ) )
5715, 42readdcld 9107 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
586adantl 453 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
59 mucl 20916 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
mmu `  n )  e.  ZZ )
6058, 59syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  ZZ )
6160zred 10367 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  RR )
6261, 58nndivred 10040 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  RR )
6362recnd 9106 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  /  n )  e.  CC )
64 mulog2sumlem2.t . . . . . 6  |-  T  =  ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )
6510recnd 9106 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
6665sqcld 11513 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  CC )
6766halfcld 10204 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  CC )
68 remulcl 9067 . . . . . . . . . 10  |-  ( (
gamma  e.  RR  /\  ( log `  ( x  /  n ) )  e.  RR )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
6919, 10, 68sylancr 645 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  RR )
7069recnd 9106 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( gamma  x.  ( log `  (
x  /  n ) ) )  e.  CC )
7122ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  L  e.  CC )
7270, 71subcld 9403 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
7367, 72addcld 9099 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) )  e.  CC )
7464, 73syl5eqel 2519 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
7563, 74mulcld 9100 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  T )  e.  CC )
764, 75fsumcl 12519 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  e.  CC )
77 relogcl 20465 . . . . 5  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
7877adantl 453 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
7978recnd 9106 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
8076, 79subcld 9403 . 2  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) )  e.  CC )
8180abscld 12230 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8281adantrr 698 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )  e.  RR )
8357adantrr 698 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  RR )
8457recnd 9106 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) )  e.  CC )
8584abscld 12230 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8685adantrr 698 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) )  /  x ) )  +  ( R  x.  2 ) ) )  e.  RR )
8760zcnd 10368 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  CC )
88 fzfid 11304 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
89 elfznn 11072 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
90 nnrp 10613 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN  ->  m  e.  RR+ )
91 rpdivcl 10626 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x  /  n
)  e.  RR+  /\  m  e.  RR+ )  ->  (
( x  /  n
)  /  m )  e.  RR+ )
929, 90, 91syl2an 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  e.  RR+ )
9392relogcld 20510 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  RR )
94 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  NN )
9593, 94nndivred 10040 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  RR )
9695recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  e.  CC )
9789, 96sylan2 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  e.  CC )
9888, 97fsumcl 12519 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
9974, 98subcld 9403 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
10058nncnd 10008 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
10158nnne0d 10036 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
10287, 99, 100, 101div23d 9819 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( ( ( mmu `  n
)  /  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
10363, 74, 98subdid 9481 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  =  ( ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( ( ( mmu `  n )  /  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
104102, 103eqtrd 2467 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( ( ( mmu `  n )  /  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
105104sumeq2dv 12489 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( mmu `  n )  /  n )  x.  T )  -  (
( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
10663, 98mulcld 9100 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
1074, 75, 106fsumsub 12563 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( mmu `  n )  /  n )  x.  T )  -  (
( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
108105, 107eqtrd 2467 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
109108adantrr 698 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
11088, 63, 97fsummulc2 12559 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( ( mmu `  n )  /  n
)  x.  ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )
11187adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( mmu `  n )  e.  CC )
112100, 101jca 519 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
113112adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
114 div23 9689 . . . . . . . . . . . . . . . . 17  |-  ( ( ( mmu `  n
)  e.  CC  /\  ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( ( mmu `  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) )  /  n
)  =  ( ( ( mmu `  n
)  /  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) ) )
115 divass 9688 . . . . . . . . . . . . . . . . 17  |-  ( ( ( mmu `  n
)  e.  CC  /\  ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( ( mmu `  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) )  /  n
)  =  ( ( mmu `  n )  x.  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n ) ) )
116114, 115eqtr3d 2469 . . . . . . . . . . . . . . . 16  |-  ( ( ( mmu `  n
)  e.  CC  /\  ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( ( mmu `  n )  /  n )  x.  ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( ( mmu `  n )  x.  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n ) ) )
117111, 96, 113, 116syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( mmu `  n )  /  n )  x.  ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( ( mmu `  n )  x.  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n ) ) )
11893recnd 9106 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  e.  CC )
11994nnrpd 10639 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  RR+ )
120 rpcnne0 10621 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
121119, 120syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  e.  CC  /\  m  =/=  0 ) )
122 divdiv1 9717 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( log `  (
( x  /  n
)  /  m ) )  e.  CC  /\  ( m  e.  CC  /\  m  =/=  0 )  /\  ( n  e.  CC  /\  n  =/=  0 ) )  -> 
( ( ( log `  ( ( x  /  n )  /  m
) )  /  m
)  /  n )  =  ( ( log `  ( ( x  /  n )  /  m
) )  /  (
m  x.  n ) ) )
123118, 121, 113, 122syl3anc 1184 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n )  =  ( ( log `  (
( x  /  n
)  /  m ) )  /  ( m  x.  n ) ) )
124 rpre 10610 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  RR+  ->  x  e.  RR )
125124adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
126125adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
127126recnd 9106 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
128127adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  x  e.  CC )
129 divdiv1 9717 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  CC  /\  ( n  e.  CC  /\  n  =/=  0 )  /\  ( m  e.  CC  /\  m  =/=  0 ) )  -> 
( ( x  /  n )  /  m
)  =  ( x  /  ( n  x.  m ) ) )
130128, 113, 121, 129syl3anc 1184 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( x  /  n )  /  m )  =  ( x  /  ( n  x.  m ) ) )
131130fveq2d 5724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( log `  (
( x  /  n
)  /  m ) )  =  ( log `  ( x  /  (
n  x.  m ) ) ) )
13294nncnd 10008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  m  e.  CC )
133100adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  n  e.  CC )
134132, 133mulcomd 9101 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( m  x.  n )  =  ( n  x.  m ) )
135131, 134oveq12d 6091 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( log `  ( ( x  /  n )  /  m
) )  /  (
m  x.  n ) )  =  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) )
136123, 135eqtrd 2467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  /  n )  =  ( ( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) )
137136oveq2d 6089 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( mmu `  n )  x.  (
( ( log `  (
( x  /  n
)  /  m ) )  /  m )  /  n ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
138117, 137eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  NN )  ->  ( ( ( mmu `  n )  /  n )  x.  ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( ( mmu `  n )  x.  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) ) )
13989, 138sylan2 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  ( ( log `  ( ( x  /  n )  /  m
) )  /  m
) )  =  ( ( mmu `  n
)  x.  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
140139sumeq2dv 12489 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( ( mmu `  n )  /  n
)  x.  ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
141110, 140eqtrd 2467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
142141sumeq2dv 12489 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
143 oveq2 6081 . . . . . . . . . . . . . 14  |-  ( k  =  ( n  x.  m )  ->  (
x  /  k )  =  ( x  / 
( n  x.  m
) ) )
144143fveq2d 5724 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  ( n  x.  m ) ) ) )
145 id 20 . . . . . . . . . . . . 13  |-  ( k  =  ( n  x.  m )  ->  k  =  ( n  x.  m ) )
146144, 145oveq12d 6091 . . . . . . . . . . . 12  |-  ( k  =  ( n  x.  m )  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  (
n  x.  m ) ) )  /  (
n  x.  m ) ) )
147146oveq2d 6089 . . . . . . . . . . 11  |-  ( k  =  ( n  x.  m )  ->  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  ( ( mmu `  n )  x.  (
( log `  (
x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
1485rpred 10640 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
149 ssrab2 3420 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  k }  C_  NN
150 simprr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  { y  e.  NN  |  y  ||  k } )
151149, 150sseldi 3338 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  NN )
152151, 59syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  ZZ )
153152zred 10367 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( mmu `  n
)  e.  RR )
154 elfznn 11072 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  NN )
155154adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  NN )
156155nnrpd 10639 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } )  ->  k  e.  RR+ )
157 rpdivcl 10626 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR+  /\  k  e.  RR+ )  ->  (
x  /  k )  e.  RR+ )
1585, 156, 157syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( x  /  k
)  e.  RR+ )
159158relogcld 20510 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( log `  (
x  /  k ) )  e.  RR )
160154ad2antrl 709 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  NN )
161159, 160nndivred 10040 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( log `  (
x  /  k ) )  /  k )  e.  RR )
162153, 161remulcld 9108 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( mmu `  n )  x.  (
( log `  (
x  /  k ) )  /  k ) )  e.  RR )
163162recnd 9106 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( ( mmu `  n )  x.  (
( log `  (
x  /  k ) )  /  k ) )  e.  CC )
164147, 148, 163dvdsflsumcom 20965 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  ( x  /  ( n  x.  m ) ) )  /  ( n  x.  m ) ) ) )
165142, 164eqtr4d 2470 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) ) )
166165adantrr 698 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
( mmu `  n
)  x.  ( ( log `  ( x  /  k ) )  /  k ) ) )
167 oveq2 6081 . . . . . . . . . . 11  |-  ( k  =  1  ->  (
x  /  k )  =  ( x  / 
1 ) )
168167fveq2d 5724 . . . . . . . . . 10  |-  ( k  =  1  ->  ( log `  ( x  / 
k ) )  =  ( log `  (
x  /  1 ) ) )
169 id 20 . . . . . . . . . 10  |-  ( k  =  1  ->  k  =  1 )
170168, 169oveq12d 6091 . . . . . . . . 9  |-  ( k  =  1  ->  (
( log `  (
x  /  k ) )  /  k )  =  ( ( log `  ( x  /  1
) )  /  1
) )
171 fzfid 11304 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
1726ssriv 3344 . . . . . . . . . 10  |-  ( 1 ... ( |_ `  x ) )  C_  NN
173172a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) ) 
C_  NN )
174125adantrr 698 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
175 simprr 734 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
176 flge1nn 11218 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  1  <_  x )  -> 
( |_ `  x
)  e.  NN )
177174, 175, 176syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN )
178 nnuz 10513 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
179177, 178syl6eleq 2525 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  ( ZZ>= ` 
1 ) )
180 eluzfz1 11056 . . . . . . . . . 10  |-  ( ( |_ `  x )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( |_ `  x ) ) )
181179, 180syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ( 1 ... ( |_ `  x ) ) )
182154nnrpd 10639 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  RR+ )
1835, 182, 157syl2an 464 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  k )  e.  RR+ )
184183relogcld 20510 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  k
) )  e.  RR )
185172a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  C_  NN )
186185sselda 3340 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  NN )
187184, 186nndivred 10040 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  RR )
188187recnd 9106 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  / 
k ) )  / 
k )  e.  CC )
189188adantlrr 702 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  k
) )  /  k
)  e.  CC )
190170, 171, 173, 181, 189musumsum 20969 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) ) sum_ n  e.  { y  e.  NN  |  y  ||  k }  ( (
mmu `  n )  x.  ( ( log `  (
x  /  k ) )  /  k ) )  =  ( ( log `  ( x  /  1 ) )  /  1 ) )
1915rpcnd 10642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
192191div1d 9774 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  1 )  =  x )
193192fveq2d 5724 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  ( x  /  1
) )  =  ( log `  x ) )
194193oveq1d 6088 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( ( log `  x
)  /  1 ) )
19579div1d 9774 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  / 
1 )  =  ( log `  x ) )
196194, 195eqtrd 2467 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  ( x  / 
1 ) )  / 
1 )  =  ( log `  x ) )
197196adantrr 698 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  (
x  /  1 ) )  /  1 )  =  ( log `  x
) )
198166, 190, 1973eqtrd 2471 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  =  ( log `  x ) )
199198oveq2d 6089 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  /  n
)  x.  T )  -  ( log `  x
) ) )
200109, 199eqtrd 2467 . . . . 5  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) ) )
201200fveq2d 5724 . . . 4  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  /  n
) )  =  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( mmu `  n
)  /  n )  x.  T )  -  ( log `  x ) ) ) )
202 ere 12683 . . . . . . . . 9  |-  _e  e.  RR
203202a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  _e  e.  RR )
204 1lt2 10134 . . . . . . . . . 10  |-  1  <  2
205 egt2lt3 12797 . . . . . . . . . . 11  |-  ( 2  <  _e  /\  _e  <  3 )
206205simpli 445 . . . . . . . . . 10  |-  2  <  _e
2071, 3, 202lttri 9191 . . . . . . . . . 10  |-  ( ( 1  <  2  /\  2  <  _e )  ->  1  <  _e )
208204, 206, 207mp2an 654 . . . . . . . . 9  |-  1  <  _e
2091, 202, 208ltleii 9188 . . . . . . . 8  |-  1  <_  _e
210203, 209jctir 525 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( _e  e.  RR  /\  1  <_  _e ) )
21139adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  R  e.  RR )
21218a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
213 1rp 10608 . . . . . . . . . . . . . 14  |-  1  e.  RR+
214 rphalfcl 10628 . . . . . . . . . . . . . 14  |-  ( 1  e.  RR+  ->  ( 1  /  2 )  e.  RR+ )
215213, 214ax-mp 8 . . . . . . . . . . . . 13  |-  ( 1  /  2 )  e.  RR+
216 rpge0 10616 . . . . . . . . . . . . 13  |-  ( ( 1  /  2 )  e.  RR+  ->  0  <_ 
( 1  /  2
) )
217215, 216mp1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( 1  /  2 ) )
21819a1i 11 . . . . . . . . . . . . 13  |-  ( ph  -> 
gamma  e.  RR )
219 0re 9083 . . . . . . . . . . . . . . 15  |-  0  e.  RR
220 emgt0 20837 . . . . . . . . . . . . . . 15  |-  0  <  gamma
221219, 19, 220ltleii 9188 . . . . . . . . . . . . . 14  |-  0  <_ 
gamma
222221a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  gamma )
22322absge0d 12238 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  ( abs `  L ) )
224218, 23, 222, 223addge0d 9594 . . . . . . . . . . . 12  |-  ( ph  ->  0  <_  ( gamma  +  ( abs `  L
) ) )
225212, 25, 217, 224addge0d 9594 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( (
1  /  2 )  +  ( gamma  +  ( abs `  L ) ) ) )
226 log1 20472 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
22731nncnd 10008 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  CC )
228227mulid2d 9098 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  =  m )
22932rpred 10640 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  e.  RR )
2303a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  e.  RR )
231202a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  _e  e.  RR )
232 elfzle2 11053 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... 2 )  ->  m  <_  2 )
233232adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  2 )
2343, 202, 206ltleii 9188 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  _e
235234a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  2  <_  _e )
236229, 230, 231, 233, 235letrd 9219 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  m  <_  _e )
237228, 236eqbrtrd 4224 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  x.  m )  <_  _e )
2381a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  e.  RR )
239238, 231, 32lemuldivd 10685 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
( 1  x.  m
)  <_  _e  <->  1  <_  ( _e  /  m ) ) )
240237, 239mpbid 202 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  1  <_  ( _e  /  m
) )
241 logleb 20490 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  RR+  /\  (
_e  /  m )  e.  RR+ )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
242213, 34, 241sylancr 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  (
1  <_  ( _e  /  m )  <->  ( log `  1 )  <_  ( log `  ( _e  /  m ) ) ) )
243240, 242mpbid 202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  (
_e  /  m )
) )
244226, 243syl5eqbrr 4238 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  (
_e  /  m )
) )
24535, 32, 244divge0d 10676 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  (
_e  /  m )
)  /  m ) )
24628, 36, 245fsumge0 12566 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  sum_ m  e.  ( 1 ... 2
) ( ( log `  ( _e  /  m
) )  /  m
) )
24727, 37, 225, 246addge0d 9594 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( (
( 1  /  2
)  +  ( gamma  +  ( abs `  L
) ) )  + 
sum_ m  e.  (
1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m ) ) )
248247, 16syl6breqr 4244 . . . . . . . . 9  |-  ( ph  ->  0  <_  R )
249248adantr 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <_  R )
250211, 249jca 519 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R  e.  RR  /\  0  <_  R ) )
25187, 99mulcld 9100 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  CC )
252 remulcl 9067 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( ( log `  (
x  /  n ) )  /  x )  e.  RR )  -> 
( 2  x.  (
( log `  (
x  /  n ) )  /  x ) )  e.  RR )
2533, 12, 252sylancr 645 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  x
) )  e.  RR )
2543a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
255 2pos 10074 . . . . . . . . . 10  |-  0  <  2
256219, 3, 255ltleii 9188 . . . . . . . . 9  |-  0  <_  2
257256a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  2 )
258100mulid2d 9098 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
259 fznnfl 11235 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
260125, 259syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( n  e.  ( 1 ... ( |_ `  x ) )  <-> 
( n  e.  NN  /\  n  <_  x )
) )
261260simplbda 608 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
262258, 261eqbrtrd 4224 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
2631a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
26458nnrpd 10639 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
265263, 126, 264lemuldivd 10685 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
266262, 265mpbid 202 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
267 logleb 20490 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR+  /\  (
x  /  n )  e.  RR+ )  ->  (
1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
268213, 9, 267sylancr 645 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  <_  ( x  /  n )  <->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) ) )
269266, 268mpbid 202 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  1 )  <_  ( log `  ( x  /  n ) ) )
270226, 269syl5eqbrr 4238 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( log `  ( x  /  n ) ) )
271 rpregt0 10617 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <  x ) )
272271ad2antlr 708 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  RR  /\  0  < 
x ) )
273 divge0 9871 . . . . . . . . 9  |-  ( ( ( ( log `  (
x  /  n ) )  e.  RR  /\  0  <_  ( log `  (
x  /  n ) ) )  /\  (
x  e.  RR  /\  0  <  x ) )  ->  0  <_  (
( log `  (
x  /  n ) )  /  x ) )
27410, 270, 272, 273syl21anc 1183 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) )  /  x ) )
275254, 12, 257, 274mulge0d 9595 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( 2  x.  ( ( log `  ( x  /  n ) )  /  x ) ) )
276251abscld 12230 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  e.  RR )
277276adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  e.  RR )
27899adantr 452 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) )  e.  CC )
279278abscld 12230 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  RR )
280264rpred 10640 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
281253, 280remulcld 9108 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
282281adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  e.  RR )
28387, 99absmuld 12248 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  =  ( ( abs `  (
mmu `  n )
)  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) ) ) )
28487abscld 12230 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  e.  RR )
28599abscld 12230 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  RR )
28699absge0d 12238 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
287 mule1 20923 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  ( abs `  ( mmu `  n ) )  <_ 
1 )
28858, 287syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  <_  1
)
289284, 263, 285, 286, 288lemul1ad 9942 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  n ) )  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( 1  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) ) )
290285recnd 9106 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  e.  CC )
291290mulid2d 9098 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  =  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
292289, 291breqtrd 4228 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  n ) )  x.  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
293283, 292eqbrtrd 4224 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
294293adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
295 logdivsum.1 . . . . . . . . . 10  |-  F  =  ( y  e.  RR+  |->  ( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( ( log `  i
)  /  i )  -  ( ( ( log `  y ) ^ 2 )  / 
2 ) ) )
29620ad3antrrr 711 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  F  ~~> r  L
)
2979adantr 452 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( x  /  n )  e.  RR+ )
298 simpr 448 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  _e  <_  ( x  /  n ) )
299295, 296, 297, 298mulog2sumlem1 21220 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) ) )  <_  (
2  x.  ( ( log `  ( x  /  n ) )  /  ( x  /  n ) ) ) )
30074, 98abssubd 12247 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  T ) ) )
301300adantr 452 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  T ) ) )
30264oveq2i 6084 . . . . . . . . . . 11  |-  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m )  -  T )  =  (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
303302fveq2i 5723 . . . . . . . . . 10  |-  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  T ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) ) )
304301, 303syl6eq 2483 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  -  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) ) ) )
30545a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
30612recnd 9106 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  x )  e.  CC )
307305, 306, 100mulassd 9103 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( ( log `  (
x  /  n ) )  /  x )  x.  n ) ) )
308 rpcnne0 10621 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
309308ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
310 divdiv2 9718 . . . . . . . . . . . . . 14  |-  ( ( ( log `  (
x  /  n ) )  e.  CC  /\  ( x  e.  CC  /\  x  =/=  0 )  /\  ( n  e.  CC  /\  n  =/=  0 ) )  -> 
( ( log `  (
x  /  n ) )  /  ( x  /  n ) )  =  ( ( ( log `  ( x  /  n ) )  x.  n )  /  x ) )
31165, 309, 112, 310syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  x.  n )  /  x ) )
312 div23 9689 . . . . . . . . . . . . . 14  |-  ( ( ( log `  (
x  /  n ) )  e.  CC  /\  n  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( ( log `  ( x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
31365, 100, 309, 312syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  x.  n )  /  x )  =  ( ( ( log `  ( x  /  n
) )  /  x
)  x.  n ) )
314311, 313eqtrd 2467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  / 
( x  /  n
) )  =  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) )
315314oveq2d 6089 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  (
x  /  n ) ) )  =  ( 2  x.  ( ( ( log `  (
x  /  n ) )  /  x )  x.  n ) ) )
316307, 315eqtr4d 2470 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( log `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
317316adantr 452 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n )  =  ( 2  x.  (
( log `  (
x  /  n ) )  /  ( x  /  n ) ) ) )
318299, 304, 3173brtr4d 4234 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) ) )  <_  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  x ) )  x.  n ) )
319277, 279, 282, 294, 318letrd 9219 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  _e  <_  (
x  /  n ) )  ->  ( abs `  ( ( mmu `  n )  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( ( 2  x.  ( ( log `  (
x  /  n ) )  /  x ) )  x.  n ) )
320276adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  e.  RR )
321285adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  e.  RR )
32239ad3antrrr 711 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  R  e.  RR )
323293adantr 452 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( mmu `  n
)  x.  ( T  -  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )  <_ 
( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
32474adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  T  e.  CC )
325324abscld 12230 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  T
)  e.  RR )
32698adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m )  e.  CC )
327326abscld 12230 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  ( ( x  /  n )  /  m ) )  /  m ) )  e.  RR )
328325, 327readdcld 9107 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( abs `  T )  +  ( abs `  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  e.  RR )
329324, 326abs2dif2d 12252 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  ( T  -  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) )  <_  (
( abs `  T
)  +  ( abs `  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  (
( x  /  n
)  /  m ) )  /  m ) ) ) )
33027ad3antrrr 711 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( 1  /  2 )  +  ( gamma  +  ( abs `  L ) ) )  e.  RR )
33137ad3antrrr 711 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  sum_ m  e.  ( 1 ... 2 ) ( ( log `  (
_e  /  m )
)  /  m )  e.  RR )
33264fveq2i 5723 . . . . . . . . . . . 12  |-  ( abs `  T )  =  ( abs `  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )
333332, 325syl5eqelr 2520 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
) ) )  e.  RR )
33467adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 )  e.  CC )
335334abscld 12230 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  e.  RR )
33672adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
)  e.  CC )
337336abscld 12230 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) )  e.  RR )
338335, 337readdcld 9107 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  +  ( abs `  ( ( gamma  x.  ( log `  ( x  /  n ) ) )  -  L ) ) )  e.  RR )
339334, 336abstrid 12250 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 )  +  ( ( gamma  x.  ( log `  (
x  /  n ) ) )  -  L
) ) )  <_ 
( ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  +  ( abs `  (
( gamma  x.  ( log `  ( x  /  n
) ) )  -  L ) ) ) )
34018a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( 1  / 
2 )  e.  RR )
34125ad3antrrr 711 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( gamma  +  ( abs `  L ) )  e.  RR )
34210resqcld 11541 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  RR )
343342rehalfcld 10206 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  /  2 )  e.  RR )
34410sqge0d 11542 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( log `  (
x  /  n ) ) ^ 2 ) )
3453, 255pm3.2i 442 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  e.  RR  /\  0  <  2 )
346345a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
347 divge0 9871 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( log `  ( x  /  n
) ) ^ 2 )  e.  RR  /\  0  <_  ( ( log `  ( x  /  n
) ) ^ 2 ) )  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  0  <_  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
348342, 344, 346, 347syl21anc 1183 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
349343, 348absidd 12217 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( ( log `  ( x  /  n
) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )
350349adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( abs `  (
( ( log `  (
x  /  n ) ) ^ 2 )  /  2 ) )  =  ( ( ( log `  ( x  /  n ) ) ^ 2 )  / 
2 ) )
3519rpred 10640 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
352 ltle 9155 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  /  n
)  e.  RR  /\  _e  e.  RR )  -> 
( ( x  /  n )  <  _e  ->  ( x  /  n
)  <_  _e )
)
353351, 202, 352sylancl 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  n )  <  _e  ->  (
x  /  n )  <_  _e ) )
354353imp 419 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  ( x  /  n )  <  _e )  ->  ( x  /  n )  <_  _e )
3559adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  RR+ )