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 ( 𝑁 ∈ ℕ0 → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( 0 [,] γ ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 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 ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( ( 1 − ( log ‘ 2 ) ) [,] γ ) )
25 23 24 sseldi ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( 0 [,] γ ) )
26 oveq2 ⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ( 1 ... 0 ) )
27 fz10 ⊢ ( 1 ... 0 ) = ∅
28 26 27 eqtrdi ⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ∅ )
29 28 sumeq1d ⊢ ( 𝑁 = 0 → Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) = Σ 𝑚 ∈ ∅ ( 1 / 𝑚 ) )
30 sum0 ⊢ Σ 𝑚 ∈ ∅ ( 1 / 𝑚 ) = 0
31 29 30 eqtrdi ⊢ ( 𝑁 = 0 → Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) = 0 )
32 fv0p1e1 ⊢ ( 𝑁 = 0 → ( log ‘ ( 𝑁 + 1 ) ) = ( log ‘ 1 ) )
33 log1 ⊢ ( log ‘ 1 ) = 0
34 32 33 eqtrdi ⊢ ( 𝑁 = 0 → ( log ‘ ( 𝑁 + 1 ) ) = 0 )
35 31 34 oveq12d ⊢ ( 𝑁 = 0 → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) = ( 0 − 0 ) )
36 0m0e0 ⊢ ( 0 − 0 ) = 0
37 35 36 eqtrdi ⊢ ( 𝑁 = 0 → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 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 ⊢ ( 𝑁 = 0 → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( 0 [,] γ ) )
44 25 43 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( 0 [,] γ ) )
45 1 44 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( Σ 𝑚 ∈ ( 1 ... 𝑁 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑁 + 1 ) ) ) ∈ ( 0 [,] γ ) )