Step |
Hyp |
Ref |
Expression |
1 |
|
elnn0 |
|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) ) |
2 |
|
0re |
|- 0 e. RR |
3 |
|
emre |
|- gamma e. RR |
4 |
|
2re |
|- 2 e. RR |
5 |
|
ere |
|- _e e. RR |
6 |
|
egt2lt3 |
|- ( 2 < _e /\ _e < 3 ) |
7 |
6
|
simpli |
|- 2 < _e |
8 |
4 5 7
|
ltleii |
|- 2 <_ _e |
9 |
|
2rp |
|- 2 e. RR+ |
10 |
|
epr |
|- _e e. RR+ |
11 |
|
logleb |
|- ( ( 2 e. RR+ /\ _e e. RR+ ) -> ( 2 <_ _e <-> ( log ` 2 ) <_ ( log ` _e ) ) ) |
12 |
9 10 11
|
mp2an |
|- ( 2 <_ _e <-> ( log ` 2 ) <_ ( log ` _e ) ) |
13 |
8 12
|
mpbi |
|- ( log ` 2 ) <_ ( log ` _e ) |
14 |
|
loge |
|- ( log ` _e ) = 1 |
15 |
13 14
|
breqtri |
|- ( log ` 2 ) <_ 1 |
16 |
|
1re |
|- 1 e. RR |
17 |
|
relogcl |
|- ( 2 e. RR+ -> ( log ` 2 ) e. RR ) |
18 |
9 17
|
ax-mp |
|- ( log ` 2 ) e. RR |
19 |
16 18
|
subge0i |
|- ( 0 <_ ( 1 - ( log ` 2 ) ) <-> ( log ` 2 ) <_ 1 ) |
20 |
15 19
|
mpbir |
|- 0 <_ ( 1 - ( log ` 2 ) ) |
21 |
3
|
leidi |
|- gamma <_ gamma |
22 |
|
iccss |
|- ( ( ( 0 e. RR /\ gamma e. RR ) /\ ( 0 <_ ( 1 - ( log ` 2 ) ) /\ gamma <_ gamma ) ) -> ( ( 1 - ( log ` 2 ) ) [,] gamma ) C_ ( 0 [,] gamma ) ) |
23 |
2 3 20 21 22
|
mp4an |
|- ( ( 1 - ( log ` 2 ) ) [,] gamma ) C_ ( 0 [,] gamma ) |
24 |
|
harmonicbnd2 |
|- ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) ) |
25 |
23 24
|
sselid |
|- ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( 0 [,] gamma ) ) |
26 |
|
oveq2 |
|- ( N = 0 -> ( 1 ... N ) = ( 1 ... 0 ) ) |
27 |
|
fz10 |
|- ( 1 ... 0 ) = (/) |
28 |
26 27
|
eqtrdi |
|- ( N = 0 -> ( 1 ... N ) = (/) ) |
29 |
28
|
sumeq1d |
|- ( N = 0 -> sum_ m e. ( 1 ... N ) ( 1 / m ) = sum_ m e. (/) ( 1 / m ) ) |
30 |
|
sum0 |
|- sum_ m e. (/) ( 1 / m ) = 0 |
31 |
29 30
|
eqtrdi |
|- ( N = 0 -> sum_ m e. ( 1 ... N ) ( 1 / m ) = 0 ) |
32 |
|
fv0p1e1 |
|- ( N = 0 -> ( log ` ( N + 1 ) ) = ( log ` 1 ) ) |
33 |
|
log1 |
|- ( log ` 1 ) = 0 |
34 |
32 33
|
eqtrdi |
|- ( N = 0 -> ( log ` ( N + 1 ) ) = 0 ) |
35 |
31 34
|
oveq12d |
|- ( N = 0 -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) = ( 0 - 0 ) ) |
36 |
|
0m0e0 |
|- ( 0 - 0 ) = 0 |
37 |
35 36
|
eqtrdi |
|- ( N = 0 -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) = 0 ) |
38 |
2
|
leidi |
|- 0 <_ 0 |
39 |
|
emgt0 |
|- 0 < gamma |
40 |
2 3 39
|
ltleii |
|- 0 <_ gamma |
41 |
2 3
|
elicc2i |
|- ( 0 e. ( 0 [,] gamma ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 <_ gamma ) ) |
42 |
2 38 40 41
|
mpbir3an |
|- 0 e. ( 0 [,] gamma ) |
43 |
37 42
|
eqeltrdi |
|- ( N = 0 -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( 0 [,] gamma ) ) |
44 |
25 43
|
jaoi |
|- ( ( N e. NN \/ N = 0 ) -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( 0 [,] gamma ) ) |
45 |
1 44
|
sylbi |
|- ( N e. NN0 -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( 0 [,] gamma ) ) |