Step |
Hyp |
Ref |
Expression |
1 |
|
fzfid |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
2 |
|
elfznn |
|- ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN ) |
3 |
2
|
adantl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN ) |
4 |
3
|
nnrpd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. RR+ ) |
5 |
4
|
relogcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` k ) e. RR ) |
6 |
5 3
|
nndivred |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) e. RR ) |
7 |
1 6
|
fsumrecl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. RR ) |
8 |
7
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. CC ) |
9 |
|
elioore |
|- ( x e. ( 1 (,) +oo ) -> x e. RR ) |
10 |
9
|
adantl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR ) |
11 |
|
1rp |
|- 1 e. RR+ |
12 |
11
|
a1i |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ ) |
13 |
|
1red |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR ) |
14 |
|
eliooord |
|- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) ) |
15 |
14
|
adantl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) ) |
16 |
15
|
simpld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x ) |
17 |
13 10 16
|
ltled |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x ) |
18 |
10 12 17
|
rpgecld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ ) |
19 |
18
|
relogcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR ) |
20 |
19
|
resqcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. RR ) |
21 |
20
|
rehalfcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. RR ) |
22 |
21
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. CC ) |
23 |
19
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC ) |
24 |
10 16
|
rplogcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ ) |
25 |
24
|
rpne0d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 ) |
26 |
8 22 23 25
|
divsubdird |
|- ( ( 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 ) ) ) ) |
27 |
7 21
|
resubcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. RR ) |
28 |
27
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. CC ) |
29 |
28 23 25
|
divrecd |
|- ( ( 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 ) ) ) ) |
30 |
20
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. CC ) |
31 |
|
2cnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC ) |
32 |
|
2ne0 |
|- 2 =/= 0 |
33 |
32
|
a1i |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 ) |
34 |
30 31 23 33 25
|
divdiv32d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) ) |
35 |
23
|
sqvald |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) = ( ( log ` x ) x. ( log ` x ) ) ) |
36 |
35
|
oveq1d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) ) |
37 |
23 23 25
|
divcan3d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) = ( log ` x ) ) |
38 |
36 37
|
eqtrd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( log ` x ) ) |
39 |
38
|
oveq1d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) = ( ( log ` x ) / 2 ) ) |
40 |
34 39
|
eqtrd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( log ` x ) / 2 ) ) |
41 |
40
|
oveq2d |
|- ( ( 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 ) ) ) |
42 |
26 29 41
|
3eqtr3rd |
|- ( ( 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 ) ) ) ) |
43 |
42
|
mpteq2dva |
|- ( 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 ) ) ) ) ) |
44 |
24
|
rprecred |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR ) |
45 |
18
|
ex |
|- ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) ) |
46 |
45
|
ssrdv |
|- ( T. -> ( 1 (,) +oo ) C_ RR+ ) |
47 |
|
eqid |
|- ( 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 ) ) ) |
48 |
47
|
logdivsum |
|- ( ( 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 ) ) ) |
49 |
48
|
simp2i |
|- ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~>r |
50 |
|
rlimdmo1 |
|- ( ( 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) ) |
51 |
49 50
|
mp1i |
|- ( T. -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) ) |
52 |
46 51
|
o1res2 |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) ) |
53 |
|
divlogrlim |
|- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 |
54 |
|
rlimo1 |
|- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~>r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) ) |
55 |
53 54
|
mp1i |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) ) |
56 |
27 44 52 55
|
o1mul2 |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) ) |
57 |
43 56
|
eqeltrd |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) ) |
58 |
8 23 25
|
divcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) e. CC ) |
59 |
23
|
halfcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC ) |
60 |
58 59
|
subcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC ) |
61 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN ) |
62 |
61
|
adantl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN ) |
63 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
64 |
62 63
|
syl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR ) |
65 |
64 62
|
nndivred |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR ) |
66 |
18
|
adantr |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ ) |
67 |
62
|
nnrpd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ ) |
68 |
66 67
|
rpdivcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ ) |
69 |
68
|
relogcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR ) |
70 |
65 69
|
remulcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR ) |
71 |
1 70
|
fsumrecl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR ) |
72 |
71
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) |
73 |
24
|
rpcnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC ) |
74 |
72 73 25
|
divcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC ) |
75 |
73
|
halfcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC ) |
76 |
74 75
|
subcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC ) |
77 |
58 74 59
|
nnncan2d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` 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 ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) ) |
78 |
8 72 23 25
|
divsubdird |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) ) |
79 |
|
fzfid |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin ) |
80 |
64
|
adantr |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` n ) e. RR ) |
81 |
62
|
adantr |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. NN ) |
82 |
|
elfznn |
|- ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN ) |
83 |
82
|
adantl |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN ) |
84 |
81 83
|
nnmulcld |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) e. NN ) |
85 |
80 84
|
nndivred |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` n ) / ( n x. m ) ) e. RR ) |
86 |
79 85
|
fsumrecl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) e. RR ) |
87 |
86
|
recnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) e. CC ) |
88 |
70
|
recnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) |
89 |
1 87 88
|
fsumsub |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
90 |
64
|
recnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC ) |
91 |
62
|
nncnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC ) |
92 |
62
|
nnne0d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 ) |
93 |
90 91 92
|
divcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC ) |
94 |
83
|
nnrecred |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. RR ) |
95 |
79 94
|
fsumrecl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. RR ) |
96 |
95
|
recnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. CC ) |
97 |
69
|
recnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC ) |
98 |
93 96 97
|
subdid |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
99 |
90
|
adantr |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` n ) e. CC ) |
100 |
91
|
adantr |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. CC ) |
101 |
83
|
nncnd |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC ) |
102 |
92
|
adantr |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n =/= 0 ) |
103 |
83
|
nnne0d |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m =/= 0 ) |
104 |
99 100 101 102 103
|
divdiv1d |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` n ) / n ) / m ) = ( ( Lam ` n ) / ( n x. m ) ) ) |
105 |
99 100 102
|
divcld |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` n ) / n ) e. CC ) |
106 |
105 101 103
|
divrecd |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` n ) / n ) / m ) = ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) ) |
107 |
104 106
|
eqtr3d |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` n ) / ( n x. m ) ) = ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) ) |
108 |
107
|
sumeq2dv |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) ) |
109 |
101 103
|
reccld |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. CC ) |
110 |
79 93 109
|
fsummulc2 |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` n ) / n ) x. ( 1 / m ) ) ) |
111 |
108 110
|
eqtr4d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) = ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) ) |
112 |
111
|
oveq1d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
113 |
98 112
|
eqtr4d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
114 |
113
|
sumeq2dv |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` 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 ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
115 |
|
vmasum |
|- ( k e. NN -> sum_ n e. { y e. NN | y || k } ( Lam ` n ) = ( log ` k ) ) |
116 |
3 115
|
syl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> sum_ n e. { y e. NN | y || k } ( Lam ` n ) = ( log ` k ) ) |
117 |
116
|
oveq1d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. { y e. NN | y || k } ( Lam ` n ) / k ) = ( ( log ` k ) / k ) ) |
118 |
|
fzfid |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... k ) e. Fin ) |
119 |
|
dvdsssfz1 |
|- ( k e. NN -> { y e. NN | y || k } C_ ( 1 ... k ) ) |
120 |
3 119
|
syl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } C_ ( 1 ... k ) ) |
121 |
118 120
|
ssfid |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } e. Fin ) |
122 |
3
|
nncnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. CC ) |
123 |
|
ssrab2 |
|- { y e. NN | y || k } C_ NN |
124 |
|
simprr |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. { y e. NN | y || k } ) |
125 |
123 124
|
sseldi |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. NN ) |
126 |
125 63
|
syl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( Lam ` n ) e. RR ) |
127 |
126
|
recnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( Lam ` n ) e. CC ) |
128 |
127
|
anassrs |
|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ n e. { y e. NN | y || k } ) -> ( Lam ` n ) e. CC ) |
129 |
3
|
nnne0d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k =/= 0 ) |
130 |
121 122 128 129
|
fsumdivc |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. { y e. NN | y || k } ( Lam ` n ) / k ) = sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) ) |
131 |
117 130
|
eqtr3d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) = sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) ) |
132 |
131
|
sumeq2dv |
|- ( ( 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 } ( ( Lam ` n ) / k ) ) |
133 |
|
oveq2 |
|- ( k = ( n x. m ) -> ( ( Lam ` n ) / k ) = ( ( Lam ` n ) / ( n x. m ) ) ) |
134 |
2
|
ad2antrl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. NN ) |
135 |
134
|
nncnd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. CC ) |
136 |
134
|
nnne0d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k =/= 0 ) |
137 |
127 135 136
|
divcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( ( Lam ` n ) / k ) e. CC ) |
138 |
133 10 137
|
dvdsflsumcom |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( Lam ` n ) / k ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) ) |
139 |
132 138
|
eqtrd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) ) |
140 |
139
|
oveq1d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) / ( n x. m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
141 |
89 114 140
|
3eqtr4rd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) |
142 |
141
|
oveq1d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) |
143 |
77 78 142
|
3eqtr2d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) |
144 |
143
|
mpteq2dva |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) ) |
145 |
|
1red |
|- ( T. -> 1 e. RR ) |
146 |
1 65
|
fsumrecl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR ) |
147 |
146 24
|
rerpdivcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. RR ) |
148 |
|
ioossre |
|- ( 1 (,) +oo ) C_ RR |
149 |
|
ax-1cn |
|- 1 e. CC |
150 |
|
o1const |
|- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) ) |
151 |
148 149 150
|
mp2an |
|- ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) |
152 |
151
|
a1i |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) ) |
153 |
147
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) e. CC ) |
154 |
12
|
rpcnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC ) |
155 |
146
|
recnd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC ) |
156 |
155 23 23 25
|
divsubdird |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - ( ( log ` x ) / ( log ` x ) ) ) ) |
157 |
155 23
|
subcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC ) |
158 |
157 23 25
|
divrecd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) |
159 |
23 25
|
dividd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 ) |
160 |
159
|
oveq2d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - ( ( log ` x ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) |
161 |
156 158 160
|
3eqtr3rd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) |
162 |
161
|
mpteq2dva |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) ) |
163 |
146 19
|
resubcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR ) |
164 |
|
vmadivsum |
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) |
165 |
164
|
a1i |
|- ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) ) |
166 |
46 165
|
o1res2 |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) ) |
167 |
163 44 166 55
|
o1mul2 |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) ) |
168 |
162 167
|
eqeltrd |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O(1) ) |
169 |
153 154 168
|
o1dif |
|- ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) ) ) |
170 |
152 169
|
mpbird |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. O(1) ) |
171 |
147 170
|
o1lo1d |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) e. <_O(1) ) |
172 |
95 69
|
resubcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) e. RR ) |
173 |
65 172
|
remulcld |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR ) |
174 |
1 173
|
fsumrecl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR ) |
175 |
174 24
|
rerpdivcld |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) e. RR ) |
176 |
|
1red |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR ) |
177 |
|
vmage0 |
|- ( n e. NN -> 0 <_ ( Lam ` n ) ) |
178 |
62 177
|
syl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) ) |
179 |
64 67 178
|
divge0d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) ) |
180 |
68
|
rpred |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR ) |
181 |
91
|
mulid2d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n ) |
182 |
|
fznnfl |
|- ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) ) |
183 |
10 182
|
syl |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) ) |
184 |
183
|
simplbda |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x ) |
185 |
181 184
|
eqbrtrd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x ) |
186 |
10
|
adantr |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR ) |
187 |
176 186 67
|
lemuldivd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) ) |
188 |
185 187
|
mpbid |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) ) |
189 |
|
harmonicubnd |
|- ( ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) ) |
190 |
180 188 189
|
syl2anc |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) ) |
191 |
95 69 176
|
lesubadd2d |
|- ( ( ( 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 ) ) ) |
192 |
190 191
|
mpbird |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <_ 1 ) |
193 |
172 176 65 179 192
|
lemul2ad |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ ( ( ( Lam ` n ) / n ) x. 1 ) ) |
194 |
93
|
mulid1d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. 1 ) = ( ( Lam ` n ) / n ) ) |
195 |
193 194
|
breqtrd |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ ( ( Lam ` n ) / n ) ) |
196 |
1 173 65 195
|
fsumle |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) |
197 |
174 146 24 196
|
lediv1dd |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) |
198 |
197
|
adantrr |
|- ( ( T. /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) / ( log ` x ) ) ) |
199 |
145 171 147 175 198
|
lo1le |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. <_O(1) ) |
200 |
|
0red |
|- ( T. -> 0 e. RR ) |
201 |
|
harmoniclbnd |
|- ( ( x / n ) e. RR+ -> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) |
202 |
68 201
|
syl |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) |
203 |
95 69
|
subge0d |
|- ( ( ( 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 ) ) ) |
204 |
202 203
|
mpbird |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) |
205 |
65 172 179 204
|
mulge0d |
|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) |
206 |
1 173 205
|
fsumge0 |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) |
207 |
174 24 206
|
divge0d |
|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) |
208 |
175 200 207
|
o1lo12 |
|- ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` 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 ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. <_O(1) ) ) |
209 |
199 208
|
mpbird |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. O(1) ) |
210 |
144 209
|
eqeltrd |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) ) |
211 |
60 76 210
|
o1dif |
|- ( 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 ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) ) ) |
212 |
57 211
|
mpbid |
|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) ) |
213 |
212
|
mptru |
|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) |