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∈ℕ→∑m=1N1m−log⁡N+1∈1−log⁡2γ

Proof

Step Hyp Ref Expression
1 oveq2 ⊢n=N→1…n=1…N
2 1 sumeq1d ⊢n=N→∑m=1n1m=∑m=1N1m
3 fvoveq1 ⊢n=N→log⁡n+1=log⁡N+1
4 2 3 oveq12d ⊢n=N→∑m=1n1m−log⁡n+1=∑m=1N1m−log⁡N+1
5 4 eleq1d ⊢n=N→∑m=1n1m−log⁡n+1∈1−log⁡2γ↔∑m=1N1m−log⁡N+1∈1−log⁡2γ
6 eqid ⊢n∈ℕ⟼∑m=1n1m−log⁡n=n∈ℕ⟼∑m=1n1m−log⁡n
7 eqid ⊢n∈ℕ⟼∑m=1n1m−log⁡n+1=n∈ℕ⟼∑m=1n1m−log⁡n+1
8 eqid ⊢n∈ℕ⟼log⁡1+1n=n∈ℕ⟼log⁡1+1n
9 oveq2 ⊢k=n→1k=1n
10 9 oveq2d ⊢k=n→1+1k=1+1n
11 10 fveq2d ⊢k=n→log⁡1+1k=log⁡1+1n
12 9 11 oveq12d ⊢k=n→1k−log⁡1+1k=1n−log⁡1+1n
13 12 cbvmptv ⊢k∈ℕ⟼1k−log⁡1+1k=n∈ℕ⟼1n−log⁡1+1n
14 6 7 8 13 emcllem7 ⊢γ∈1−log⁡21∧n∈ℕ⟼∑m=1n1m−log⁡n:ℕ⟶γ1∧n∈ℕ⟼∑m=1n1m−log⁡n+1:ℕ⟶1−log⁡2γ
15 14 simp3i ⊢n∈ℕ⟼∑m=1n1m−log⁡n+1:ℕ⟶1−log⁡2γ
16 7 fmpt ⊢∀n∈ℕ∑m=1n1m−log⁡n+1∈1−log⁡2γ↔n∈ℕ⟼∑m=1n1m−log⁡n+1:ℕ⟶1−log⁡2γ
17 15 16 mpbir ⊢∀n∈ℕ∑m=1n1m−log⁡n+1∈1−log⁡2γ
18 5 17 vtoclri ⊢N∈ℕ→∑m=1N1m−log⁡N+1∈1−log⁡2γ