Metamath Proof Explorer

Theorem harmonicbnd2

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

Ref Expression
Assertion harmonicbnd2 
|- ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
2 1 sumeq1d 
 |-  ( n = N -> sum_ m e. ( 1 ... n ) ( 1 / m ) = sum_ m e. ( 1 ... N ) ( 1 / m ) )
3 fvoveq1 
 |-  ( n = N -> ( log ` ( n + 1 ) ) = ( log ` ( N + 1 ) ) )
4 2 3 oveq12d 
 |-  ( n = N -> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) = ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) )
5 4 eleq1d 
 |-  ( n = N -> ( ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) <-> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) ) )
6 eqid 
 |-  ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) ) = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )
7 eqid 
 |-  ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) ) = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )
8 eqid 
 |-  ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) ) = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )
9 oveq2 
 |-  ( k = n -> ( 1 / k ) = ( 1 / n ) )
10 9 oveq2d 
 |-  ( k = n -> ( 1 + ( 1 / k ) ) = ( 1 + ( 1 / n ) ) )
11 10 fveq2d 
 |-  ( k = n -> ( log ` ( 1 + ( 1 / k ) ) ) = ( log ` ( 1 + ( 1 / n ) ) ) )
12 9 11 oveq12d 
 |-  ( k = n -> ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) = ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
13 12 cbvmptv 
 |-  ( k e. NN |-> ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) ) = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
14 6 7 8 13 emcllem7 
 |-  ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) /\ ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) ) : NN --> ( gamma [,] 1 ) /\ ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) ) : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
15 14 simp3i 
 |-  ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) ) : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma )
16 7 fmpt 
 |-  ( A. n e. NN ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) <-> ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) ) : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
17 15 16 mpbir 
 |-  A. n e. NN ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma )
18 5 17 vtoclri 
 |-  ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) )