Step | Hyp | Ref
| Expression |
1 | | rpcn 12625 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
2 | 1 | times2d 12103 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 · 2) =
(𝐴 + 𝐴)) |
3 | 2 | oveq2d 7250 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
(𝐴 · 2)) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
4 | | relogcl 25495 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
5 | 4 | recnd 10890 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℂ) |
6 | | 2cnd 11937 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 2 ∈ ℂ) |
7 | 1, 5, 6 | subdid 11317 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= ((𝐴 ·
(log‘𝐴)) −
(𝐴 ·
2))) |
8 | | rpre 12623 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
9 | 8, 4 | remulcld 10892 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℝ) |
10 | 9 | recnd 10890 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ∈
ℂ) |
11 | 10, 1, 1 | subsub4d 11249 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) = ((𝐴 · (log‘𝐴)) − (𝐴 + 𝐴))) |
12 | 3, 7, 11 | 3eqtr4d 2789 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
= (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴)) |
13 | 9, 8 | resubcld 11289 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ∈
ℝ) |
14 | | fzfid 13577 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (1...(⌊‘𝐴)) ∈ Fin) |
15 | | fzfid 13577 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (1...𝑛) ∈
Fin) |
16 | | elfznn 13170 |
. . . . . . . 8
⊢ (𝑑 ∈ (1...𝑛) → 𝑑 ∈ ℕ) |
17 | 16 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → 𝑑 ∈ ℕ) |
18 | 17 | nnrecred 11910 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℝ) |
19 | 15, 18 | fsumrecl 15330 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ∈
ℝ) |
20 | 14, 19 | fsumrecl 15330 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ∈ ℝ) |
21 | | rprege0 12630 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 ≤ 𝐴)) |
22 | | flge0nn0 13424 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
24 | 23 | faccld 13882 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈ ℕ) |
25 | 24 | nnrpd 12655 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (!‘(⌊‘𝐴)) ∈
ℝ+) |
26 | 25 | relogcld 25542 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) ∈ ℝ) |
27 | 26, 8 | readdcld 10891 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + 𝐴) ∈ ℝ) |
28 | | elfznn 13170 |
. . . . . . . . . 10
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ 𝑑 ∈
ℕ) |
29 | 28 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℕ) |
30 | 29 | nnrecred 11910 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ) |
31 | 14, 30 | fsumrecl 15330 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑) ∈
ℝ) |
32 | 8, 31 | remulcld 10892 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) ∈
ℝ) |
33 | | reflcl 13400 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
34 | 8, 33 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
35 | 32, 34 | resubcld 11289 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ∈
ℝ) |
36 | | harmoniclbnd 25922 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ≤
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) |
37 | | rpregt0 12629 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℝ
∧ 0 < 𝐴)) |
38 | | lemul2 11714 |
. . . . . . . 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 235 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
(log‘𝐴)) ≤ (𝐴 · Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑))) |
41 | | flle 13403 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
42 | 8, 41 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
≤ 𝐴) |
43 | 9, 34, 32, 8, 40, 42 | le2subd 11481 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ ((𝐴 · Σ𝑑 ∈ (1...(⌊‘𝐴))(1 / 𝑑)) − (⌊‘𝐴))) |
44 | 28 | nnrecred 11910 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (1 / 𝑑) ∈
ℝ) |
45 | | remulcl 10843 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (1 / 𝑑) ∈ ℝ) → (𝐴 · (1 / 𝑑)) ∈
ℝ) |
46 | 8, 44, 45 | syl2an 599 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℝ) |
47 | | peano2rem 11174 |
. . . . . . . 8
⊢ ((𝐴 · (1 / 𝑑)) ∈ ℝ → ((𝐴 · (1 / 𝑑)) − 1) ∈
ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ∈
ℝ) |
49 | | fzfid 13577 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑...(⌊‘𝐴)) ∈ Fin) |
50 | 30 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) → (1 / 𝑑) ∈
ℝ) |
51 | 49, 50 | fsumrecl 15330 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) ∈ ℝ) |
52 | 8 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
53 | 52, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℝ) |
54 | | peano2re 11034 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℝ → ((⌊‘𝐴) + 1) ∈ ℝ) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((⌊‘𝐴) +
1) ∈ ℝ) |
56 | 29 | nnred 11874 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ) |
57 | | fllep1 13405 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ ((⌊‘𝐴) + 1)) |
58 | 8, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
59 | 58 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ≤
((⌊‘𝐴) +
1)) |
60 | 52, 55, 56, 59 | lesub1dd 11477 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑)) |
61 | 52, 56 | resubcld 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 − 𝑑) ∈
ℝ) |
62 | 55, 56 | resubcld 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) ∈
ℝ) |
63 | 29 | nnrpd 12655 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℝ+) |
64 | 63 | rpreccld 12667 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℝ+) |
65 | 61, 62, 64 | lemul1d 12700 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) ≤ (((⌊‘𝐴) + 1) − 𝑑) ↔ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑)))) |
66 | 60, 65 | mpbid 235 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) ≤ ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
67 | 1 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℂ) |
68 | 29 | nncnd 11875 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ∈
ℂ) |
69 | 30 | recnd 10890 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑑) ∈
ℂ) |
70 | 67, 68, 69 | subdird 11318 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 − 𝑑) · (1 / 𝑑)) = ((𝐴 · (1 / 𝑑)) − (𝑑 · (1 / 𝑑)))) |
71 | 29 | nnne0d 11909 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 𝑑 ≠
0) |
72 | 68, 71 | recidd 11632 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝑑 · (1 /
𝑑)) = 1) |
73 | 72 | oveq2d 7250 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − (𝑑 · (1 / 𝑑))) = ((𝐴 · (1 / 𝑑)) − 1)) |
74 | 70, 73 | eqtr2d 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) = ((𝐴 − 𝑑) · (1 / 𝑑))) |
75 | | fsumconst 15386 |
. . . . . . . . . 10
⊢ (((𝑑...(⌊‘𝐴)) ∈ Fin ∧ (1 / 𝑑) ∈ ℂ) →
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
76 | 49, 69, 75 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑))) |
77 | | elfzuz3 13138 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
78 | 77 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) |
79 | | hashfz 14026 |
. . . . . . . . . . . 12
⊢
((⌊‘𝐴)
∈ (ℤ≥‘𝑑) → (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) − 𝑑) + 1)) |
81 | 34 | recnd 10890 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℂ) |
82 | 81 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (⌊‘𝐴)
∈ ℂ) |
83 | | 1cnd 10857 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
84 | 82, 83, 68 | addsubd 11239 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (((⌊‘𝐴)
+ 1) − 𝑑) =
(((⌊‘𝐴) −
𝑑) + 1)) |
85 | 80, 84 | eqtr4d 2782 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (♯‘(𝑑...(⌊‘𝐴))) = (((⌊‘𝐴) + 1) − 𝑑)) |
86 | 85 | oveq1d 7249 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((♯‘(𝑑...(⌊‘𝐴))) · (1 / 𝑑)) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
87 | 76, 86 | eqtrd 2779 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ Σ𝑛 ∈
(𝑑...(⌊‘𝐴))(1 / 𝑑) = ((((⌊‘𝐴) + 1) − 𝑑) · (1 / 𝑑))) |
88 | 66, 74, 87 | 3brtr4d 5101 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ ((𝐴 · (1 /
𝑑)) − 1) ≤
Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
89 | 14, 48, 51, 88 | fsumle 15395 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) ≤ Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
90 | 14, 1, 69 | fsummulc2 15380 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) = Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑))) |
91 | | ax-1cn 10816 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
92 | | fsumconst 15386 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
93 | 14, 91, 92 | sylancl 589 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
94 | | hashfz1 13944 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ ℕ0 → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
95 | 23, 94 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ+
→ (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
96 | 95 | oveq1d 7249 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((♯‘(1...(⌊‘𝐴))) · 1) = ((⌊‘𝐴) · 1)) |
97 | 81 | mulid1d 10879 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴)
· 1) = (⌊‘𝐴)) |
98 | 93, 96, 97 | 3eqtrrd 2784 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑑 ∈
(1...(⌊‘𝐴))1) |
99 | 90, 98 | oveq12d 7252 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
(Σ𝑑 ∈
(1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
100 | 46 | recnd 10890 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑑 ∈
(1...(⌊‘𝐴)))
→ (𝐴 · (1 /
𝑑)) ∈
ℂ) |
101 | 14, 100, 83 | fsumsub 15384 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1) = (Σ𝑑 ∈ (1...(⌊‘𝐴))(𝐴 · (1 / 𝑑)) − Σ𝑑 ∈ (1...(⌊‘𝐴))1)) |
102 | 99, 101 | eqtr4d 2782 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) =
Σ𝑑 ∈
(1...(⌊‘𝐴))((𝐴 · (1 / 𝑑)) − 1)) |
103 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘1) =
(ℤ≥‘1) |
104 | 103 | uztrn2 12486 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) → 𝑛 ∈
(ℤ≥‘1)) |
105 | 104 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → 𝑛 ∈
(ℤ≥‘1)) |
106 | 105 | biantrurd 536 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
107 | | uzss 12490 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑑) → (ℤ≥‘𝑛) ⊆
(ℤ≥‘𝑑)) |
108 | 107 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) →
(ℤ≥‘𝑛) ⊆ (ℤ≥‘𝑑)) |
109 | 108 | sseld 3916 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) → (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
110 | 109 | pm4.71rd 566 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((⌊‘𝐴) ∈
(ℤ≥‘𝑛) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
111 | 106, 110 | bitr3d 284 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ (𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑))) → ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ↔ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
112 | 111 | pm5.32da 582 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (((𝑑 ∈
(ℤ≥‘1) ∧ 𝑛 ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
113 | | ancom 464 |
. . . . . . . . 9
⊢ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)))) |
114 | | an4 656 |
. . . . . . . . 9
⊢ (((𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)) ∧ ((⌊‘𝐴) ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
115 | 112, 113,
114 | 3bitr4g 317 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (((𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))))) |
116 | | elfzuzb 13135 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑛))) |
117 | | elfzuzb 13135 |
. . . . . . . . 9
⊢ (𝑑 ∈ (1...𝑛) ↔ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑))) |
118 | 116, 117 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ ((𝑛 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑛)) ∧ (𝑑 ∈ (ℤ≥‘1)
∧ 𝑛 ∈
(ℤ≥‘𝑑)))) |
119 | | elfzuzb 13135 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝐴))
↔ (𝑑 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ (ℤ≥‘𝑑))) |
120 | | elfzuzb 13135 |
. . . . . . . . 9
⊢ (𝑛 ∈ (𝑑...(⌊‘𝐴)) ↔ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛))) |
121 | 119, 120 | anbi12i 630 |
. . . . . . . 8
⊢ ((𝑑 ∈
(1...(⌊‘𝐴))
∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))) ↔ ((𝑑 ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ (ℤ≥‘𝑑)) ∧ (𝑛 ∈ (ℤ≥‘𝑑) ∧ (⌊‘𝐴) ∈
(ℤ≥‘𝑛)))) |
122 | 115, 118,
121 | 3bitr4g 317 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛)) ↔ (𝑑 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (𝑑...(⌊‘𝐴))))) |
123 | 18 | recnd 10890 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
∧ 𝑑 ∈ (1...𝑛)) → (1 / 𝑑) ∈
ℂ) |
124 | 123 | anasss 470 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ 𝑑 ∈ (1...𝑛))) → (1 / 𝑑) ∈
ℂ) |
125 | 14, 14, 15, 122, 124 | fsumcom2 15370 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) = Σ𝑑 ∈ (1...(⌊‘𝐴))Σ𝑛 ∈ (𝑑...(⌊‘𝐴))(1 / 𝑑)) |
126 | 89, 102, 125 | 3brtr4d 5101 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
Σ𝑑 ∈
(1...(⌊‘𝐴))(1 /
𝑑)) −
(⌊‘𝐴)) ≤
Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
127 | 13, 35, 20, 43, 126 | letrd 11018 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
128 | 26, 34 | readdcld 10891 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ∈ ℝ) |
129 | | elfznn 13170 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
130 | 129 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
131 | 130 | nnrpd 12655 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
132 | 131 | relogcld 25542 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
133 | | peano2re 11034 |
. . . . . . . 8
⊢
((log‘𝑛)
∈ ℝ → ((log‘𝑛) + 1) ∈ ℝ) |
134 | 132, 133 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((log‘𝑛) + 1)
∈ ℝ) |
135 | | nnz 12228 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
136 | | flid 13412 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(⌊‘𝑛) = 𝑛) |
138 | 137 | oveq2d 7250 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
139 | 138 | sumeq1d 15297 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) = Σ𝑑 ∈ (1...𝑛)(1 / 𝑑)) |
140 | | nnre 11866 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
141 | | nnge1 11887 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 1 ≤
𝑛) |
142 | | harmonicubnd 25923 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℝ ∧ 1 ≤
𝑛) → Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
143 | 140, 141,
142 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈
(1...(⌊‘𝑛))(1 /
𝑑) ≤ ((log‘𝑛) + 1)) |
144 | 139, 143 | eqbrtrrd 5093 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
145 | 130, 144 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ Σ𝑑 ∈
(1...𝑛)(1 / 𝑑) ≤ ((log‘𝑛) + 1)) |
146 | 14, 19, 134, 145 | fsumle 15395 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛) + 1)) |
147 | 132 | recnd 10890 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℂ) |
148 | | 1cnd 10857 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℂ) |
149 | 14, 147, 148 | fsumadd 15336 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
150 | | logfac 25520 |
. . . . . . . . 9
⊢
((⌊‘𝐴)
∈ ℕ0 → (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
151 | 23, 150 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (log‘(!‘(⌊‘𝐴))) = Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛)) |
152 | | fsumconst 15386 |
. . . . . . . . . 10
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
153 | 14, 91, 152 | sylancl 589 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))1 =
((♯‘(1...(⌊‘𝐴))) · 1)) |
154 | 153, 96, 97 | 3eqtrrd 2784 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴) =
Σ𝑛 ∈
(1...(⌊‘𝐴))1) |
155 | 151, 154 | oveq12d 7252 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) = (Σ𝑛 ∈ (1...(⌊‘𝐴))(log‘𝑛) + Σ𝑛 ∈ (1...(⌊‘𝐴))1)) |
156 | 149, 155 | eqtr4d 2782 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))((log‘𝑛) + 1) =
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
157 | 146, 156 | breqtrd 5095 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴))) |
158 | 34, 8, 26, 42 | leadd2dd 11476 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ ((log‘(!‘(⌊‘𝐴))) + (⌊‘𝐴)) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
159 | 20, 128, 27, 157, 158 | letrd 11018 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝐴))Σ𝑑 ∈ (1...𝑛)(1 / 𝑑) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
160 | 13, 20, 27, 127, 159 | letrd 11018 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((𝐴 ·
(log‘𝐴)) −
𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴)) |
161 | 13, 8, 26 | lesubaddd 11458 |
. . 3
⊢ (𝐴 ∈ ℝ+
→ ((((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴))) ↔ ((𝐴 · (log‘𝐴)) − 𝐴) ≤
((log‘(!‘(⌊‘𝐴))) + 𝐴))) |
162 | 160, 161 | mpbird 260 |
. 2
⊢ (𝐴 ∈ ℝ+
→ (((𝐴 ·
(log‘𝐴)) −
𝐴) − 𝐴) ≤
(log‘(!‘(⌊‘𝐴)))) |
163 | 12, 162 | eqbrtrd 5091 |
1
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ·
((log‘𝐴) − 2))
≤ (log‘(!‘(⌊‘𝐴)))) |