Step | Hyp | Ref
| Expression |
1 | | rpcn 11841 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
2 | 1 | times2d 11276 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 2) =
(𝐴 + 𝐴)) |
3 | 2 | oveq2d 6666 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
(𝐴 · 2)) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
4 | | relogcl 24322 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
5 | 4 | recnd 10068 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
6 | | 2cnd 11093 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℂ) |
7 | 1, 5, 6 | subdid 10486 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= ((𝐴 ·
(log‘𝐴)) −
(𝐴 ·
2))) |
8 | | rpre 11839 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
9 | 8, 4 | remulcld 10070 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℝ) |
10 | 9 | recnd 10068 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℂ) |
11 | 10, 1, 1 | subsub4d 10423 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
12 | 3, 7, 11 | 3eqtr4d 2666 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴)) |
13 | 9, 8 | resubcld 10458 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ∈
ℝ) |
14 | | fzfid 12772 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
15 | | fzfid 12772 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (1...𝑛) ∈
Fin) |
16 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑑 ∈ (1...𝑛) → 𝑑 ∈ ℕ) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → 𝑑 ∈ ℕ) |
18 | 17 | nnrecred 11066 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℝ) |
19 | 15, 18 | fsumrecl 14465 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ∈
ℝ) |
20 | 14, 19 | fsumrecl 14465 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ∈ ℝ) |
21 | | rprege0 11847 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
22 | | flge0nn0 12621 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
24 | | faccl 13070 |
. . . . . . . 8
⊢
((⌊‘𝐴)
∈ ℕ0 → (!‘(⌊‘𝐴)) ∈ ℕ) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈ ℕ) |
26 | 25 | nnrpd 11870 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈
ℝ+) |
27 | 26 | relogcld 24369 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
28 | 27, 8 | readdcld 10069 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + 𝐴) ∈ ℝ) |
29 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℕ) |
30 | 29 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℕ) |
31 | 30 | nnrecred 11066 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ) |
32 | 14, 31 | fsumrecl 14465 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ∈
ℝ) |
33 | 8, 32 | remulcld 10070 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) ∈
ℝ) |
34 | | reflcl 12597 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
35 | 8, 34 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
36 | 33, 35 | resubcld 10458 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ∈
ℝ) |
37 | | harmoniclbnd 24735 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) |
38 | | rpregt0 11846 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
39 | | lemul2 10876 |
. . . . . . . 8
⊢
(((log‘𝐴)
∈ ℝ ∧ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((log‘𝐴) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))) |
40 | 4, 32, 38, 39 | syl3anc 1326 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ↔ (𝐴 · (log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)))) |
41 | 37, 40 | mpbid 222 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑))) |
42 | | flle 12600 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
43 | 8, 42 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
44 | 9, 35, 33, 8, 41, 43 | le2subd 10647 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴))) |
45 | 29 | nnrecred 11066 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (1 / 𝑑) ∈
ℝ) |
46 | | remulcl 10021 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (1 / 𝑑) ∈ ℝ) → (𝐴 · (1 / 𝑑)) ∈
ℝ) |
47 | 8, 45, 46 | syl2an 494 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℝ) |
48 | | peano2rem 10348 |
. . . . . . . 8
⊢ ((𝐴 · (1 / 𝑑)) ∈ ℝ → ((𝐴 · (1 / 𝑑)) − 1) ∈
ℝ) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ∈
ℝ) |
50 | | fzfid 12772 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑...(⌊‘𝐴)) ∈ Fin) |
51 | 31 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) → (1 / 𝑑) ∈
ℝ) |
52 | 50, 51 | fsumrecl 14465 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ) |
53 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
54 | 53, 34 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℝ) |
55 | | peano2re 10209 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
57 | 30 | nnred 11035 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ) |
58 | | fllep1 12602 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
59 | 8, 58 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
60 | 59 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
61 | 53, 56, 57, 60 | lesub1dd 10643 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑)) |
62 | 53, 57 | resubcld 10458 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ∈
ℝ) |
63 | 56, 57 | resubcld 10458 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) ∈
ℝ) |
64 | 30 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ+) |
65 | 64 | rpreccld 11882 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ+) |
66 | 62, 63, 65 | lemul1d 11915 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑) ↔ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))) |
67 | 61, 66 | mpbid 222 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
68 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℂ) |
69 | 30 | nncnd 11036 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℂ) |
70 | 31 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℂ) |
71 | 68, 69, 70 | subdird 10487 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) = ((𝐴 · (1 / 𝑑)) − (𝑑 · (1 / 𝑑)))) |
72 | 30 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ≠
0) |
73 | 69, 72 | recidd 10796 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑 · (1 /
𝑑)) = 1) |
74 | 73 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − (𝑑 · (1 / 𝑑))) = ((𝐴 · (1 / 𝑑)) − 1)) |
75 | 71, 74 | eqtr2d 2657 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) = ((𝐴 − 𝑑) · (1 / 𝑑))) |
76 | | fsumconst 14522 |
. . . . . . . . . 10
⊢ (((𝑑...(⌊‘𝐴)) ∈ Fin ∧ (1 / 𝑑) ∈ ℂ) →
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((#‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
77 | 50, 70, 76 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((#‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
78 | | elfzuz3 12339 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
79 | 78 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
80 | | hashfz 13214 |
. . . . . . . . . . . 12
⊢
((⌊‘𝐴)
∈ (ℤ≥‘𝑑) → (#‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (#‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
82 | 35 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
83 | 82 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℂ) |
84 | | 1cnd 10056 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
85 | 83, 84, 69 | addsubd 10413 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) =
(((⌊‘𝐴) −
𝑑) + 1)) |
86 | 81, 85 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (#‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) + 1) − 𝑑)) |
87 | 86 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((#‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
88 | 77, 87 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
89 | 67, 75, 88 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ≤
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
90 | 14, 49, 52, 89 | fsumle 14531 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
91 | 14, 1, 70 | fsummulc2 14516 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) = Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑))) |
92 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
93 | | fsumconst 14522 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((#‘(1...(⌊‘𝐴))) · 1)) |
94 | 14, 92, 93 | sylancl 694 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((#‘(1...(⌊‘𝐴))) · 1)) |
95 | | hashfz1 13134 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℕ0 → (#‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
96 | 23, 95 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (#‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
97 | 96 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((#‘(1...(⌊‘𝐴))) · 1) = ((⌊‘𝐴) · 1)) |
98 | 82 | mulid1d 10057 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴)
· 1) = (⌊‘𝐴)) |
99 | 94, 97, 98 | 3eqtrrd 2661 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑑 ∈
(1...(⌊‘𝐴))1) |
100 | 91, 99 | oveq12d 6668 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
(Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
101 | 47 | recnd 10068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℂ) |
102 | 14, 101, 84 | fsumsub 14520 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) = (Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
103 | 100, 102 | eqtr4d 2659 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1)) |
104 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
105 | 104 | uztrn2 11705 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) → 𝑛 ∈
(ℤ≥‘1)) |
106 | 105 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → 𝑛 ∈
(ℤ≥‘1)) |
107 | 106 | biantrurd 529 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
108 | | uzss 11708 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑑) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑑)) |
109 | 108 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) →
(ℤ≥‘𝑛) ⊆ (ℤ≥‘𝑑)) |
110 | 109 | sseld 3602 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) → (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
111 | 110 | pm4.71rd 667 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
112 | 107, 111 | bitr3d 270 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
113 | 112 | pm5.32da 673 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
114 | | ancom 466 |
. . . . . . . . 9
⊢ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
115 | | an4 865 |
. . . . . . . . 9
⊢ (((𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
116 | 113, 114,
115 | 3bitr4g 303 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
117 | | elfzuzb 12336 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛))) |
118 | | elfzuzb 12336 |
. . . . . . . . 9
⊢ (𝑑 ∈ (1...𝑛) ↔ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) |
119 | 117, 118 | anbi12i 733 |
. . . . . . . 8
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)))) |
120 | | elfzuzb 12336 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
121 | | elfzuzb 12336 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑑...(⌊‘𝐴)) ↔ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) |
122 | 120, 121 | anbi12i 733 |
. . . . . . . 8
⊢ ((𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
123 | 116, 119,
122 | 3bitr4g 303 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))))) |
124 | 18 | recnd 10068 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℂ) |
125 | 124 | anasss 679 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛))) → (1 / 𝑑) ∈
ℂ) |
126 | 14, 14, 15, 123, 125 | fsumcom2 14505 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
127 | 90, 103, 126 | 3brtr4d 4685 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ≤
Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
128 | 13, 36, 20, 44, 127 | letrd 10194 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
129 | 27, 35 | readdcld 10069 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ∈ ℝ) |
130 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
131 | 130 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
132 | 131 | nnrpd 11870 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
133 | 132 | relogcld 24369 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
134 | | peano2re 10209 |
. . . . . . . 8
⊢
((log‘𝑛)
∈ ℝ → ((log‘𝑛) + 1) ∈ ℝ) |
135 | 133, 134 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((log‘𝑛) + 1)
∈ ℝ) |
136 | | nnz 11399 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
137 | | flid 12609 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(⌊‘𝑛) = 𝑛) |
139 | 138 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
140 | 139 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) = Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
141 | | nnre 11027 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
142 | | nnge1 11046 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ≤
𝑛) |
143 | | harmonicubnd 24736 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ 1 ≤
𝑛) → Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
144 | 141, 142,
143 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
145 | 140, 144 | eqbrtrrd 4677 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
146 | 131, 145 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
147 | 14, 19, 135, 146 | fsumle 14531 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1)) |
148 | 133 | recnd 10068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℂ) |
149 | | 1cnd 10056 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
150 | 14, 148, 149 | fsumadd 14470 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
151 | | logfac 24347 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
152 | 23, 151 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
153 | | fsumconst 14522 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((#‘(1...(⌊‘𝐴))) · 1)) |
154 | 14, 92, 153 | sylancl 694 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((#‘(1...(⌊‘𝐴))) · 1)) |
155 | 154, 97, 98 | 3eqtrrd 2661 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑛 ∈
(1...(⌊‘𝐴))1) |
156 | 152, 155 | oveq12d 6668 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
157 | 150, 156 | eqtr4d 2659 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) =
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
158 | 147, 157 | breqtrd 4679 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
159 | 35, 8, 27, 43 | leadd2dd 10642 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
160 | 20, 129, 28, 158, 159 | letrd 10194 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
161 | 13, 20, 28, 128, 160 | letrd 10194 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
162 | 13, 8, 27 | lesubaddd 10624 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴))) ↔ ((𝐴 · (log‘𝐴)) − 𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴))) |
163 | 161, 162 | mpbird 247 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴)))) |
164 | 12, 163 | eqbrtrd 4675 |
1
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
≤ (log‘(!‘(⌊‘𝐴)))) |