This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
2 1 sumeq1d ⊢ ( 𝑛 = 𝑁 → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) )
3 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( log ‘ ( 𝑛 + 1 ) ) = ( log ‘ ( 𝑁 + 1 ) ) )
4 2 3 oveq12d ⊢ ( 𝑛 = 𝑁 → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) )
5 4 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ↔ ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ) )
6 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
7 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
8 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
9 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 1 / 𝑘 ) = ( 1 / 𝑛 ) )
10 9 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 1 + ( 1 / 𝑘 ) ) = ( 1 + ( 1 / 𝑛 ) ) )
11 10 fveq2d ⊢ ( 𝑘 = 𝑛 → ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) = ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) )
12 9 11 oveq12d ⊢ ( 𝑘 = 𝑛 → ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) = ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
13 12 cbvmptv ⊢ ( 𝑘 ∈ ℕ ↦ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 1 / 𝑛 ) − ( log ‘ ( 1 + ( 1 / 𝑛 ) ) ) ) )
14 6 7 8 13 emcllem7 ⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ∧ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) ) : ℕ ⟶ ( γ [,] 1 ) ∧ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ) : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
15 14 simp3i ⊢ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ) : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ )
16 7 fmpt ⊢ ( ∀ 𝑛 ∈ ℕ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) ↔ ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ) : ℕ ⟶ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
17 15 16 mpbir ⊢ ∀ 𝑛 ∈ ℕ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ )
18 5 17 vtoclri ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )