Metamath Proof Explorer

Theorem emcl

Description: Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Assertion emcl 
|- gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 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 ) ) ) )
3 eqid 
 |-  ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) ) = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )
4 oveq2 
 |-  ( k = n -> ( 1 / k ) = ( 1 / n ) )
5 4 oveq2d 
 |-  ( k = n -> ( 1 + ( 1 / k ) ) = ( 1 + ( 1 / n ) ) )
6 5 fveq2d 
 |-  ( k = n -> ( log ` ( 1 + ( 1 / k ) ) ) = ( log ` ( 1 + ( 1 / n ) ) ) )
7 4 6 oveq12d 
 |-  ( k = n -> ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) = ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
8 7 cbvmptv 
 |-  ( k e. NN |-> ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) ) = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )
9 1 2 3 8 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 ) )
10 9 simp1i 
 |-  gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 )