Metamath Proof Explorer

Theorem harmonicbnd3

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

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

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 0re ⊢ 0 ∈ ℝ
3 emre ⊢ γ ∈ ℝ
4 2re ⊢ 2 ∈ ℝ
5 ere ⊢ e ∈ ℝ
6 egt2lt3 ⊢ 2 < e ∧ e < 3
7 6 simpli ⊢ 2 < e
8 4 5 7 ltleii ⊢ 2 ≤ e
9 2rp ⊢ 2 ∈ ℝ +
10 epr ⊢ e ∈ ℝ +
11 logleb ⊢ 2 ∈ ℝ + ∧ e ∈ ℝ + → 2 ≤ e ↔ log ⁡ 2 ≤ log ⁡ e
12 9 10 11 mp2an ⊢ 2 ≤ e ↔ log ⁡ 2 ≤ log ⁡ e
13 8 12 mpbi ⊢ log ⁡ 2 ≤ log ⁡ e
14 loge ⊢ log ⁡ e = 1
15 13 14 breqtri ⊢ log ⁡ 2 ≤ 1
16 1re ⊢ 1 ∈ ℝ
17 relogcl ⊢ 2 ∈ ℝ + → log ⁡ 2 ∈ ℝ
18 9 17 ax-mp ⊢ log ⁡ 2 ∈ ℝ
19 16 18 subge0i ⊢ 0 ≤ 1 − log ⁡ 2 ↔ log ⁡ 2 ≤ 1
20 15 19 mpbir ⊢ 0 ≤ 1 − log ⁡ 2
21 3 leidi ⊢ γ ≤ γ
22 iccss ⊢ 0 ∈ ℝ ∧ γ ∈ ℝ ∧ 0 ≤ 1 − log ⁡ 2 ∧ γ ≤ γ → 1 − log ⁡ 2 γ ⊆ 0 γ
23 2 3 20 21 22 mp4an ⊢ 1 − log ⁡ 2 γ ⊆ 0 γ
24 harmonicbnd2 ⊢ N ∈ ℕ → ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 1 − log ⁡ 2 γ
25 23 24 sselid ⊢ N ∈ ℕ → ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 0 γ
26 oveq2 ⊢ N = 0 → 1 … N = 1 … 0
27 fz10 ⊢ 1 … 0 = ∅
28 26 27 eqtrdi ⊢ N = 0 → 1 … N = ∅
29 28 sumeq1d ⊢ N = 0 → ∑ m = 1 N 1 m = ∑ m ∈ ∅ 1 m
30 sum0 ⊢ ∑ m ∈ ∅ 1 m = 0
31 29 30 eqtrdi ⊢ N = 0 → ∑ m = 1 N 1 m = 0
32 fv0p1e1 ⊢ N = 0 → log ⁡ N + 1 = log ⁡ 1
33 log1 ⊢ log ⁡ 1 = 0
34 32 33 eqtrdi ⊢ N = 0 → log ⁡ N + 1 = 0
35 31 34 oveq12d ⊢ N = 0 → ∑ m = 1 N 1 m − log ⁡ N + 1 = 0 − 0
36 0m0e0 ⊢ 0 − 0 = 0
37 35 36 eqtrdi ⊢ N = 0 → ∑ m = 1 N 1 m − log ⁡ N + 1 = 0
38 2 leidi ⊢ 0 ≤ 0
39 emgt0 ⊢ 0 < γ
40 2 3 39 ltleii ⊢ 0 ≤ γ
41 2 3 elicc2i ⊢ 0 ∈ 0 γ ↔ 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 ≤ γ
42 2 38 40 41 mpbir3an ⊢ 0 ∈ 0 γ
43 37 42 eqeltrdi ⊢ N = 0 → ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 0 γ
44 25 43 jaoi ⊢ N ∈ ℕ ∨ N = 0 → ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 0 γ
45 1 44 sylbi ⊢ N ∈ ℕ 0 → ∑ m = 1 N 1 m − log ⁡ N + 1 ∈ 0 γ