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 ⊢ A ∈ ℝ ∧ 1 ≤ A → ∑ m = 1 A 1 m ≤ log ⁡ A + 1

Proof

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