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 ) ) [,] γ ) )