Step | Hyp | Ref
| Expression |
1 | | rpcn 12149 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
2 | 1 | times2d 11626 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 2) =
(𝐴 + 𝐴)) |
3 | 2 | oveq2d 6938 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
(𝐴 · 2)) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
4 | | relogcl 24759 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
5 | 4 | recnd 10405 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
6 | | 2cnd 11453 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℂ) |
7 | 1, 5, 6 | subdid 10831 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= ((𝐴 ·
(log‘𝐴)) −
(𝐴 ·
2))) |
8 | | rpre 12145 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
9 | 8, 4 | remulcld 10407 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℝ) |
10 | 9 | recnd 10405 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℂ) |
11 | 10, 1, 1 | subsub4d 10765 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
12 | 3, 7, 11 | 3eqtr4d 2823 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴)) |
13 | 9, 8 | resubcld 10803 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ∈
ℝ) |
14 | | fzfid 13091 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
15 | | fzfid 13091 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (1...𝑛) ∈
Fin) |
16 | | elfznn 12687 |
. . . . . . . 8
⊢ (𝑑 ∈ (1...𝑛) → 𝑑 ∈ ℕ) |
17 | 16 | adantl 475 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → 𝑑 ∈ ℕ) |
18 | 17 | nnrecred 11426 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℝ) |
19 | 15, 18 | fsumrecl 14872 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ∈
ℝ) |
20 | 14, 19 | fsumrecl 14872 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ∈ ℝ) |
21 | | rprege0 12154 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
22 | | flge0nn0 12940 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
24 | | faccl 13388 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℕ0 → (!‘(⌊‘𝐴)) ∈ ℕ) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈ ℕ) |
26 | 25 | nnrpd 12179 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈
ℝ+) |
27 | 26 | relogcld 24806 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
28 | 27, 8 | readdcld 10406 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + 𝐴) ∈ ℝ) |
29 | | elfznn 12687 |
. . . . . . . . . 10
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℕ) |
30 | 29 | adantl 475 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℕ) |
31 | 30 | nnrecred 11426 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ) |
32 | 14, 31 | fsumrecl 14872 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ∈
ℝ) |
33 | 8, 32 | remulcld 10407 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) ∈
ℝ) |
34 | | reflcl 12916 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
35 | 8, 34 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
36 | 33, 35 | resubcld 10803 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ∈
ℝ) |
37 | | harmoniclbnd 25187 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) |
38 | | rpregt0 12153 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
39 | | lemul2 11230 |
. . . . . . . 8
⊢
(((log‘𝐴)
∈ ℝ ∧ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((log‘𝐴) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))) |
40 | 4, 32, 38, 39 | syl3anc 1439 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))) |
41 | 37, 40 | mpbid 224 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑))) |
42 | | flle 12919 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
43 | 8, 42 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
44 | 9, 35, 33, 8, 41, 43 | le2subd 10995 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴))) |
45 | 29 | nnrecred 11426 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (1 / 𝑑) ∈
ℝ) |
46 | | remulcl 10357 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (1 / 𝑑) ∈ ℝ) → (𝐴 · (1 / 𝑑)) ∈
ℝ) |
47 | 8, 45, 46 | syl2an 589 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℝ) |
48 | | peano2rem 10690 |
. . . . . . . 8
⊢ ((𝐴 · (1 / 𝑑)) ∈ ℝ → ((𝐴 · (1 / 𝑑)) − 1) ∈
ℝ) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ∈
ℝ) |
50 | | fzfid 13091 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑...(⌊‘𝐴)) ∈ Fin) |
51 | 31 | adantr 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) → (1 / 𝑑) ∈
ℝ) |
52 | 50, 51 | fsumrecl 14872 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ) |
53 | 8 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
54 | 53, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℝ) |
55 | | peano2re 10549 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
57 | 30 | nnred 11391 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ) |
58 | | fllep1 12921 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
59 | 8, 58 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
60 | 59 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
61 | 53, 56, 57, 60 | lesub1dd 10991 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑)) |
62 | 53, 57 | resubcld 10803 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ∈
ℝ) |
63 | 56, 57 | resubcld 10803 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) ∈
ℝ) |
64 | 30 | nnrpd 12179 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ+) |
65 | 64 | rpreccld 12191 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ+) |
66 | 62, 63, 65 | lemul1d 12224 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑) ↔ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))) |
67 | 61, 66 | mpbid 224 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
68 | 1 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℂ) |
69 | 30 | nncnd 11392 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℂ) |
70 | 31 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℂ) |
71 | 68, 69, 70 | subdird 10832 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) = ((𝐴 · (1 / 𝑑)) − (𝑑 · (1 / 𝑑)))) |
72 | 30 | nnne0d 11425 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ≠
0) |
73 | 69, 72 | recidd 11146 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑 · (1 /
𝑑)) = 1) |
74 | 73 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − (𝑑 · (1 / 𝑑))) = ((𝐴 · (1 / 𝑑)) − 1)) |
75 | 71, 74 | eqtr2d 2814 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) = ((𝐴 − 𝑑) · (1 / 𝑑))) |
76 | | fsumconst 14926 |
. . . . . . . . . 10
⊢ (((𝑑...(⌊‘𝐴)) ∈ Fin ∧ (1 / 𝑑) ∈ ℂ) →
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
77 | 50, 70, 76 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
78 | | elfzuz3 12656 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
79 | 78 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
80 | | hashfz 13528 |
. . . . . . . . . . . 12
⊢
((⌊‘𝐴)
∈ (ℤ≥‘𝑑) → (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
82 | 35 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
83 | 82 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℂ) |
84 | | 1cnd 10371 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
85 | 83, 84, 69 | addsubd 10755 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) =
(((⌊‘𝐴) −
𝑑) + 1)) |
86 | 81, 85 | eqtr4d 2816 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) + 1) − 𝑑)) |
87 | 86 | oveq1d 6937 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
88 | 77, 87 | eqtrd 2813 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
89 | 67, 75, 88 | 3brtr4d 4918 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ≤
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
90 | 14, 49, 52, 89 | fsumle 14935 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
91 | 14, 1, 70 | fsummulc2 14920 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) = Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑))) |
92 | | ax-1cn 10330 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
93 | | fsumconst 14926 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
94 | 14, 92, 93 | sylancl 580 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
95 | | hashfz1 13451 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℕ0 → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
96 | 23, 95 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
97 | 96 | oveq1d 6937 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((♯‘(1...(⌊‘𝐴))) · 1) = ((⌊‘𝐴) · 1)) |
98 | 82 | mulid1d 10394 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴)
· 1) = (⌊‘𝐴)) |
99 | 94, 97, 98 | 3eqtrrd 2818 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑑 ∈
(1...(⌊‘𝐴))1) |
100 | 91, 99 | oveq12d 6940 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
(Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
101 | 47 | recnd 10405 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℂ) |
102 | 14, 101, 84 | fsumsub 14924 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) = (Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
103 | 100, 102 | eqtr4d 2816 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1)) |
104 | | eqid 2777 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
105 | 104 | uztrn2 12010 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) → 𝑛 ∈
(ℤ≥‘1)) |
106 | 105 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → 𝑛 ∈
(ℤ≥‘1)) |
107 | 106 | biantrurd 528 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
108 | | uzss 12013 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑑) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑑)) |
109 | 108 | ad2antll 719 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) →
(ℤ≥‘𝑛) ⊆ (ℤ≥‘𝑑)) |
110 | 109 | sseld 3819 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) → (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
111 | 110 | pm4.71rd 558 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
112 | 107, 111 | bitr3d 273 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
113 | 112 | pm5.32da 574 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
114 | | ancom 454 |
. . . . . . . . 9
⊢ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
115 | | an4 646 |
. . . . . . . . 9
⊢ (((𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
116 | 113, 114,
115 | 3bitr4g 306 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
117 | | elfzuzb 12653 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛))) |
118 | | elfzuzb 12653 |
. . . . . . . . 9
⊢ (𝑑 ∈ (1...𝑛) ↔ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) |
119 | 117, 118 | anbi12i 620 |
. . . . . . . 8
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)))) |
120 | | elfzuzb 12653 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
121 | | elfzuzb 12653 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑑...(⌊‘𝐴)) ↔ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) |
122 | 120, 121 | anbi12i 620 |
. . . . . . . 8
⊢ ((𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
123 | 116, 119,
122 | 3bitr4g 306 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))))) |
124 | 18 | recnd 10405 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℂ) |
125 | 124 | anasss 460 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛))) → (1 / 𝑑) ∈
ℂ) |
126 | 14, 14, 15, 123, 125 | fsumcom2 14910 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
127 | 90, 103, 126 | 3brtr4d 4918 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ≤
Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
128 | 13, 36, 20, 44, 127 | letrd 10533 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
129 | 27, 35 | readdcld 10406 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ∈ ℝ) |
130 | | elfznn 12687 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
131 | 130 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
132 | 131 | nnrpd 12179 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
133 | 132 | relogcld 24806 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
134 | | peano2re 10549 |
. . . . . . . 8
⊢
((log‘𝑛)
∈ ℝ → ((log‘𝑛) + 1) ∈ ℝ) |
135 | 133, 134 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((log‘𝑛) + 1)
∈ ℝ) |
136 | | nnz 11751 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
137 | | flid 12928 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(⌊‘𝑛) = 𝑛) |
139 | 138 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
140 | 139 | sumeq1d 14839 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) = Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
141 | | nnre 11382 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
142 | | nnge1 11404 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ≤
𝑛) |
143 | | harmonicubnd 25188 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ 1 ≤
𝑛) → Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
144 | 141, 142,
143 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
145 | 140, 144 | eqbrtrrd 4910 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
146 | 131, 145 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
147 | 14, 19, 135, 146 | fsumle 14935 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1)) |
148 | 133 | recnd 10405 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℂ) |
149 | | 1cnd 10371 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
150 | 14, 148, 149 | fsumadd 14877 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
151 | | logfac 24784 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
152 | 23, 151 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
153 | | fsumconst 14926 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
154 | 14, 92, 153 | sylancl 580 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
155 | 154, 97, 98 | 3eqtrrd 2818 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑛 ∈
(1...(⌊‘𝐴))1) |
156 | 152, 155 | oveq12d 6940 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
157 | 150, 156 | eqtr4d 2816 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) =
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
158 | 147, 157 | breqtrd 4912 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
159 | 35, 8, 27, 43 | leadd2dd 10990 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
160 | 20, 129, 28, 158, 159 | letrd 10533 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
161 | 13, 20, 28, 128, 160 | letrd 10533 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
162 | 13, 8, 27 | lesubaddd 10972 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴))) ↔ ((𝐴 · (log‘𝐴)) − 𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴))) |
163 | 161, 162 | mpbird 249 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴)))) |
164 | 12, 163 | eqbrtrd 4908 |
1
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
≤ (log‘(!‘(⌊‘𝐴)))) |