Metamath Proof Explorer

Theorem harmonicbnd3

Description: A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Assertion harmonicbnd3 
|- ( N e. NN0 -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( 0 [,] gamma ) )

Proof

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 ) )