| Step | Hyp | Ref
| Expression |
| 1 | | rpcn 13045 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
| 2 | 1 | times2d 12510 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 2) =
(𝐴 + 𝐴)) |
| 3 | 2 | oveq2d 7447 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
(𝐴 · 2)) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
| 4 | | relogcl 26617 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
| 5 | 4 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
| 6 | | 2cnd 12344 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℂ) |
| 7 | 1, 5, 6 | subdid 11719 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= ((𝐴 ·
(log‘𝐴)) −
(𝐴 ·
2))) |
| 8 | | rpre 13043 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 9 | 8, 4 | remulcld 11291 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℝ) |
| 10 | 9 | recnd 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℂ) |
| 11 | 10, 1, 1 | subsub4d 11651 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
| 12 | 3, 7, 11 | 3eqtr4d 2787 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴)) |
| 13 | 9, 8 | resubcld 11691 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ∈
ℝ) |
| 14 | | fzfid 14014 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
| 15 | | fzfid 14014 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (1...𝑛) ∈
Fin) |
| 16 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑑 ∈ (1...𝑛) → 𝑑 ∈ ℕ) |
| 17 | 16 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → 𝑑 ∈ ℕ) |
| 18 | 17 | nnrecred 12317 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℝ) |
| 19 | 15, 18 | fsumrecl 15770 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ∈
ℝ) |
| 20 | 14, 19 | fsumrecl 15770 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ∈ ℝ) |
| 21 | | rprege0 13050 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
| 22 | | flge0nn0 13860 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
| 23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
| 24 | 23 | faccld 14323 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈ ℕ) |
| 25 | 24 | nnrpd 13075 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈
ℝ+) |
| 26 | 25 | relogcld 26665 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
| 27 | 26, 8 | readdcld 11290 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + 𝐴) ∈ ℝ) |
| 28 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℕ) |
| 29 | 28 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℕ) |
| 30 | 29 | nnrecred 12317 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ) |
| 31 | 14, 30 | fsumrecl 15770 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ∈
ℝ) |
| 32 | 8, 31 | remulcld 11291 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) ∈
ℝ) |
| 33 | | reflcl 13836 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
| 34 | 8, 33 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
| 35 | 32, 34 | resubcld 11691 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ∈
ℝ) |
| 36 | | harmoniclbnd 27052 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) |
| 37 | | rpregt0 13049 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
| 38 | | lemul2 12120 |
. . . . . . . 8
⊢
(((log‘𝐴)
∈ ℝ ∧ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((log‘𝐴) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))) |
| 39 | 4, 31, 37, 38 | syl3anc 1373 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))) |
| 40 | 36, 39 | mpbid 232 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑))) |
| 41 | | flle 13839 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
| 42 | 8, 41 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
| 43 | 9, 34, 32, 8, 40, 42 | le2subd 11883 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴))) |
| 44 | 28 | nnrecred 12317 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (1 / 𝑑) ∈
ℝ) |
| 45 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (1 / 𝑑) ∈ ℝ) → (𝐴 · (1 / 𝑑)) ∈
ℝ) |
| 46 | 8, 44, 45 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℝ) |
| 47 | | peano2rem 11576 |
. . . . . . . 8
⊢ ((𝐴 · (1 / 𝑑)) ∈ ℝ → ((𝐴 · (1 / 𝑑)) − 1) ∈
ℝ) |
| 48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ∈
ℝ) |
| 49 | | fzfid 14014 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑...(⌊‘𝐴)) ∈ Fin) |
| 50 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) → (1 / 𝑑) ∈
ℝ) |
| 51 | 49, 50 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ) |
| 52 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
| 53 | 52, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℝ) |
| 54 | | peano2re 11434 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
| 56 | 29 | nnred 12281 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ) |
| 57 | | fllep1 13841 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
| 58 | 8, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
| 59 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
| 60 | 52, 55, 56, 59 | lesub1dd 11879 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑)) |
| 61 | 52, 56 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ∈
ℝ) |
| 62 | 55, 56 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) ∈
ℝ) |
| 63 | 29 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ+) |
| 64 | 63 | rpreccld 13087 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ+) |
| 65 | 61, 62, 64 | lemul1d 13120 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑) ↔ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))) |
| 66 | 60, 65 | mpbid 232 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
| 67 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℂ) |
| 68 | 29 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℂ) |
| 69 | 30 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℂ) |
| 70 | 67, 68, 69 | subdird 11720 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) = ((𝐴 · (1 / 𝑑)) − (𝑑 · (1 / 𝑑)))) |
| 71 | 29 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ≠
0) |
| 72 | 68, 71 | recidd 12038 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑 · (1 /
𝑑)) = 1) |
| 73 | 72 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − (𝑑 · (1 / 𝑑))) = ((𝐴 · (1 / 𝑑)) − 1)) |
| 74 | 70, 73 | eqtr2d 2778 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) = ((𝐴 − 𝑑) · (1 / 𝑑))) |
| 75 | | fsumconst 15826 |
. . . . . . . . . 10
⊢ (((𝑑...(⌊‘𝐴)) ∈ Fin ∧ (1 / 𝑑) ∈ ℂ) →
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
| 76 | 49, 69, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
| 77 | | elfzuz3 13561 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
| 78 | 77 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
| 79 | | hashfz 14466 |
. . . . . . . . . . . 12
⊢
((⌊‘𝐴)
∈ (ℤ≥‘𝑑) → (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
| 80 | 78, 79 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
| 81 | 34 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℂ) |
| 83 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
| 84 | 82, 83, 68 | addsubd 11641 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) =
(((⌊‘𝐴) −
𝑑) + 1)) |
| 85 | 80, 84 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) + 1) − 𝑑)) |
| 86 | 85 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
| 87 | 76, 86 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
| 88 | 66, 74, 87 | 3brtr4d 5175 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ≤
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
| 89 | 14, 48, 51, 88 | fsumle 15835 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
| 90 | 14, 1, 69 | fsummulc2 15820 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) = Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑))) |
| 91 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 92 | | fsumconst 15826 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
| 93 | 14, 91, 92 | sylancl 586 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
| 94 | | hashfz1 14385 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℕ0 → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
| 95 | 23, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
| 96 | 95 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((♯‘(1...(⌊‘𝐴))) · 1) = ((⌊‘𝐴) · 1)) |
| 97 | 81 | mulridd 11278 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴)
· 1) = (⌊‘𝐴)) |
| 98 | 93, 96, 97 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑑 ∈
(1...(⌊‘𝐴))1) |
| 99 | 90, 98 | oveq12d 7449 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
(Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
| 100 | 46 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℂ) |
| 101 | 14, 100, 83 | fsumsub 15824 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) = (Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
| 102 | 99, 101 | eqtr4d 2780 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1)) |
| 103 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
| 104 | 103 | uztrn2 12897 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) → 𝑛 ∈
(ℤ≥‘1)) |
| 105 | 104 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → 𝑛 ∈
(ℤ≥‘1)) |
| 106 | 105 | biantrurd 532 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
| 107 | | uzss 12901 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑑) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑑)) |
| 108 | 107 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) →
(ℤ≥‘𝑛) ⊆ (ℤ≥‘𝑑)) |
| 109 | 108 | sseld 3982 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) → (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
| 110 | 109 | pm4.71rd 562 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
| 111 | 106, 110 | bitr3d 281 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
| 112 | 111 | pm5.32da 579 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
| 113 | | ancom 460 |
. . . . . . . . 9
⊢ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
| 114 | | an4 656 |
. . . . . . . . 9
⊢ (((𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
| 115 | 112, 113,
114 | 3bitr4g 314 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
| 116 | | elfzuzb 13558 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛))) |
| 117 | | elfzuzb 13558 |
. . . . . . . . 9
⊢ (𝑑 ∈ (1...𝑛) ↔ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) |
| 118 | 116, 117 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)))) |
| 119 | | elfzuzb 13558 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
| 120 | | elfzuzb 13558 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑑...(⌊‘𝐴)) ↔ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) |
| 121 | 119, 120 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
| 122 | 115, 118,
121 | 3bitr4g 314 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))))) |
| 123 | 18 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℂ) |
| 124 | 123 | anasss 466 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛))) → (1 / 𝑑) ∈
ℂ) |
| 125 | 14, 14, 15, 122, 124 | fsumcom2 15810 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
| 126 | 89, 102, 125 | 3brtr4d 5175 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ≤
Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
| 127 | 13, 35, 20, 43, 126 | letrd 11418 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
| 128 | 26, 34 | readdcld 11290 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ∈ ℝ) |
| 129 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
| 130 | 129 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
| 131 | 130 | nnrpd 13075 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
| 132 | 131 | relogcld 26665 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
| 133 | | peano2re 11434 |
. . . . . . . 8
⊢
((log‘𝑛)
∈ ℝ → ((log‘𝑛) + 1) ∈ ℝ) |
| 134 | 132, 133 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((log‘𝑛) + 1)
∈ ℝ) |
| 135 | | nnz 12634 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
| 136 | | flid 13848 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
| 137 | 135, 136 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(⌊‘𝑛) = 𝑛) |
| 138 | 137 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
| 139 | 138 | sumeq1d 15736 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) = Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
| 140 | | nnre 12273 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
| 141 | | nnge1 12294 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ≤
𝑛) |
| 142 | | harmonicubnd 27053 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ 1 ≤
𝑛) → Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
| 143 | 140, 141,
142 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
| 144 | 139, 143 | eqbrtrrd 5167 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
| 145 | 130, 144 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
| 146 | 14, 19, 134, 145 | fsumle 15835 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1)) |
| 147 | 132 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℂ) |
| 148 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
| 149 | 14, 147, 148 | fsumadd 15776 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
| 150 | | logfac 26643 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
| 151 | 23, 150 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
| 152 | | fsumconst 15826 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
| 153 | 14, 91, 152 | sylancl 586 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
| 154 | 153, 96, 97 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑛 ∈
(1...(⌊‘𝐴))1) |
| 155 | 151, 154 | oveq12d 7449 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
| 156 | 149, 155 | eqtr4d 2780 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) =
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
| 157 | 146, 156 | breqtrd 5169 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
| 158 | 34, 8, 26, 42 | leadd2dd 11878 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
| 159 | 20, 128, 27, 157, 158 | letrd 11418 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
| 160 | 13, 20, 27, 127, 159 | letrd 11418 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
| 161 | 13, 8, 26 | lesubaddd 11860 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴))) ↔ ((𝐴 · (log‘𝐴)) − 𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴))) |
| 162 | 160, 161 | mpbird 257 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴)))) |
| 163 | 12, 162 | eqbrtrd 5165 |
1
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
≤ (log‘(!‘(⌊‘𝐴)))) |