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