Proof of Theorem harmonicbnd4
| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
| 2 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝐴))
→ 𝑚 ∈
ℕ) |
| 3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ 𝑚 ∈
ℕ) |
| 4 | 3 | nnrecred 12317 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑚) ∈
ℝ) |
| 5 | 1, 4 | fsumrecl 15770 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) ∈
ℝ) |
| 6 | 5 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) ∈
ℂ) |
| 7 | | relogcl 26617 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
| 8 | 7 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
| 9 | | emre 27049 |
. . . . . 6
⊢ γ
∈ ℝ |
| 10 | 9 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ γ ∈ ℝ) |
| 11 | 10 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ γ ∈ ℂ) |
| 12 | 6, 8, 11 | subsub4d 11651 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − γ) =
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ))) |
| 13 | 12 | fveq2d 6910 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) =
(abs‘(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) +
γ)))) |
| 14 | | rpreccl 13061 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℝ+) |
| 15 | 14 | rpred 13077 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℝ) |
| 16 | | resubcl 11573 |
. . . . 5
⊢ ((γ
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (γ − (1
/ 𝐴)) ∈
ℝ) |
| 17 | 9, 15, 16 | sylancr 587 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ∈ ℝ) |
| 18 | | rprege0 13050 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
| 19 | | flge0nn0 13860 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
| 20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
| 21 | | nn0p1nn 12565 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℕ0 → ((⌊‘𝐴) + 1) ∈ ℕ) |
| 22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℕ) |
| 23 | 22 | nnrpd 13075 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℝ+) |
| 24 | | relogcl 26617 |
. . . . . 6
⊢
(((⌊‘𝐴)
+ 1) ∈ ℝ+ → (log‘((⌊‘𝐴) + 1)) ∈
ℝ) |
| 25 | 23, 24 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ∈ ℝ) |
| 26 | 5, 25 | resubcld 11691 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ) |
| 27 | 5, 7 | resubcld 11691 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ∈
ℝ) |
| 28 | 22 | nnrecred 12317 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ∈ ℝ) |
| 29 | | fzfid 14014 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (1...((⌊‘𝐴) + 1)) ∈ Fin) |
| 30 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...((⌊‘𝐴) +
1)) → 𝑚 ∈
ℕ) |
| 31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → 𝑚 ∈
ℕ) |
| 32 | 31 | nnrecred 12317 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → (1 / 𝑚) ∈
ℝ) |
| 33 | 29, 32 | fsumrecl 15770 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) ∈
ℝ) |
| 34 | 33, 25 | resubcld 11691 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ) |
| 35 | | harmonicbnd 27047 |
. . . . . . . 8
⊢
(((⌊‘𝐴)
+ 1) ∈ ℕ → (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈
(γ[,]1)) |
| 36 | 22, 35 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈
(γ[,]1)) |
| 37 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 38 | 9, 37 | elicc2i 13453 |
. . . . . . . 8
⊢
((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1) ↔
((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ γ ≤
(Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤
1)) |
| 39 | 38 | simp2bi 1147 |
. . . . . . 7
⊢
((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (γ[,]1) → γ
≤ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
| 40 | 36, 39 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ γ ≤ (Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
| 41 | | rpre 13043 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 42 | | fllep1 13841 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
| 43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
| 44 | | rpregt0 13049 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
| 45 | 22 | nnred 12281 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
| 46 | 22 | nngt0d 12315 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ 0 < ((⌊‘𝐴) + 1)) |
| 47 | | lerec 12151 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧
(((⌊‘𝐴) + 1)
∈ ℝ ∧ 0 < ((⌊‘𝐴) + 1))) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))) |
| 48 | 44, 45, 46, 47 | syl12anc 837 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ≤
((⌊‘𝐴) + 1)
↔ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴))) |
| 49 | 43, 48 | mpbid 232 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ≤ (1 / 𝐴)) |
| 50 | 10, 28, 34, 15, 40, 49 | le2subd 11883 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ ((Σ𝑚 ∈ (1...((⌊‘𝐴) + 1))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) − (1 /
((⌊‘𝐴) +
1)))) |
| 51 | 33 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) ∈
ℂ) |
| 52 | 25 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ∈ ℂ) |
| 53 | 28 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (1 / ((⌊‘𝐴) + 1)) ∈ ℂ) |
| 54 | 51, 52, 53 | sub32d 11652 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1)))
− (log‘((⌊‘𝐴) + 1)))) |
| 55 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 56 | 22, 55 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) +
1) ∈ (ℤ≥‘1)) |
| 57 | 32 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝐴) +
1))) → (1 / 𝑚) ∈
ℂ) |
| 58 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝐴) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝐴) + 1))) |
| 59 | 56, 57, 58 | fsumm1 15787 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) = (Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) + (1
/ ((⌊‘𝐴) +
1)))) |
| 60 | 20 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
| 61 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 62 | | pncan 11514 |
. . . . . . . . . . . . 13
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝐴) + 1) − 1) =
(⌊‘𝐴)) |
| 63 | 60, 61, 62 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) − 1) = (⌊‘𝐴)) |
| 64 | 63 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (1...(((⌊‘𝐴) + 1) − 1)) =
(1...(⌊‘𝐴))) |
| 65 | 64 | sumeq1d 15736 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) =
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) |
| 66 | 65 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(((⌊‘𝐴) +
1) − 1))(1 / 𝑚) + (1
/ ((⌊‘𝐴) + 1)))
= (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) +
1)))) |
| 67 | 59, 66 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) = (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) + (1 /
((⌊‘𝐴) +
1)))) |
| 68 | 6, 53, 67 | mvrraddd 11675 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1))) =
Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚)) |
| 69 | 68 | oveq1d 7446 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) − (1 /
((⌊‘𝐴) + 1)))
− (log‘((⌊‘𝐴) + 1))) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
| 70 | 54, 69 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...((⌊‘𝐴) +
1))(1 / 𝑚) −
(log‘((⌊‘𝐴) + 1))) − (1 / ((⌊‘𝐴) + 1))) = (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
| 71 | 50, 70 | breqtrd 5169 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1)))) |
| 72 | | logleb 26645 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ ((⌊‘𝐴) +
1) ∈ ℝ+) → (𝐴 ≤ ((⌊‘𝐴) + 1) ↔ (log‘𝐴) ≤ (log‘((⌊‘𝐴) + 1)))) |
| 73 | 23, 72 | mpdan 687 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ≤
((⌊‘𝐴) + 1)
↔ (log‘𝐴) ≤
(log‘((⌊‘𝐴) + 1)))) |
| 74 | 43, 73 | mpbid 232 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
(log‘((⌊‘𝐴) + 1))) |
| 75 | 7, 25, 5, 74 | lesub2dd 11880 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴))) |
| 76 | 17, 26, 27, 71, 75 | letrd 11418 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (γ − (1 / 𝐴)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴))) |
| 77 | 27, 15 | resubcld 11691 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ∈
ℝ) |
| 78 | 15 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (1 / 𝐴) ∈
ℂ) |
| 79 | 6, 8, 78 | subsub4d 11651 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) = (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + (1 / 𝐴)))) |
| 80 | 7, 15 | readdcld 11290 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) + (1
/ 𝐴)) ∈
ℝ) |
| 81 | | id 22 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ+) |
| 82 | 23, 81 | relogdivd 26668 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) = ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴))) |
| 83 | | rerpdivcl 13065 |
. . . . . . . . . . . . 13
⊢
((((⌊‘𝐴)
+ 1) ∈ ℝ ∧ 𝐴
∈ ℝ+) → (((⌊‘𝐴) + 1) / 𝐴) ∈ ℝ) |
| 84 | 45, 83 | mpancom 688 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ∈
ℝ) |
| 85 | 37 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 1 ∈ ℝ) |
| 86 | 85, 15 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) ∈
ℝ) |
| 87 | 15 | reefcld 16124 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (exp‘(1 / 𝐴))
∈ ℝ) |
| 88 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ 1 ∈ ℂ) |
| 89 | | rpcnne0 13053 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℂ
∧ 𝐴 ≠
0)) |
| 90 | | divdir 11947 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝐴)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (((⌊‘𝐴) + 1) / 𝐴) = (((⌊‘𝐴) / 𝐴) + (1 / 𝐴))) |
| 91 | 60, 88, 89, 90 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) =
(((⌊‘𝐴) / 𝐴) + (1 / 𝐴))) |
| 92 | | reflcl 13836 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 93 | 41, 92 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
| 94 | | rerpdivcl 13065 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 𝐴
∈ ℝ+) → ((⌊‘𝐴) / 𝐴) ∈ ℝ) |
| 95 | 93, 94 | mpancom 688 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) /
𝐴) ∈
ℝ) |
| 96 | | flle 13839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
| 97 | 41, 96 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
| 98 | | rpcn 13045 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
| 99 | 98 | mulridd 11278 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 1) =
𝐴) |
| 100 | 97, 99 | breqtrrd 5171 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ (𝐴 ·
1)) |
| 101 | | ledivmul 12144 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (((⌊‘𝐴) / 𝐴) ≤ 1 ↔ (⌊‘𝐴) ≤ (𝐴 · 1))) |
| 102 | 93, 85, 44, 101 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
/ 𝐴) ≤ 1 ↔
(⌊‘𝐴) ≤
(𝐴 ·
1))) |
| 103 | 100, 102 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴) /
𝐴) ≤ 1) |
| 104 | 95, 85, 15, 103 | leadd1dd 11877 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
/ 𝐴) + (1 / 𝐴)) ≤ (1 + (1 / 𝐴))) |
| 105 | 91, 104 | eqbrtrd 5165 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ≤ (1 + (1 /
𝐴))) |
| 106 | | efgt1p 16151 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝐴) ∈
ℝ+ → (1 + (1 / 𝐴)) < (exp‘(1 / 𝐴))) |
| 107 | 14, 106 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) <
(exp‘(1 / 𝐴))) |
| 108 | 86, 87, 107 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (1 + (1 / 𝐴)) ≤
(exp‘(1 / 𝐴))) |
| 109 | 84, 86, 87, 105, 108 | letrd 11418 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ≤
(exp‘(1 / 𝐴))) |
| 110 | | rpdivcl 13060 |
. . . . . . . . . . . . 13
⊢
((((⌊‘𝐴)
+ 1) ∈ ℝ+ ∧ 𝐴 ∈ ℝ+) →
(((⌊‘𝐴) + 1) /
𝐴) ∈
ℝ+) |
| 111 | 23, 110 | mpancom 688 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (((⌊‘𝐴)
+ 1) / 𝐴) ∈
ℝ+) |
| 112 | 15 | rpefcld 16141 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ+
→ (exp‘(1 / 𝐴))
∈ ℝ+) |
| 113 | 111, 112 | logled 26669 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ ((((⌊‘𝐴)
+ 1) / 𝐴) ≤
(exp‘(1 / 𝐴)) ↔
(log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴))))) |
| 114 | 109, 113 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (log‘(exp‘(1 / 𝐴)))) |
| 115 | 15 | relogefd 26670 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (log‘(exp‘(1 / 𝐴))) = (1 / 𝐴)) |
| 116 | 114, 115 | breqtrd 5169 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (log‘(((⌊‘𝐴) + 1) / 𝐴)) ≤ (1 / 𝐴)) |
| 117 | 82, 116 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ ((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴)) |
| 118 | 25, 7, 15 | lesubadd2d 11862 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((log‘((⌊‘𝐴) + 1)) − (log‘𝐴)) ≤ (1 / 𝐴) ↔ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴)))) |
| 119 | 117, 118 | mpbid 232 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘((⌊‘𝐴) + 1)) ≤ ((log‘𝐴) + (1 / 𝐴))) |
| 120 | 25, 80, 5, 119 | lesub2dd 11880 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
((log‘𝐴) + (1 / 𝐴))) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
| 121 | 79, 120 | eqbrtrd 5165 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1)))) |
| 122 | | harmonicbnd3 27051 |
. . . . . . 7
⊢
((⌊‘𝐴)
∈ ℕ0 → (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ∈
(0[,]γ)) |
| 123 | 20, 122 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈
(0[,]γ)) |
| 124 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 125 | 124, 9 | elicc2i 13453 |
. . . . . . 7
⊢
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) ↔
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ ℝ ∧ 0 ≤
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∧ (Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘((⌊‘𝐴) + 1))) ≤
γ)) |
| 126 | 125 | simp3bi 1148 |
. . . . . 6
⊢
((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ∈ (0[,]γ) →
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ γ) |
| 127 | 123, 126 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) −
(log‘((⌊‘𝐴) + 1))) ≤ γ) |
| 128 | 77, 26, 10, 121, 127 | letrd 11418 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤
γ) |
| 129 | 27, 15, 10 | lesubaddd 11860 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (((Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) − (1 / 𝐴)) ≤ γ ↔
(Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴)))) |
| 130 | 128, 129 | mpbid 232 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))) |
| 131 | 27, 10, 15 | absdifled 15473 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴) ↔ ((γ − (1 /
𝐴)) ≤ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ∧ (Σ𝑚 ∈
(1...(⌊‘𝐴))(1 /
𝑚) − (log‘𝐴)) ≤ (γ + (1 / 𝐴))))) |
| 132 | 76, 130, 131 | mpbir2and 713 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − (log‘𝐴)) − γ)) ≤ (1 / 𝐴)) |
| 133 | 13, 132 | eqbrtrrd 5167 |
1
⊢ (𝐴 ∈ ℝ+
→ (abs‘(Σ𝑚
∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴)) |