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