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

Theorem vmalogdivsum2 20681
Description: The sum  sum_ n  <_  x , Λ ( n ) log ( x  /  n )  /  n is asymptotic to  log ^ 2 ( x )  / 
2  +  O ( log x ). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
Assertion
Ref Expression
vmalogdivsum2  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  e.  O ( 1 )
Distinct variable group:    x, n
Dummy variables  k  m  y are mutually distinct and distinct from all other variables.

Proof of Theorem vmalogdivsum2
StepHypRef Expression
1 fzfid 11029 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
2 elfznn 10813 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... ( |_ `  x
) )  ->  k  e.  NN )
32adantl 454 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  NN )
43nnrpd 10384 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  RR+ )
54relogcld 19968 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  k )  e.  RR )
65, 3nndivred 9789 . . . . . . . . 9  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  k )  / 
k )  e.  RR )
71, 6fsumrecl 12201 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  e.  RR )
87recnd 8856 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  e.  CC )
9 elioore 10680 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
109adantl 454 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
11 1rp 10353 . . . . . . . . . . . . 13  |-  1  e.  RR+
1211a1i 12 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
1312rpred 10385 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
14 eliooord 10704 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
1514adantl 454 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
1615simpld 447 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
1713, 10, 16ltled 8962 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
1810, 12, 17rpgecld 10420 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
1918relogcld 19968 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
2019resqcld 11265 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
) ^ 2 )  e.  RR )
2120rehalfcld 9953 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
) ^ 2 )  /  2 )  e.  RR )
2221recnd 8856 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
) ^ 2 )  /  2 )  e.  CC )
2319recnd 8856 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
2410, 16rplogcld 19974 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2524rpne0d 10390 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
268, 22, 23, 25divsubdird 9570 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  / 
( log `  x
) )  =  ( ( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( ( ( log `  x ) ^ 2 )  /  2 )  /  ( log `  x
) ) ) )
277, 21resubcld 9206 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  e.  RR )
2827recnd 8856 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  e.  CC )
2928, 23, 25divrecd 9534 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  / 
( log `  x
) )  =  ( ( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  x.  ( 1  /  ( log `  x ) ) ) )
3020recnd 8856 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
) ^ 2 )  e.  CC )
31 2cn 9811 . . . . . . . . . 10  |-  2  e.  CC
3231a1i 12 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
33 2ne0 9824 . . . . . . . . . 10  |-  2  =/=  0
3433a1i 12 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  =/=  0 )
3530, 32, 23, 34, 25divdiv32d 9556 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( log `  x ) ^ 2 )  /  2 )  /  ( log `  x
) )  =  ( ( ( ( log `  x ) ^ 2 )  /  ( log `  x ) )  / 
2 ) )
3623sqvald 11236 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
) ^ 2 )  =  ( ( log `  x )  x.  ( log `  x ) ) )
3736oveq1d 5834 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
) ^ 2 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  x.  ( log `  x ) )  / 
( log `  x
) ) )
3823, 23, 25divcan3d 9536 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  x.  ( log `  x ) )  / 
( log `  x
) )  =  ( log `  x ) )
3937, 38eqtrd 2316 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
) ^ 2 )  /  ( log `  x
) )  =  ( log `  x ) )
4039oveq1d 5834 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( log `  x ) ^ 2 )  /  ( log `  x ) )  / 
2 )  =  ( ( log `  x
)  /  2 ) )
4135, 40eqtrd 2316 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( log `  x ) ^ 2 )  /  2 )  /  ( log `  x
) )  =  ( ( log `  x
)  /  2 ) )
4241oveq2d 5835 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( ( ( log `  x ) ^ 2 )  /  2 )  /  ( log `  x
) ) )  =  ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) ) )
4326, 29, 423eqtr3rd 2325 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) )  =  ( (
sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  x.  ( 1  /  ( log `  x ) ) ) )
4443mpteq2dva 4107 . . . 4  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( (
sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  x.  ( 1  /  ( log `  x ) ) ) ) )
4524rprecred 10396 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
4618ex 425 . . . . . . 7  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  ->  x  e.  RR+ )
)
4746ssrdv 3186 . . . . . 6  |-  (  T. 
->  ( 1 (,)  +oo )  C_  RR+ )
48 eqid 2284 . . . . . . . . 9  |-  ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  =  ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )
4948logdivsum 20676 . . . . . . . 8  |-  ( ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) ) : RR+ --> RR  /\  (
x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  e.  dom  ~~> r  /\  ( ( ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  ~~> r  1  /\  1  e.  RR+  /\  _e  <_  1 )  ->  ( abs `  ( ( ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) ) `
 1 )  - 
1 ) )  <_ 
( ( log `  1
)  /  1 ) ) )
5049simp2i 967 . . . . . . 7  |-  ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  e.  dom  ~~> r
51 rlimdmo1 12085 . . . . . . 7  |-  ( ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  e.  dom  ~~> r  -> 
( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  e.  O ( 1 ) )
5250, 51mp1i 13 . . . . . 6  |-  (  T. 
->  ( x  e.  RR+  |->  ( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  e.  O ( 1 ) )
5347, 52o1res2 12031 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) ) )  e.  O ( 1 ) )
54 divlogrlim 19976 . . . . . 6  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
55 rlimo1 12084 . . . . . 6  |-  ( ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  / 
( log `  x
) ) )  e.  O ( 1 ) )
5654, 55mp1i 13 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O ( 1 ) )
5727, 45, 53, 56o1mul2 12092 . . . 4  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  ( ( ( log `  x ) ^ 2 )  / 
2 ) )  x.  ( 1  /  ( log `  x ) ) ) )  e.  O
( 1 ) )
5844, 57eqeltrd 2358 . . 3  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) ) )  e.  O
( 1 ) )
598, 23, 25divcld 9531 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  e.  CC )
6023halfcld 9951 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  2 )  e.  CC )
6159, 60subcld 9152 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) )  e.  CC )
62 elfznn 10813 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
6362adantl 454 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
64 vmacl 20350 . . . . . . . . . . 11  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
6563, 64syl 17 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
6665, 63nndivred 9789 . . . . . . . . 9  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
6718adantr 453 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
6863nnrpd 10384 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
6967, 68rpdivcld 10402 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
7069relogcld 19968 . . . . . . . . 9  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
7166, 70remulcld 8858 . . . . . . . 8  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  e.  RR )
721, 71fsumrecl 12201 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  e.  RR )
7372recnd 8856 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  e.  CC )
7424rpcnd 10387 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
7573, 74, 25divcld 9531 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  CC )
7674halfcld 9951 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  2 )  e.  CC )
7775, 76subcld 9152 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) )  e.  CC )
7859, 75, 60nnncan2d 9187 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) )  -  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  =  ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) ) )
798, 73, 23, 25divsubdird 9570 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  / 
( log `  x
) )  =  ( ( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) ) )
80 fzfid 11029 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
8165adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (Λ `  n
)  e.  RR )
8263adantr 453 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  n  e.  NN )
83 elfznn 10813 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
8483adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  NN )
8582, 84nnmulcld 9788 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( n  x.  m )  e.  NN )
8681, 85nndivred 9789 . . . . . . . . . . . 12  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  n )  /  (
n  x.  m ) )  e.  RR )
8780, 86fsumrecl 12201 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  e.  RR )
8887recnd 8856 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  e.  CC )
8971recnd 8856 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  e.  CC )
901, 88, 89fsumsub 12244 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  -  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  /  ( n  x.  m ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) ) )
9165recnd 8856 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
9263nncnd 9757 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
9363nnne0d 9785 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
9491, 92, 93divcld 9531 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
9584nnrecred 9786 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( 1  /  m )  e.  RR )
9680, 95fsumrecl 12201 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  e.  RR )
9796recnd 8856 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  e.  CC )
9870recnd 8856 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
9994, 97, 98subdid 9230 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) ) )  =  ( ( ( (Λ `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
) )  -  (
( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )
10091adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (Λ `  n
)  e.  CC )
10192adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  n  e.  CC )
10284nncnd 9757 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  CC )
10393adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  n  =/=  0 )
10484nnne0d 9785 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  =/=  0 )
105100, 101, 102, 103, 104divdiv1d 9562 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
(Λ `  n )  /  n )  /  m
)  =  ( (Λ `  n )  /  (
n  x.  m ) ) )
106100, 101, 103divcld 9531 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
107106, 102, 104divrecd 9534 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
(Λ `  n )  /  n )  /  m
)  =  ( ( (Λ `  n )  /  n )  x.  (
1  /  m ) ) )
108105, 107eqtr3d 2318 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  n )  /  (
n  x.  m ) )  =  ( ( (Λ `  n )  /  n )  x.  (
1  /  m ) ) )
109108sumeq2dv 12170 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( (Λ `  n
)  /  n )  x.  ( 1  /  m ) ) )
110102, 104reccld 9524 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( 1  /  m )  e.  CC )
11180, 94, 110fsummulc2 12240 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( 1  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( ( (Λ `  n
)  /  n )  x.  ( 1  /  m ) ) )
112109, 111eqtr4d 2319 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  =  ( ( (Λ `  n )  /  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
) ) )
113112oveq1d 5834 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  n )  /  (
n  x.  m ) )  -  ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) )  =  ( ( ( (Λ `  n
)  /  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( 1  /  m
) )  -  (
( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )
11499, 113eqtr4d 2319 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) ) )  =  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  -  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) ) )
115114sumeq2dv 12170 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) )  -  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) ) )
116 vmasum 20449 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  sum_ n  e.  { y  e.  NN  |  y  ||  k }  (Λ `  n )  =  ( log `  k
) )
1173, 116syl 17 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ n  e. 
{ y  e.  NN  |  y  ||  k }  (Λ `  n )  =  ( log `  k
) )
118117oveq1d 5834 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ n  e.  { y  e.  NN  |  y  ||  k }  (Λ `  n
)  /  k )  =  ( ( log `  k )  /  k
) )
119 fzfid 11029 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... k )  e. 
Fin )
120 sgmss 20338 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  { y  e.  NN  |  y 
||  k }  C_  ( 1 ... k
) )
1213, 120syl 17 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  { y  e.  NN  |  y  ||  k }  C_  ( 1 ... k ) )
122 ssfi 7078 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... k
)  e.  Fin  /\  { y  e.  NN  | 
y  ||  k }  C_  ( 1 ... k
) )  ->  { y  e.  NN  |  y 
||  k }  e.  Fin )
123119, 121, 122syl2anc 644 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  { y  e.  NN  |  y  ||  k }  e.  Fin )
1243nncnd 9757 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  e.  CC )
125 ssrab2 3259 . . . . . . . . . . . . . . . . . 18  |-  { y  e.  NN  |  y 
||  k }  C_  NN
126 simprr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  { y  e.  NN  |  y  ||  k } )
127125, 126sseldi 3179 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  ->  n  e.  NN )
128127, 64syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
(Λ `  n )  e.  RR )
129128recnd 8856 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
(Λ `  n )  e.  CC )
130129anassrs 631 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  /\  n  e.  {
y  e.  NN  | 
y  ||  k }
)  ->  (Λ `  n
)  e.  CC )
1313nnne0d 9785 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  k  =/=  0 )
132123, 124, 130, 131fsumdivc 12242 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ n  e.  { y  e.  NN  |  y  ||  k }  (Λ `  n
)  /  k )  =  sum_ n  e.  {
y  e.  NN  | 
y  ||  k } 
( (Λ `  n )  /  k ) )
133118, 132eqtr3d 2318 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  k )  / 
k )  =  sum_ n  e.  { y  e.  NN  |  y  ||  k }  ( (Λ `  n )  /  k
) )
134133sumeq2dv 12170 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  =  sum_ k  e.  ( 1 ... ( |_
`  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
(Λ `  n )  / 
k ) )
135 oveq2 5827 . . . . . . . . . . . 12  |-  ( k  =  ( n  x.  m )  ->  (
(Λ `  n )  / 
k )  =  ( (Λ `  n )  /  ( n  x.  m ) ) )
1362ad2antrl 710 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  NN )
137136nncnd 9757 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  e.  CC )
138136nnne0d 9785 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
k  =/=  0 )
139129, 137, 138divcld 9531 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
k  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  { y  e.  NN  |  y  ||  k } ) )  -> 
( (Λ `  n )  /  k )  e.  CC )
140135, 10, 139dvdsflsumcom 20422 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  { y  e.  NN  |  y 
||  k }  (
(Λ `  n )  / 
k )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  /  ( n  x.  m ) ) )
141134, 140eqtrd 2316 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  /  ( n  x.  m ) ) )
142141oveq1d 5834 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  /  ( n  x.  m ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) ) )
14390, 115, 1423eqtr4rd 2327 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) ) )
144143oveq1d 5834 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  x ) ) ( ( log `  k
)  /  k )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  / 
( log `  x
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )
14578, 79, 1443eqtr2d 2322 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) )  -  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )
146145mpteq2dva 4107 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) )  -  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) ) )
147 1re 8832 . . . . . . . 8  |-  1  e.  RR
148147a1i 12 . . . . . . 7  |-  (  T. 
->  1  e.  RR )
1491, 66fsumrecl 12201 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  RR )
150149, 24rerpdivcld 10412 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  e.  RR )
151 ioossre 10706 . . . . . . . . . . 11  |-  ( 1 (,)  +oo )  C_  RR
152 ax-1cn 8790 . . . . . . . . . . 11  |-  1  e.  CC
153 o1const 12087 . . . . . . . . . . 11  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  1  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O ( 1 ) )
154151, 152, 153mp2an 655 . . . . . . . . . 10  |-  ( x  e.  ( 1 (,) 
+oo )  |->  1 )  e.  O ( 1 )
155154a1i 12 . . . . . . . . 9  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O
( 1 ) )
156150recnd 8856 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  e.  CC )
15712rpcnd 10387 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
158149recnd 8856 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
159158, 23, 23, 25divsubdird 9570 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  /  ( log `  x ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) )  -  ( ( log `  x
)  /  ( log `  x ) ) ) )
160158, 23subcld 9152 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  CC )
161160, 23, 25divrecd 9534 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  /  ( log `  x ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) )  x.  ( 1  /  ( log `  x ) ) ) )
16223, 25dividd 9529 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
163162oveq2d 5835 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  (
( log `  x
)  /  ( log `  x ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) )  - 
1 ) )
164159, 161, 1633eqtr3rd 2325 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  1 )  =  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  x.  ( 1  / 
( log `  x
) ) ) )
165164mpteq2dva 4107 . . . . . . . . . . 11  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  1 ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  x.  ( 1  / 
( log `  x
) ) ) ) )
166149, 19resubcld 9206 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  RR )
167 vmadivsum 20625 . . . . . . . . . . . . . 14  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O ( 1 )
168167a1i 12 . . . . . . . . . . . . 13  |-  (  T. 
->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O ( 1 ) )
16947, 168o1res2 12031 . . . . . . . . . . . 12  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O ( 1 ) )
170166, 45, 169, 56o1mul2 12092 . . . . . . . . . . 11  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  (
1  /  ( log `  x ) ) ) )  e.  O ( 1 ) )
171165, 170eqeltrd 2358 . . . . . . . . . 10  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  1 ) )  e.  O
( 1 ) )
172156, 157, 171o1dif 12097 . . . . . . . . 9  |-  (  T. 
->  ( ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) ) )  e.  O ( 1 )  <-> 
( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O
( 1 ) ) )
173155, 172mpbird 225 . . . . . . . 8  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) ) )  e.  O ( 1 ) )
174150, 173o1lo1d 12007 . . . . . . 7  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) ) )  e. 
<_ O ( 1 ) )
17596, 70resubcld 9206 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( 1  /  m )  -  ( log `  ( x  /  n ) ) )  e.  RR )
17666, 175remulcld 8858 . . . . . . . . 9  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) ) )  e.  RR )
1771, 176fsumrecl 12201 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  e.  RR )
178177, 24rerpdivcld 10412 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) )  e.  RR )
179147a1i 12 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
180 vmage0 20353 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
18163, 180syl 17 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
18265, 68, 181divge0d 10421 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( (Λ `  n )  /  n ) )
18369rpred 10385 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
18492mulid2d 8848 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
185 fznnfl 10960 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
18610, 185syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
187186simplbda 609 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
188184, 187eqbrtrd 4044 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
18910adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
190179, 189, 68lemuldivd 10430 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
191188, 190mpbid 203 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
192 harmonicubnd 20297 . . . . . . . . . . . . . 14  |-  ( ( ( x  /  n
)  e.  RR  /\  1  <_  ( x  /  n ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  <_  ( ( log `  ( x  /  n
) )  +  1 ) )
193183, 191, 192syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  <_  ( ( log `  ( x  /  n ) )  +  1 ) )
19496, 70, 179lesubadd2d 9366 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) )  <_  1  <->  sum_
m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  <_  ( ( log `  ( x  /  n
) )  +  1 ) ) )
195193, 194mpbird 225 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( 1  /  m )  -  ( log `  ( x  /  n ) ) )  <_  1 )
196175, 179, 66, 182, 195lemul2ad 9692 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) ) )  <_ 
( ( (Λ `  n
)  /  n )  x.  1 ) )
19794mulid1d 8847 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  1 )  =  ( (Λ `  n )  /  n
) )
198196, 197breqtrd 4048 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) ) )  <_ 
( (Λ `  n )  /  n ) )
1991, 176, 66, 198fsumle 12251 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  <_  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n ) )
200177, 149, 24, 199lediv1dd 10439 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) )  <_  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) ) )
201200adantrr 699 . . . . . . 7  |-  ( (  T.  /\  ( x  e.  ( 1 (,) 
+oo )  /\  1  <_  x ) )  -> 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) )  <_  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) ) )
202148, 174, 150, 178, 201lo1le 12119 . . . . . 6  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )  e. 
<_ O ( 1 ) )
203 0re 8833 . . . . . . . 8  |-  0  e.  RR
204203a1i 12 . . . . . . 7  |-  (  T. 
->  0  e.  RR )
205 harmoniclbnd 20296 . . . . . . . . . . . 12  |-  ( ( x  /  n )  e.  RR+  ->  ( log `  ( x  /  n
) )  <_  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
) )
20669, 205syl 17 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  <_  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
) )
20796, 70subge0d 9357 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  <_  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) )  <->  ( log `  ( x  /  n
) )  <_  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
) ) )
208206, 207mpbird 225 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( 1  /  m )  -  ( log `  (
x  /  n ) ) ) )
20966, 175, 182, 208mulge0d 9344 . . . . . . . . 9  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) ) )
2101, 176, 209fsumge0 12247 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) ) )
211177, 24, 210divge0d 10421 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )
212178, 204, 211o1lo12 12006 . . . . . 6  |-  (  T. 
->  ( ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )  e.  O ( 1 )  <-> 
( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )  e. 
<_ O ( 1 ) ) )
213202, 212mpbird 225 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( 1  /  m
)  -  ( log `  ( x  /  n
) ) ) )  /  ( log `  x
) ) )  e.  O ( 1 ) )
214146, 213eqeltrd 2358 . . . 4  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) )  -  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) ) )  e.  O ( 1 ) )
21561, 77, 214o1dif 12097 . . 3  |-  (  T. 
->  ( ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ k  e.  ( 1 ... ( |_ `  x ) ) ( ( log `  k
)  /  k )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) ) )  e.  O
( 1 )  <->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  /  ( log `  x
) )  -  (
( log `  x
)  /  2 ) ) )  e.  O
( 1 ) ) )
21658, 215mpbid 203 . 2  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  e.  O ( 1 ) )
217216trud 1316 1  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  e.  O ( 1 )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 936    T. wtru 1309    = wceq 1624    e. wcel 1685    =/= wne 2447   {crab 2548    C_ wss 3153   class class class wbr 4024    e. cmpt 4078   dom cdm 4688   -->wf 5217   ` cfv 5221  (class class class)co 5819   Fincfn 6858   CCcc 8730   RRcr 8731   0cc0 8732   1c1 8733    + caddc 8735    x. cmul 8737    +oocpnf 8859    < clt 8862    <_ cle 8863    - cmin 9032    / cdiv 9418   NNcn 9741   2c2 9790   RR+crp 10349   (,)cioo 10650   ...cfz 10776   |_cfl 10918   ^cexp 11098   abscabs 11713    ~~> r crli 11953   O ( 1 )co1 11954   <_ O ( 1 )clo1 11955   sum_csu 12152   _eceu 12338    || cdivides 12525   logclog 19906  Λcvma 20323
This theorem is referenced by:  vmalogdivsum  20682  2vmadivsumlem  20683  selberg4lem1  20703
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-inf2 7337  ax-cnex 8788  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-mulcom 8796  ax-addass 8797  ax-mulass 8798  ax-distr 8799  ax-i2m1 8800  ax-1ne0 8801  ax-1rid 8802  ax-rnegex 8803  ax-rrecex 8804  ax-cnre 8805  ax-pre-lttri 8806  ax-pre-lttrn 8807  ax-pre-ltadd 8808  ax-pre-mulgt0 8809  ax-pre-sup 8810  ax-addf 8811  ax-mulf 8812
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-se 4352  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-isom 5230  df-ov 5822  df-oprab 5823  df-mpt2 5824  df-of 6039  df-1st 6083  df-2nd 6084  df-iota 6252  df-riota 6299  df-recs 6383  df-rdg 6418  df-1o 6474  df-2o 6475  df-oadd 6478  df-er 6655  df-map 6769  df-pm 6770  df-ixp 6813  df-en 6859  df-dom 6860  df-sdom 6861  df-fin 6862  df-fi 7160  df-sup 7189  df-oi 7220  df-card 7567  df-cda 7789  df-pnf 8864  df-mnf 8865  df-xr 8866  df-ltxr 8867  df-le 8868  df-sub 9034  df-neg 9035  df-div 9419  df-nn 9742  df-2 9799  df-3 9800  df-4 9801  df-5 9802  df-6 9803  df-7 9804  df-8 9805  df-9 9806  df-10 9807  df-n0 9961  df-z 10020  df-dec 10120  df-uz 10226  df-q 10312  df-rp 10350  df-xneg 10447  df-xadd 10448  df-xmul 10449  df-ioo 10654  df-ioc 10655  df-ico 10656  df-icc 10657  df-fz 10777  df-fzo 10865  df-fl 10919  df-mod 10968  df-seq 11041  df-exp 11099  df-fac 11283  df-bc 11310  df-hash 11332  df-shft 11556  df-cj 11578  df-re 11579  df-im 11580  df-sqr 11714  df-abs 11715  df-limsup 11939  df-clim 11956  df-rlim 11957  df-o1 11958  df-lo1 11959  df-sum 12153  df-ef 12343  df-e 12344  df-sin 12345  df-cos 12346  df-pi 12348  df-dvds 12526  df-gcd 12680  df-prm 12753  df-pc 12884  df-struct 13144  df-ndx 13145  df-slot 13146  df-base 13147  df-sets 13148  df-ress 13149  df-plusg 13215  df-mulr 13216  df-starv 13217  df-sca 13218  df-vsca 13219  df-tset 13221  df-ple 13222  df-ds 13224  df-hom 13226  df-cco 13227  df-rest 13321  df-topn 13322  df-topgen 13338  df-pt 13339  df-prds 13342  df-xrs 13397  df-0g 13398  df-gsum 13399  df-qtop 13404  df-imas 13405  df-xps 13407  df-mre 13482  df-mrc 13483  df-acs 13485  df-mnd 14361  df-submnd 14410  df-mulg 14486  df-cntz 14787  df-cmn 15085  df-xmet 16367  df-met 16368  df-bl 16369  df-mopn 16370  df-cnfld 16372  df-top 16630  df-bases 16632  df-topon 16633  df-topsp 16634  df-cld 16750  df-ntr 16751  df-cls 16752  df-nei 16829  df-lp 16862  df-perf 16863  df-cn 16951  df-cnp 16952  df-haus 17037  df-cmp 17108  df-tx 17251  df-hmeo 17440  df-fbas 17514  df-fg 17515  df-fil 17535  df-fm 17627  df-flim 17628  df-flf 17629  df-xms 17879  df-ms 17880  df-tms 17881  df-cncf 18376  df-limc 19210  df-dv 19211  df-log 19908  df-cxp 19909  df-em 20281  df-cht 20328  df-vma 20329  df-chp 20330  df-ppi 20331
  Copyright terms: Public domain W3C validator