Metamath Proof Explorer

Theorem harmonicubnd

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

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

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 ... ( |_ ` A ) ) e. Fin )
2 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. NN )
3 2 adantl 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. NN )
4 3 nnrecred 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / m ) e. RR )
5 1 4 fsumrecl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) e. RR )
6 flge1nn 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( |_ ` A ) e. NN )
7 6 nnrpd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( |_ ` A ) e. RR+ )
8 7 relogcld 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( log ` ( |_ ` A ) ) e. RR )
9 peano2re 
 |-  ( ( log ` ( |_ ` A ) ) e. RR -> ( ( log ` ( |_ ` A ) ) + 1 ) e. RR )
10 8 9 syl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( ( log ` ( |_ ` A ) ) + 1 ) e. RR )
11 simpl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> A e. RR )
12 0red 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 e. RR )
13 1re 
 |-  1 e. RR
14 13 a1i 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 1 e. RR )
15 0lt1 
 |-  0 < 1
16 15 a1i 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 < 1 )
17 simpr 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 1 <_ A )
18 12 14 11 16 17 ltletrd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 < A )
19 11 18 elrpd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> A e. RR+ )
20 19 relogcld 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( log ` A ) e. RR )
21 peano2re 
 |-  ( ( log ` A ) e. RR -> ( ( log ` A ) + 1 ) e. RR )
22 20 21 syl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( ( log ` A ) + 1 ) e. RR )
23 harmonicbnd 
 |-  ( ( |_ ` A ) e. NN -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) e. ( gamma [,] 1 ) )
24 6 23 syl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) e. ( gamma [,] 1 ) )
25 emre 
 |-  gamma e. RR
26 25 13 elicc2i 
 |-  ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) e. ( gamma [,] 1 ) <-> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) e. RR /\ gamma <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) /\ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) <_ 1 ) )
27 26 simp3bi 
 |-  ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) e. ( gamma [,] 1 ) -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) <_ 1 )
28 24 27 syl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) <_ 1 )
29 5 8 14 lesubadd2d 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( |_ ` A ) ) ) <_ 1 <-> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) <_ ( ( log ` ( |_ ` A ) ) + 1 ) ) )
30 28 29 mpbid 
 |-  ( ( A e. RR /\ 1 <_ A ) -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) <_ ( ( log ` ( |_ ` A ) ) + 1 ) )
31 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
32 31 adantr 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( |_ ` A ) <_ A )
33 7 19 logled 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( ( |_ ` A ) <_ A <-> ( log ` ( |_ ` A ) ) <_ ( log ` A ) ) )
34 32 33 mpbid 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( log ` ( |_ ` A ) ) <_ ( log ` A ) )
35 8 20 14 34 leadd1dd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( ( log ` ( |_ ` A ) ) + 1 ) <_ ( ( log ` A ) + 1 ) )
36 5 10 22 30 35 letrd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) <_ ( ( log ` A ) + 1 ) )