Metamath Proof Explorer

Theorem harmonicbnd

Description: A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion harmonicbnd ⊢ N ∈ ℕ → ∑ m = 1 N 1 m − log ⁡ N ∈ γ 1

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 fveq2 ⊢ n = N → log ⁡ n = log ⁡ N
4 2 3 oveq12d ⊢ n = N → ∑ m = 1 n 1 m − log ⁡ n = ∑ m = 1 N 1 m − log ⁡ N
5 4 eleq1d ⊢ n = N → ∑ m = 1 n 1 m − log ⁡ n ∈ γ 1 ↔ ∑ m = 1 N 1 m − log ⁡ N ∈ γ 1
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 simp2i ⊢ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n : ℕ ⟶ γ 1
16 6 fmpt ⊢ ∀ n ∈ ℕ ∑ m = 1 n 1 m − log ⁡ n ∈ γ 1 ↔ n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n : ℕ ⟶ γ 1
17 15 16 mpbir ⊢ ∀ n ∈ ℕ ∑ m = 1 n 1 m − log ⁡ n ∈ γ 1
18 5 17 vtoclri ⊢ N ∈ ℕ → ∑ m = 1 N 1 m − log ⁡ N ∈ γ 1