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 / 𝑚 ) )