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

Theorem selberglem2 24326
Description: Lemma for selberg 24328. (Contributed by Mario Carneiro, 23-May-2016.)
Hypothesis
Ref Expression
selberglem1.t  |-  T  =  ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) )  /  n )
Assertion
Ref Expression
selberglem2  |-  ( x  e.  RR+  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( mmu `  n )  x.  ( ( log `  m ) ^ 2 ) )  /  x
)  -  ( 2  x.  ( log `  x
) ) ) )  e.  O(1)
Distinct variable group:    m, n, x
Allowed substitution hints:    T( x, m, n)

Proof of Theorem selberglem2
StepHypRef Expression
1 reex 9581 . . . . . . 7  |-  RR  e.  _V
2 rpssre 11263 . . . . . . 7  |-  RR+  C_  RR
31, 2ssexi 4512 . . . . . 6  |-  RR+  e.  _V
43a1i 11 . . . . 5  |-  ( T. 
->  RR+  e.  _V )
5 fzfid 12136 . . . . . 6  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
6 elfznn 11779 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76adantl 467 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
8 mucl 24010 . . . . . . . . . 10  |-  ( n  e.  NN  ->  (
mmu `  n )  e.  ZZ )
97, 8syl 17 . . . . . . . . 9  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  ZZ )
109zred 10991 . . . . . . . 8  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  RR )
1110recnd 9620 . . . . . . 7  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  n )  e.  CC )
12 fzfid 12136 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
13 elfznn 11779 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
1413adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  NN )
1514nnrpd 11290 . . . . . . . . . . . . 13  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  RR+ )
1615relogcld 23514 . . . . . . . . . . . 12  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( log `  m )  e.  RR )
1716resqcld 12392 . . . . . . . . . . 11  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  m ) ^
2 )  e.  RR )
1812, 17fsumrecl 13743 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  e.  RR )
19 simplr 760 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
2018, 19rerpdivcld 11320 . . . . . . . . 9  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  e.  RR )
2120recnd 9620 . . . . . . . 8  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  e.  CC )
22 selberglem1.t . . . . . . . . . 10  |-  T  =  ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) )  /  n )
23 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  RR+ )  ->  x  e.  RR+ )
246nnrpd 11290 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
25 rpdivcl 11276 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
2623, 24, 25syl2an 479 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
2726relogcld 23514 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
2827resqcld 12392 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  RR )
29 2re 10630 . . . . . . . . . . . . 13  |-  2  e.  RR
30 remulcl 9575 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  RR  /\  ( log `  ( x  /  n ) )  e.  RR )  -> 
( 2  x.  ( log `  ( x  /  n ) ) )  e.  RR )
3129, 27, 30sylancr 667 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( log `  (
x  /  n ) ) )  e.  RR )
32 resubcl 9889 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  ( 2  x.  ( log `  ( x  /  n ) ) )  e.  RR )  -> 
( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) )  e.  RR )
3329, 31, 32sylancr 667 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) )  e.  RR )
3428, 33readdcld 9621 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) )  e.  RR )
3534, 7nndivred 10609 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) )  /  n
)  e.  RR )
3622, 35syl5eqel 2510 . . . . . . . . 9  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  RR )
3736recnd 9620 . . . . . . . 8  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
3821, 37subcld 9937 . . . . . . 7  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T )  e.  CC )
3911, 38mulcld 9614 . . . . . 6  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  e.  CC )
405, 39fsumcl 13742 . . . . 5  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  e.  CC )
4111, 37mulcld 9614 . . . . . . 7  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  T )  e.  CC )
425, 41fsumcl 13742 . . . . . 6  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n )  x.  T
)  e.  CC )
43 2cn 10631 . . . . . . 7  |-  2  e.  CC
44 relogcl 23467 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
4544adantl 467 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
4645recnd 9620 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
47 mulcl 9574 . . . . . . 7  |-  ( ( 2  e.  CC  /\  ( log `  x )  e.  CC )  -> 
( 2  x.  ( log `  x ) )  e.  CC )
4843, 46, 47sylancr 667 . . . . . 6  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( 2  x.  ( log `  x
) )  e.  CC )
4942, 48subcld 9937 . . . . 5  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) )  e.  CC )
50 eqidd 2429 . . . . 5  |-  ( T. 
->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  =  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) ) )
51 eqidd 2429 . . . . 5  |-  ( T. 
->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  T
)  -  ( 2  x.  ( log `  x
) ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n )  x.  T
)  -  ( 2  x.  ( log `  x
) ) ) ) )
524, 40, 49, 50, 51offval2 6506 . . . 4  |-  ( T. 
->  ( ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  oF  +  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  T
)  -  ( 2  x.  ( log `  x
) ) ) ) ) )
5340, 42, 48addsubassd 9957 . . . . . 6  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  + 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  T ) )  -  ( 2  x.  ( log `  x
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  T
)  -  ( 2  x.  ( log `  x
) ) ) ) )
54 rpcnne0 11270 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
5554adantl 467 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
5655simpld 460 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  RR+ )  ->  x  e.  CC )
5710adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( mmu `  n )  e.  RR )
5857, 17remulcld 9622 . . . . . . . . . . 11  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
mmu `  n )  x.  ( ( log `  m
) ^ 2 ) )  e.  RR )
5912, 58fsumrecl 13743 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  e.  RR )
6059recnd 9620 . . . . . . . . 9  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  e.  CC )
6155simprd 464 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  RR+ )  ->  x  =/=  0 )
625, 56, 60, 61fsumdivc 13790 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  /  x )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  /  x ) )
6317recnd 9620 . . . . . . . . . . . 12  |-  ( ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  m ) ^
2 )  e.  CC )
6412, 63fsumcl 13742 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  e.  CC )
6555adantr 466 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
66 divass 10239 . . . . . . . . . . 11  |-  ( ( ( mmu `  n
)  e.  CC  /\  sum_
m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( ( mmu `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 ) )  /  x )  =  ( ( mmu `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x ) ) )
6711, 64, 65, 66syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 ) )  /  x )  =  ( ( mmu `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x ) ) )
6812, 11, 63fsummulc2 13788 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) ) )
6968oveq1d 6264 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( mmu `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 ) )  /  x )  =  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  /  x ) )
7021, 37npcand 9941 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T )  +  T
)  =  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x ) )
7170oveq2d 6265 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  ( ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
)  +  T ) )  =  ( ( mmu `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x ) ) )
7211, 38, 37adddid 9618 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  ( ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
)  +  T ) )  =  ( ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( ( mmu `  n )  x.  T
) ) )
7371, 72eqtr3d 2464 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x ) )  =  ( ( ( mmu `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) )  +  ( ( mmu `  n
)  x.  T ) ) )
7467, 69, 733eqtr3d 2470 . . . . . . . . 9  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( mmu `  n )  x.  ( ( log `  m ) ^ 2 ) )  /  x
)  =  ( ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( ( mmu `  n )  x.  T
) ) )
7574sumeq2dv 13712 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  /  x )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( ( mmu `  n )  x.  T
) ) )
765, 39, 41fsumadd 13748 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( ( mmu `  n )  x.  T
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  + 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  T ) ) )
7762, 75, 763eqtrrd 2467 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  m ) ^ 2 ) )  /  x ) )
7877oveq1d 6264 . . . . . 6  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  + 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  T ) )  -  ( 2  x.  ( log `  x
) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  m ) ^ 2 ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )
7953, 78eqtr3d 2464 . . . . 5  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) )  +  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  T )  -  ( 2  x.  ( log `  x
) ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( mmu `  n )  x.  (
( log `  m
) ^ 2 ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) )
8079mpteq2dva 4453 . . . 4  |-  ( T. 
->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  +  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  T
)  -  ( 2  x.  ( log `  x
) ) ) ) )  =  ( x  e.  RR+  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( mmu `  n )  x.  ( ( log `  m ) ^ 2 ) )  /  x
)  -  ( 2  x.  ( log `  x
) ) ) ) )
8152, 80eqtrd 2462 . . 3  |-  ( T. 
->  ( ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  oF  +  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) ) ) )  =  ( x  e.  RR+  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  m ) ^ 2 ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) ) )
82 1red 9609 . . . . 5  |-  ( T. 
->  1  e.  RR )
835, 28fsumrecl 13743 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  e.  RR )
8483, 23rerpdivcld 11320 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x )  e.  RR )
8584recnd 9620 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x )  e.  CC )
86 2cnd 10633 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  2  e.  CC )
87 2nn0 10837 . . . . . . . 8  |-  2  e.  NN0
88 logexprlim 24095 . . . . . . . 8  |-  ( 2  e.  NN0  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x ) )  ~~> r  ( ! `  2 ) )
8987, 88mp1i 13 . . . . . . 7  |-  ( T. 
->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x ) )  ~~> r  ( ! ` 
2 ) )
90 2cnd 10633 . . . . . . . 8  |-  ( T. 
->  2  e.  CC )
91 rlimconst 13551 . . . . . . . 8  |-  ( (
RR+  C_  RR  /\  2  e.  CC )  ->  (
x  e.  RR+  |->  2 )  ~~> r  2 )
922, 90, 91sylancr 667 . . . . . . 7  |-  ( T. 
->  ( x  e.  RR+  |->  2 )  ~~> r  2 )
9385, 86, 89, 92rlimadd 13649 . . . . . 6  |-  ( T. 
->  ( x  e.  RR+  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )  ~~> r  ( ( ! `  2
)  +  2 ) )
94 rlimo1 13623 . . . . . 6  |-  ( ( x  e.  RR+  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )  ~~> r  ( ( ! `  2
)  +  2 )  ->  ( x  e.  RR+  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x )  +  2 ) )  e.  O(1) )
9593, 94syl 17 . . . . 5  |-  ( T. 
->  ( x  e.  RR+  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )  e.  O(1) )
96 readdcl 9573 . . . . . 6  |-  ( ( ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  e.  RR  /\  2  e.  RR )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 )  e.  RR )
9784, 29, 96sylancl 666 . . . . 5  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 )  e.  RR )
9840abscld 13441 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( abs `  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  e.  RR )
9997recnd 9620 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 )  e.  CC )
10099abscld 13441 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( abs `  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )  e.  RR )
10139abscld 13441 . . . . . . . . 9  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  e.  RR )
1025, 101fsumrecl 13743 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  (
( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  e.  RR )
1035, 39fsumabs 13804 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( abs `  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  (
( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) ) )
104 readdcl 9573 . . . . . . . . . . . 12  |-  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  e.  RR  /\  2  e.  RR )  ->  (
( ( log `  (
x  /  n ) ) ^ 2 )  +  2 )  e.  RR )
10528, 29, 104sylancl 666 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  +  2 )  e.  RR )
106105, 19rerpdivcld 11320 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( ( log `  (
x  /  n ) ) ^ 2 )  +  2 )  /  x )  e.  RR )
1075, 106fsumrecl 13743 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 )  /  x
)  e.  RR )
10838abscld 13441 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  e.  RR )
10911, 38absmuld 13459 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  =  ( ( abs `  ( mmu `  n
) )  x.  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) ) ) )
11011abscld 13441 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  e.  RR )
111 1red 9609 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
11238absge0d 13449 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )
113 mule1 24017 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  ( abs `  ( mmu `  n ) )  <_ 
1 )
1147, 113syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( mmu `  n
) )  <_  1
)
115110, 111, 108, 112, 114lemul1ad 10497 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  n ) )  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( 1  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) ) )
116108recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  e.  CC )
117116mulid2d 9612 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  =  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )
118115, 117breqtrd 4391 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  n ) )  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )
119109, 118eqbrtrd 4387 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )
12065simpld 460 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
121120, 38absmuld 13459 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  =  ( ( abs `  x )  x.  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) ) ) )
122120, 21, 37subdid 10025 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  =  ( ( x  x.  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x ) )  -  ( x  x.  T ) ) )
12365simprd 464 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
12464, 120, 123divcan2d 10336 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 ) )
12534recnd 9620 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) )  e.  CC )
1267nnrpd 11290 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
127 rpcnne0 11270 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  ( n  e.  CC  /\  n  =/=  0 ) )
128126, 127syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
129 divass 10239 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  CC  /\  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( x  x.  ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) ) )  /  n
)  =  ( x  x.  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) )  /  n
) ) )
13022oveq2i 6260 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  x.  T )  =  ( x  x.  (
( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) )  /  n ) )
131129, 130syl6eqr 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  CC  /\  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( x  x.  ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) ) )  /  n
)  =  ( x  x.  T ) )
132 div23 10240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  CC  /\  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( x  x.  ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) ) )  /  n
)  =  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( 2  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) ) ) )
133131, 132eqtr3d 2464 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  CC  /\  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( x  x.  T )  =  ( ( x  /  n
)  x.  ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) ) ) )
134120, 125, 128, 133syl3anc 1264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  T )  =  ( ( x  /  n
)  x.  ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) ) ) )
135124, 134oveq12d 6267 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x ) )  -  ( x  x.  T
) )  =  (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  -  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) ) ) ) )
136122, 135eqtrd 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  =  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  -  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) ) ) ) )
137136fveq2d 5829 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  =  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  -  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) ) ) ) ) )
138 rprege0 11267 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR+  ->  ( x  e.  RR  /\  0  <_  x ) )
139 absid 13303 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( abs `  x
)  =  x )
14019, 138, 1393syl 18 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  x )  =  x )
141140oveq1d 6264 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  x )  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  =  ( x  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) ) )
142121, 137, 1413eqtr3d 2470 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  -  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) ) ) ) )  =  ( x  x.  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) ) ) )
1437nncnd 10576 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
144143mulid2d 9612 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
145 rpre 11259 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR+  ->  x  e.  RR )
146145adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  RR+ )  ->  x  e.  RR )
147 fznnfl 12039 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
148146, 147syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( n  e.  ( 1 ... ( |_ `  x
) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
149148simplbda 628 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
150144, 149eqbrtrd 4387 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
15119rpred 11292 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
152111, 151, 126lemuldivd 11338 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
153150, 152mpbid 213 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
154 log2sumbnd 24324 . . . . . . . . . . . . . 14  |-  ( ( ( x  /  n
)  e.  RR+  /\  1  <_  ( x  /  n
) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  -  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) ) ) ) )  <_ 
( ( ( log `  ( x  /  n
) ) ^ 2 )  +  2 ) )
15526, 153, 154syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  -  ( ( x  /  n )  x.  ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  ( 2  -  ( 2  x.  ( log `  (
x  /  n ) ) ) ) ) ) ) )  <_ 
( ( ( log `  ( x  /  n
) ) ^ 2 )  +  2 ) )
156142, 155eqbrtrrd 4389 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 ) )
157108, 105, 19lemuldiv2d 11339 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  x.  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 )  <->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  <_ 
( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 )  /  x
) ) )
158156, 157mpbid 213 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) )  <_ 
( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 )  /  x
) )
159101, 108, 106, 119, 158letrd 9743 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  2 )  /  x ) )
1605, 101, 106, 159fsumle 13802 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  (
( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 )  /  x
) )
1615, 105fsumrecl 13743 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  2 )  e.  RR )
162 remulcl 9575 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  2  e.  RR )  ->  ( x  x.  2 )  e.  RR )
163146, 29, 162sylancl 666 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( x  x.  2 )  e.  RR )
16483, 163readdcld 9621 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) )  e.  RR )
16528recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) ) ^
2 )  e.  CC )
166 2cnd 10633 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
1675, 165, 166fsumadd 13748 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  2 )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) 2 ) )
168 fsumconst 13794 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  2  e.  CC )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) 2  =  ( (
# `  ( 1 ... ( |_ `  x
) ) )  x.  2 ) )
1695, 43, 168sylancl 666 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) 2  =  ( (
# `  ( 1 ... ( |_ `  x
) ) )  x.  2 ) )
170138adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( x  e.  RR  /\  0  <_  x ) )
171 flge0nn0 12004 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
172 hashfz1 12479 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  x )  e.  NN0  ->  ( # `  ( 1 ... ( |_ `  x ) ) )  =  ( |_
`  x ) )
173170, 171, 1723syl 18 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( # `  ( 1 ... ( |_ `  x ) ) )  =  ( |_
`  x ) )
174173oveq1d 6264 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
# `  ( 1 ... ( |_ `  x
) ) )  x.  2 )  =  ( ( |_ `  x
)  x.  2 ) )
175169, 174eqtrd 2462 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) 2  =  ( ( |_ `  x )  x.  2 ) )
176175oveq2d 6265 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  + 
sum_ n  e.  (
1 ... ( |_ `  x ) ) 2 )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( ( |_ `  x )  x.  2 ) ) )
177167, 176eqtrd 2462 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  2 )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( ( |_
`  x )  x.  2 ) ) )
178 reflcl 11982 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  ( |_ `  x )  e.  RR )
179146, 178syl 17 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( |_
`  x )  e.  RR )
18029a1i 11 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  RR+ )  ->  2  e.  RR )
181179, 180remulcld 9622 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( ( |_ `  x )  x.  2 )  e.  RR )
182 flle 11985 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  ( |_ `  x )  <_  x )
183146, 182syl 17 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( |_
`  x )  <_  x )
184 2pos 10652 . . . . . . . . . . . . . . . . 17  |-  0  <  2
18529, 184pm3.2i 456 . . . . . . . . . . . . . . . 16  |-  ( 2  e.  RR  /\  0  <  2 )
186185a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( 2  e.  RR  /\  0  <  2 ) )
187 lemul1 10408 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  x
)  e.  RR  /\  x  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( |_
`  x )  <_  x 
<->  ( ( |_ `  x )  x.  2 )  <_  ( x  x.  2 ) ) )
188179, 146, 186, 187syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( ( |_ `  x )  <_  x  <->  ( ( |_ `  x )  x.  2 )  <_  (
x  x.  2 ) ) )
189183, 188mpbid 213 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( ( |_ `  x )  x.  2 )  <_ 
( x  x.  2 ) )
190181, 163, 83, 189leadd2dd 10179 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( ( |_ `  x )  x.  2 ) )  <_  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) ) )
191177, 190eqbrtrd 4387 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( log `  ( x  /  n
) ) ^ 2 )  +  2 )  <_  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) ) )
192161, 164, 23, 191lediv1dd 11347 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  2 )  /  x )  <_  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) )  /  x ) )
193105recnd 9620 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) ) ^ 2 )  +  2 )  e.  CC )
1945, 56, 193, 61fsumdivc 13790 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  2 )  /  x )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( ( log `  (
x  /  n ) ) ^ 2 )  +  2 )  /  x ) )
19583recnd 9620 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  e.  CC )
19656, 86mulcld 9614 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( x  x.  2 )  e.  CC )
197 divdir 10244 . . . . . . . . . . . 12  |-  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  e.  CC  /\  (
x  x.  2 )  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) )  /  x
)  =  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  ( ( x  x.  2 )  /  x
) ) )
198195, 196, 55, 197syl3anc 1264 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) )  /  x )  =  ( ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  ( ( x  x.  2 )  /  x
) ) )
19986, 56, 61divcan3d 10339 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( ( x  x.  2 )  /  x )  =  2 )
200199oveq2d 6265 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  ( ( x  x.  2 )  /  x
) )  =  ( ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )
201198, 200eqtrd 2462 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  +  ( x  x.  2 ) )  /  x )  =  ( ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )
202192, 194, 2013brtr3d 4396 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( log `  ( x  /  n ) ) ^ 2 )  +  2 )  /  x
)  <_  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) )
203102, 107, 97, 160, 202letrd 9743 . . . . . . . 8  |-  ( ( T.  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  (
( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x )  +  2 ) )
20498, 102, 97, 103, 203letrd 9743 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( abs `  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x )  +  2 ) )
20597leabsd 13420 . . . . . . 7  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 )  <_  ( abs `  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( log `  ( x  /  n ) ) ^ 2 )  /  x )  +  2 ) ) )
20698, 97, 100, 204, 205letrd 9743 . . . . . 6  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( abs `  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  <_  ( abs `  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) ) )
207206adantrr 721 . . . . 5  |-  ( ( T.  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( log `  m ) ^ 2 )  /  x )  -  T
) ) )  <_ 
( abs `  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  (
x  /  n ) ) ^ 2 )  /  x )  +  2 ) ) )
20882, 95, 97, 40, 207o1le 13659 . . . 4  |-  ( T. 
->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  e.  O(1) )
20922selberglem1 24325 . . . 4  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O(1)
210 o1add 13620 . . . 4  |-  ( ( ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  e.  O(1)  /\  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O(1) )  ->  ( ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  oF  +  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) ) ) )  e.  O(1) )
211208, 209, 210sylancl 666 . . 3  |-  ( T. 
->  ( ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( mmu `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( log `  m
) ^ 2 )  /  x )  -  T ) ) )  oF  +  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( mmu `  n )  x.  T )  -  ( 2  x.  ( log `  x ) ) ) ) )  e.  O(1) )
21281, 211eqeltrrd 2507 . 2  |-  ( T. 
->  ( x  e.  RR+  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( mmu `  n
)  x.  ( ( log `  m ) ^ 2 ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O(1) )
213212trud 1446 1  |-  ( x  e.  RR+  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( ( mmu `  n )  x.  ( ( log `  m ) ^ 2 ) )  /  x
)  -  ( 2  x.  ( log `  x
) ) ) )  e.  O(1)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   T. wtru 1438    e. wcel 1872    =/= wne 2599   _Vcvv 3022    C_ wss 3379   class class class wbr 4366    |-> cmpt 4425   ` cfv 5544  (class class class)co 6249    oFcof 6487   Fincfn 7524   CCcc 9488   RRcr 9489   0cc0 9490   1c1 9491    + caddc 9493    x. cmul 9495    < clt 9626    <_ cle 9627    - cmin 9811    / cdiv 10220   NNcn 10560   2c2 10610   NN0cn0 10820   ZZcz 10888   RR+crp 11253   ...cfz 11735   |_cfl 11976   ^cexp 12222   !cfa 12409   #chash 12465   abscabs 13241    ~~> r crli 13492   O(1)co1 13493   sum_csu 13695   logclog 23446   mmucmu 23963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-inf2 8099  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568  ax-addf 9569  ax-mulf 9570
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-iin 4245  df-disj 4338  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-se 4756  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-isom 5553  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-of 6489  df-om 6651  df-1st 6751  df-2nd 6752  df-supp 6870  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-2o 7138  df-oadd 7141  df-er 7318  df-map 7429  df-pm 7430  df-ixp 7478  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-fsupp 7837  df-fi 7878  df-sup 7909  df-inf 7910  df-oi 7978  df-card 8325  df-cda 8549  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-div 10221  df-nn 10561  df-2 10619  df-3 10620  df-4 10621  df-5 10622  df-6 10623  df-7 10624  df-8 10625  df-9 10626  df-10 10627  df-n0 10821  df-z 10889  df-dec 11003  df-uz 11111  df-q 11216  df-rp 11254  df-xneg 11360  df-xadd 11361  df-xmul 11362  df-ioo 11590  df-ioc 11591  df-ico 11592  df-icc 11593  df-fz 11736  df-fzo 11867  df-fl 11978  df-mod 12047  df-seq 12164  df-exp 12223  df-fac 12410  df-bc 12438  df-hash 12466  df-shft 13074  df-cj 13106  df-re 13107  df-im 13108  df-sqrt 13242  df-abs 13243  df-limsup 13469  df-clim 13495  df-rlim 13496  df-o1 13497  df-lo1 13498  df-sum 13696  df-ef 14064  df-e 14065  df-sin 14066  df-cos 14067  df-pi 14069  df-dvds 14249  df-gcd 14412  df-prm 14566  df-pc 14730  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-sets 15070  df-ress 15071  df-plusg 15146  df-mulr 15147  df-starv 15148  df-sca 15149  df-vsca 15150  df-ip 15151  df-tset 15152  df-ple 15153  df-ds 15155  df-unif 15156  df-hom 15157  df-cco 15158  df-rest 15264  df-topn 15265  df-0g 15283  df-gsum 15284  df-topgen 15285  df-pt 15286  df-prds 15289  df-xrs 15343  df-qtop 15349  df-imas 15350  df-xps 15353  df-mre 15435  df-mrc 15436  df-acs 15438  df-mgm 16431  df-sgrp 16470  df-mnd 16480  df-submnd 16526  df-mulg 16619  df-cntz 16914  df-cmn 17375  df-psmet 18905  df-xmet 18906  df-met 18907  df-bl 18908  df-mopn 18909  df-fbas 18910  df-fg 18911  df-cnfld 18914  df-top 19863  df-bases 19864  df-topon 19865  df-topsp 19866  df-cld 19976  df-ntr 19977  df-cls 19978  df-nei 20056  df-lp 20094  df-perf 20095  df-cn 20185  df-cnp 20186  df-haus 20273  df-cmp 20344  df-tx 20519  df-hmeo 20712  df-fil 20803  df-fm 20895  df-flim 20896  df-flf 20897  df-xms 21277  df-ms 21278  df-tms 21279  df-cncf 21852  df-limc 22763  df-dv 22764  df-log 23448  df-cxp 23449  df-em 23860  df-mu 23969
This theorem is referenced by:  selberglem3  24327  selberg  24328
  Copyright terms: Public domain W3C validator