Step |
Hyp |
Ref |
Expression |
1 |
|
logdivsum.1 |
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) |
2 |
|
mulog2sumlem.1 |
|- ( ph -> F ~~>r L ) |
3 |
|
2cn |
|- 2 e. CC |
4 |
3
|
a1i |
|- ( ( ph /\ x e. RR+ ) -> 2 e. CC ) |
5 |
|
fzfid |
|- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
6 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN ) |
7 |
6
|
adantl |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN ) |
8 |
|
mucl |
|- ( n e. NN -> ( mmu ` n ) e. ZZ ) |
9 |
7 8
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ ) |
10 |
9
|
zred |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR ) |
11 |
10 7
|
nndivred |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR ) |
12 |
11
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC ) |
13 |
|
simpr |
|- ( ( ph /\ x e. RR+ ) -> x e. RR+ ) |
14 |
6
|
nnrpd |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ ) |
15 |
|
rpdivcl |
|- ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ ) |
16 |
13 14 15
|
syl2an |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ ) |
17 |
16
|
relogcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR ) |
18 |
17
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC ) |
19 |
18
|
sqcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. CC ) |
20 |
19
|
halfcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) e. CC ) |
21 |
12 20
|
mulcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) e. CC ) |
22 |
5 21
|
fsumcl |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) e. CC ) |
23 |
|
relogcl |
|- ( x e. RR+ -> ( log ` x ) e. RR ) |
24 |
23
|
adantl |
|- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR ) |
25 |
24
|
recnd |
|- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC ) |
26 |
4 22 25
|
subdid |
|- ( ( ph /\ x e. RR+ ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) - ( 2 x. ( log ` x ) ) ) ) |
27 |
5 4 21
|
fsummulc2 |
|- ( ( ph /\ x e. RR+ ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) ) |
28 |
3
|
a1i |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC ) |
29 |
28 12 20
|
mul12d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = ( ( ( mmu ` n ) / n ) x. ( 2 x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) ) |
30 |
|
2ne0 |
|- 2 =/= 0 |
31 |
30
|
a1i |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 =/= 0 ) |
32 |
19 28 31
|
divcan2d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) = ( ( log ` ( x / n ) ) ^ 2 ) ) |
33 |
32
|
oveq2d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( 2 x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) ) |
34 |
29 33
|
eqtrd |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) ) |
35 |
34
|
sumeq2dv |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) ) |
36 |
27 35
|
eqtrd |
|- ( ( ph /\ x e. RR+ ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) ) |
37 |
36
|
oveq1d |
|- ( ( ph /\ x e. RR+ ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) - ( 2 x. ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) |
38 |
26 37
|
eqtrd |
|- ( ( ph /\ x e. RR+ ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) |
39 |
38
|
mpteq2dva |
|- ( ph -> ( x e. RR+ |-> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) ) |
40 |
22 25
|
subcld |
|- ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) e. CC ) |
41 |
|
rpssre |
|- RR+ C_ RR |
42 |
|
o1const |
|- ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) ) |
43 |
41 3 42
|
mp2an |
|- ( x e. RR+ |-> 2 ) e. O(1) |
44 |
43
|
a1i |
|- ( ph -> ( x e. RR+ |-> 2 ) e. O(1) ) |
45 |
|
emre |
|- gamma e. RR |
46 |
45
|
recni |
|- gamma e. CC |
47 |
|
mulcl |
|- ( ( gamma e. CC /\ ( log ` ( x / n ) ) e. CC ) -> ( gamma x. ( log ` ( x / n ) ) ) e. CC ) |
48 |
46 18 47
|
sylancr |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( log ` ( x / n ) ) ) e. CC ) |
49 |
|
rlimcl |
|- ( F ~~>r L -> L e. CC ) |
50 |
2 49
|
syl |
|- ( ph -> L e. CC ) |
51 |
50
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> L e. CC ) |
52 |
48 51
|
subcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( log ` ( x / n ) ) ) - L ) e. CC ) |
53 |
20 52
|
addcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC ) |
54 |
12 53
|
mulcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. CC ) |
55 |
5 54
|
fsumcl |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. CC ) |
56 |
12 52
|
mulcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC ) |
57 |
5 56
|
fsumcl |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC ) |
58 |
55 25 57
|
sub32d |
|- ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) ) |
59 |
5 54 56
|
fsumsub |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) |
60 |
12 53 52
|
subdid |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) - ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) |
61 |
20 52
|
pncand |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) - ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) = ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) |
62 |
61
|
oveq2d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) - ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) |
63 |
60 62
|
eqtr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) |
64 |
63
|
sumeq2dv |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) |
65 |
59 64
|
eqtr3d |
|- ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) |
66 |
65
|
oveq1d |
|- ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) |
67 |
58 66
|
eqtrd |
|- ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) |
68 |
67
|
mpteq2dva |
|- ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) ) |
69 |
55 25
|
subcld |
|- ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) e. CC ) |
70 |
|
eqid |
|- ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) = ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) |
71 |
|
eqid |
|- ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) ) = ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) ) |
72 |
1 2 70 71
|
mulog2sumlem2 |
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) ) e. O(1) ) |
73 |
46
|
a1i |
|- ( ( ph /\ x e. RR+ ) -> gamma e. CC ) |
74 |
12 18
|
mulcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) |
75 |
5 73 74
|
fsummulc2 |
|- ( ( ph /\ x e. RR+ ) -> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) |
76 |
50
|
adantr |
|- ( ( ph /\ x e. RR+ ) -> L e. CC ) |
77 |
5 76 12
|
fsummulc1 |
|- ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. L ) ) |
78 |
75 77
|
oveq12d |
|- ( ( ph /\ x e. RR+ ) -> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. L ) ) ) |
79 |
|
mulcl |
|- ( ( gamma e. CC /\ ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) -> ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC ) |
80 |
46 74 79
|
sylancr |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC ) |
81 |
12 51
|
mulcld |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. L ) e. CC ) |
82 |
5 80 81
|
fsumsub |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. L ) ) ) |
83 |
46
|
a1i |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> gamma e. CC ) |
84 |
83 12 18
|
mul12d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( ( mmu ` n ) / n ) x. ( gamma x. ( log ` ( x / n ) ) ) ) ) |
85 |
84
|
oveq1d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = ( ( ( ( mmu ` n ) / n ) x. ( gamma x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) ) |
86 |
12 48 51
|
subdid |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) = ( ( ( ( mmu ` n ) / n ) x. ( gamma x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) ) |
87 |
85 86
|
eqtr4d |
|- ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) |
88 |
87
|
sumeq2dv |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) |
89 |
78 82 88
|
3eqtr2d |
|- ( ( ph /\ x e. RR+ ) -> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) |
90 |
89
|
mpteq2dva |
|- ( ph -> ( x e. RR+ |-> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) |
91 |
5 74
|
fsumcl |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) |
92 |
|
mulcl |
|- ( ( gamma e. CC /\ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) -> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC ) |
93 |
46 91 92
|
sylancr |
|- ( ( ph /\ x e. RR+ ) -> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC ) |
94 |
5 12
|
fsumcl |
|- ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC ) |
95 |
94 76
|
mulcld |
|- ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) e. CC ) |
96 |
46
|
a1i |
|- ( ph -> gamma e. CC ) |
97 |
|
o1const |
|- ( ( RR+ C_ RR /\ gamma e. CC ) -> ( x e. RR+ |-> gamma ) e. O(1) ) |
98 |
41 96 97
|
sylancr |
|- ( ph -> ( x e. RR+ |-> gamma ) e. O(1) ) |
99 |
|
mulogsum |
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1) |
100 |
99
|
a1i |
|- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1) ) |
101 |
73 91 98 100
|
o1mul2 |
|- ( ph -> ( x e. RR+ |-> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1) ) |
102 |
|
mudivsum |
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1) |
103 |
102
|
a1i |
|- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1) ) |
104 |
|
o1const |
|- ( ( RR+ C_ RR /\ L e. CC ) -> ( x e. RR+ |-> L ) e. O(1) ) |
105 |
41 50 104
|
sylancr |
|- ( ph -> ( x e. RR+ |-> L ) e. O(1) ) |
106 |
94 76 103 105
|
o1mul2 |
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) e. O(1) ) |
107 |
93 95 101 106
|
o1sub2 |
|- ( ph -> ( x e. RR+ |-> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) ) e. O(1) ) |
108 |
90 107
|
eqeltrrd |
|- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. O(1) ) |
109 |
69 57 72 108
|
o1sub2 |
|- ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) e. O(1) ) |
110 |
68 109
|
eqeltrrd |
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) e. O(1) ) |
111 |
4 40 44 110
|
o1mul2 |
|- ( ph -> ( x e. RR+ |-> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) ) e. O(1) ) |
112 |
39 111
|
eqeltrrd |
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) ) |