Metamath Proof Explorer


Theorem harmonicubnd

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

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

Proof

Step Hyp Ref Expression
1 fzfid ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
2 elfznn ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ )
3 2 adantl ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ )
4 3 nnrecred ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
5 1 4 fsumrecl ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℝ )
6 flge1nn ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
7 6 nnrpd ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ+ )
8 7 relogcld ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ )
9 peano2re ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) ∈ ℝ → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ∈ ℝ )
10 8 9 syl ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ∈ ℝ )
11 simpl ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
12 0red ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ∈ ℝ )
13 1re 1 ∈ ℝ
14 13 a1i ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ∈ ℝ )
15 0lt1 0 < 1
16 15 a1i ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 1 )
17 simpr ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 )
18 12 14 11 16 17 ltletrd ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 𝐴 )
19 11 18 elrpd ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
20 19 relogcld ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ )
21 peano2re ( ( log ‘ 𝐴 ) ∈ ℝ → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ )
22 20 21 syl ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ )
23 harmonicbnd ( ( ⌊ ‘ 𝐴 ) ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) )
24 6 23 syl ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) )
25 emre γ ∈ ℝ
26 25 13 elicc2i ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) ↔ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ℝ ∧ γ ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∧ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 ) )
27 26 simp3bi ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ∈ ( γ [,] 1 ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 )
28 24 27 syl ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 )
29 5 8 14 lesubadd2d ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( log ‘ ( ⌊ ‘ 𝐴 ) ) ) ≤ 1 ↔ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ) )
30 28 29 mpbid ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) )
31 flle ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
32 31 adantr ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
33 7 19 logled ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ↔ ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) ) )
34 32 33 mpbid ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( log ‘ 𝐴 ) )
35 8 20 14 34 leadd1dd ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( log ‘ ( ⌊ ‘ 𝐴 ) ) + 1 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) )
36 5 10 22 30 35 letrd ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) )