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 = 1 N 1 m − 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 = 1 n 1 m = ∑ m = 1 N 1 m
3 fvoveq1 ⊢ n = N → log ⁡ n + 1 = log ⁡ N + 1
4 2 3 oveq12d ⊢ n = N → ∑ m = 1 n 1 m − log ⁡ n + 1 = ∑ m = 1 N 1 m − log ⁡ N + 1
5 4 eleq1d ⊢ n = N → ∑ m = 1 n 1 m − log ⁡ n + 1 ∈ 1 − log ⁡ 2 γ ↔ ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 1 − log ⁡ 2 γ
6 eqid ⊢ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n
7 eqid ⊢ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1 = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1
8 eqid ⊢ n ∈ ℕ ⟼ log ⁡ 1 + 1 n = n ∈ ℕ ⟼ log ⁡ 1 + 1 n
9 oveq2 ⊢ k = n → 1 k = 1 n
10 9 oveq2d ⊢ k = n → 1 + 1 k = 1 + 1 n
11 10 fveq2d ⊢ k = n → log ⁡ 1 + 1 k = log ⁡ 1 + 1 n
12 9 11 oveq12d ⊢ k = n → 1 k − log ⁡ 1 + 1 k = 1 n − log ⁡ 1 + 1 n
13 12 cbvmptv ⊢ k ∈ ℕ ⟼ 1 k − log ⁡ 1 + 1 k = n ∈ ℕ ⟼ 1 n − log ⁡ 1 + 1 n
14 6 7 8 13 emcllem7 ⊢ γ ∈ 1 − log ⁡ 2 1 ∧ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n : ℕ ⟶ γ 1 ∧ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1 : ℕ ⟶ 1 − log ⁡ 2 γ
15 14 simp3i ⊢ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1 : ℕ ⟶ 1 − log ⁡ 2 γ
16 7 fmpt ⊢ ∀ n ∈ ℕ ∑ m = 1 n 1 m − log ⁡ n + 1 ∈ 1 − log ⁡ 2 γ ↔ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1 : ℕ ⟶ 1 − log ⁡ 2 γ
17 15 16 mpbir ⊢ ∀ n ∈ ℕ ∑ m = 1 n 1 m − log ⁡ n + 1 ∈ 1 − log ⁡ 2 γ
18 5 17 vtoclri ⊢ N ∈ ℕ → ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 1 − log ⁡ 2 γ