Metamath Proof Explorer

Theorem harmoniclbnd

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

Ref Expression
Assertion harmoniclbnd ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) )

Proof

Step Hyp Ref Expression
1 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
2 rprege0 ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
3 flge0nn0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )
4 2 3 syl ⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )
5 nn0p1nn ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℕ )
6 4 5 syl ⊢ ( 𝐴 ∈ ℝ+ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℕ )
7 6 nnrpd ⊢ ( 𝐴 ∈ ℝ+ → ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ+ )
8 relogcl ⊢ ( ( ( ⌊ ‘ 𝐴 ) + 1 ) ∈ ℝ+ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
9 7 8 syl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
10 fzfid ⊢ ( 𝐴 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
11 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ )
12 11 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ )
13 12 nnrecred ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
14 10 13 fsumrecl ⊢ ( 𝐴 ∈ ℝ+ → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℝ )
15 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
16 fllep1 ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
17 15 16 syl ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) )
18 id ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ+ )
19 18 7 logled ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ≤ ( ( ⌊ ‘ 𝐴 ) + 1 ) ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
20 17 19 mpbid ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) )
21 harmonicbnd3 ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) )
22 4 21 syl ⊢ ( 𝐴 ∈ ℝ+ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) )
23 0re ⊢ 0 ∈ ℝ
24 emre ⊢ γ ∈ ℝ
25 23 24 elicc2i ⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) ↔ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ ∧ 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∧ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ≤ γ ) )
26 25 simp2bi ⊢ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ∈ ( 0 [,] γ ) → 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
27 22 26 syl ⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) )
28 14 9 subge0d ⊢ ( 𝐴 ∈ ℝ+ → ( 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ) ↔ ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ) )
29 27 28 mpbid ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( ( ⌊ ‘ 𝐴 ) + 1 ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) )
30 1 9 14 20 29 letrd ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) )