Metamath Proof Explorer

Theorem harmoniclbnd

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

Ref Expression
Assertion harmoniclbnd 
|- ( A e. RR+ -> ( log ` A ) <_ sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) )

Proof

Step Hyp Ref Expression
1 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
2 rprege0 
 |-  ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
3 flge0nn0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
4 2 3 syl 
 |-  ( A e. RR+ -> ( |_ ` A ) e. NN0 )
5 nn0p1nn 
 |-  ( ( |_ ` A ) e. NN0 -> ( ( |_ ` A ) + 1 ) e. NN )
6 4 5 syl 
 |-  ( A e. RR+ -> ( ( |_ ` A ) + 1 ) e. NN )
7 6 nnrpd 
 |-  ( A e. RR+ -> ( ( |_ ` A ) + 1 ) e. RR+ )
8 relogcl 
 |-  ( ( ( |_ ` A ) + 1 ) e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) e. RR )
9 7 8 syl 
 |-  ( A e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) e. RR )
10 fzfid 
 |-  ( A e. RR+ -> ( 1 ... ( |_ ` A ) ) e. Fin )
11 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. NN )
12 11 adantl 
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. NN )
13 12 nnrecred 
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / m ) e. RR )
14 10 13 fsumrecl 
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) e. RR )
15 rpre 
 |-  ( A e. RR+ -> A e. RR )
16 fllep1 
 |-  ( A e. RR -> A <_ ( ( |_ ` A ) + 1 ) )
17 15 16 syl 
 |-  ( A e. RR+ -> A <_ ( ( |_ ` A ) + 1 ) )
18 id 
 |-  ( A e. RR+ -> A e. RR+ )
19 18 7 logled 
 |-  ( A e. RR+ -> ( A <_ ( ( |_ ` A ) + 1 ) <-> ( log ` A ) <_ ( log ` ( ( |_ ` A ) + 1 ) ) ) )
20 17 19 mpbid 
 |-  ( A e. RR+ -> ( log ` A ) <_ ( log ` ( ( |_ ` A ) + 1 ) ) )
21 harmonicbnd3 
 |-  ( ( |_ ` A ) e. NN0 -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) )
22 4 21 syl 
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) )
23 0re 
 |-  0 e. RR
24 emre 
 |-  gamma e. RR
25 23 24 elicc2i 
 |-  ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) <-> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. RR /\ 0 <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) /\ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <_ gamma ) )
26 25 simp2bi 
 |-  ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) -> 0 <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
27 22 26 syl 
 |-  ( A e. RR+ -> 0 <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
28 14 9 subge0d 
 |-  ( A e. RR+ -> ( 0 <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <-> ( log ` ( ( |_ ` A ) + 1 ) ) <_ sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) ) )
29 27 28 mpbid 
 |-  ( A e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) <_ sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) )
30 1 9 14 20 29 letrd 
 |-  ( A e. RR+ -> ( log ` A ) <_ sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) )