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 γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
2 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
3 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
4 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 1 / 𝑘 ) = ( 1 / 𝑛 ) )
5 4 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 1 + ( 1 / 𝑘 ) ) = ( 1 + ( 1 / 𝑛 ) ) )
6 5 fveq2d ⊢ ( 𝑘 = 𝑛 → ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) = ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
7 4 6 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) = ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
8 7 cbvmptv ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
9 1 2 3 8 emcllem7 ⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ∧ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) ) : ℕ ⟶ ( γ [,] 1 ) ∧ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ) : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
10 9 simp1i ⊢ γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 )