Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
2 | | elfznn 12370 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
3 | 2 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ) |
4 | 3 | nnrpd 11870 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℝ+) |
5 | 4 | relogcld 24369 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘𝑘) ∈
ℝ) |
6 | 5, 3 | nndivred 11069 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘𝑘) / 𝑘) ∈ ℝ) |
7 | 1, 6 | fsumrecl 14465 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) ∈ ℝ) |
8 | 7 | recnd 10068 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) ∈ ℂ) |
9 | | elioore 12205 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
10 | 9 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
11 | | 1rp 11836 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
13 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
14 | | eliooord 12233 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
15 | 14 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
16 | 15 | simpld 475 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
17 | 13, 10, 16 | ltled 10185 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
18 | 10, 12, 17 | rpgecld 11911 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
19 | 18 | relogcld 24369 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
20 | 19 | resqcld 13035 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥)↑2) ∈ ℝ) |
21 | 20 | rehalfcld 11279 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / 2) ∈
ℝ) |
22 | 21 | recnd 10068 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / 2) ∈
ℂ) |
23 | 19 | recnd 10068 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
24 | 10, 16 | rplogcld 24375 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
25 | 24 | rpne0d 11877 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
26 | 8, 22, 23, 25 | divsubdird 10840 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((((log‘𝑥)↑2) / 2) / (log‘𝑥)))) |
27 | 7, 21 | resubcld 10458 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) ∈
ℝ) |
28 | 27 | recnd 10068 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) ∈
ℂ) |
29 | 28, 23, 25 | divrecd 10804 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥)))) |
30 | 20 | recnd 10068 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥)↑2) ∈ ℂ) |
31 | | 2cnd 11093 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℂ) |
32 | | 2ne0 11113 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ≠ 0) |
34 | 30, 31, 23, 33, 25 | divdiv32d 10826 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / 2) / (log‘𝑥)) = ((((log‘𝑥)↑2) / (log‘𝑥)) / 2)) |
35 | 23 | sqvald 13005 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥)↑2) = ((log‘𝑥) · (log‘𝑥))) |
36 | 35 | oveq1d 6665 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / (log‘𝑥)) = (((log‘𝑥) · (log‘𝑥)) / (log‘𝑥))) |
37 | 23, 23, 25 | divcan3d 10806 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥) · (log‘𝑥)) / (log‘𝑥)) = (log‘𝑥)) |
38 | 36, 37 | eqtrd 2656 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((log‘𝑥)↑2) / (log‘𝑥)) = (log‘𝑥)) |
39 | 38 | oveq1d 6665 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / (log‘𝑥)) / 2) = ((log‘𝑥) / 2)) |
40 | 34, 39 | eqtrd 2656 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / 2) / (log‘𝑥)) = ((log‘𝑥) / 2)) |
41 | 40 | oveq2d 6666 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((((log‘𝑥)↑2) / 2) / (log‘𝑥))) = ((Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) |
42 | 26, 29, 41 | 3eqtr3rd 2665 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥)))) |
43 | 42 | mpteq2dva 4744 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥))))) |
44 | 24 | rprecred 11883 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ) |
45 | 18 | ex 450 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) → 𝑥
∈ ℝ+)) |
46 | 45 | ssrdv 3609 |
. . . . . 6
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ+) |
47 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) |
48 | 47 | logdivsum 25222 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) /
2))):ℝ+⟶ℝ ∧ (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom
⇝𝑟 ∧ (((𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ⇝𝑟
1 ∧ 1 ∈ ℝ+ ∧ e ≤ 1) → (abs‘(((𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)))‘1) − 1)) ≤
((log‘1) / 1))) |
49 | 48 | simp2i 1071 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom
⇝𝑟 |
50 | | rlimdmo1 14348 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom
⇝𝑟 → (𝑥 ∈ ℝ+ ↦
(Σ𝑘 ∈
(1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈
𝑂(1)) |
51 | 49, 50 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈
𝑂(1)) |
52 | 46, 51 | o1res2 14294 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈
𝑂(1)) |
53 | | divlogrlim 24381 |
. . . . . 6
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 |
54 | | rlimo1 14347 |
. . . . . 6
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
55 | 53, 54 | mp1i 13 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1)) |
56 | 27, 44, 52, 55 | o1mul2 14355 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 /
(log‘𝑥)))) ∈
𝑂(1)) |
57 | 43, 56 | eqeltrd 2701 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) |
58 | 8, 23, 25 | divcld 10801 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) ∈ ℂ) |
59 | 23 | halfcld 11277 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ) |
60 | 58, 59 | subcld 10392 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ) |
61 | | elfznn 12370 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
62 | 61 | adantl 482 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
63 | | vmacl 24844 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
65 | 64, 62 | nndivred 11069 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
66 | 18 | adantr 481 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
67 | 62 | nnrpd 11870 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
68 | 66, 67 | rpdivcld 11889 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
69 | 68 | relogcld 24369 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
70 | 65, 69 | remulcld 10070 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
71 | 1, 70 | fsumrecl 14465 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ) |
72 | 71 | recnd 10068 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) |
73 | 24 | rpcnd 11874 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
74 | 72, 73, 25 | divcld 10801 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ) |
75 | 73 | halfcld 11277 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ) |
76 | 74, 75 | subcld 10392 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ) |
77 | 58, 74, 59 | nnncan2d 10427 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) |
78 | 8, 72, 23, 25 | divsubdird 10840 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) |
79 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑥 /
𝑛))) ∈
Fin) |
80 | 64 | adantr 481 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑛) ∈
ℝ) |
81 | 62 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℕ) |
82 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
83 | 82 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ) |
84 | 81, 83 | nnmulcld 11068 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑛 · 𝑚) ∈ ℕ) |
85 | 80, 84 | nndivred 11069 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℝ) |
86 | 79, 85 | fsumrecl 14465 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℝ) |
87 | 86 | recnd 10068 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℂ) |
88 | 70 | recnd 10068 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) |
89 | 1, 87, 88 | fsumsub 14520 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
90 | 64 | recnd 10068 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℂ) |
91 | 62 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
92 | 62 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0) |
93 | 90, 91, 92 | divcld 10801 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
94 | 83 | nnrecred 11066 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℝ) |
95 | 79, 94 | fsumrecl 14465 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) ∈ ℝ) |
96 | 95 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) ∈ ℂ) |
97 | 69 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ) |
98 | 93, 96, 97 | subdid 10486 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
99 | 90 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑛) ∈
ℂ) |
100 | 91 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℂ) |
101 | 83 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ) |
102 | 92 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ≠ 0) |
103 | 83 | nnne0d 11065 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≠ 0) |
104 | 99, 100, 101, 102, 103 | divdiv1d 10832 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑛) / 𝑛) / 𝑚) = ((Λ‘𝑛) / (𝑛 · 𝑚))) |
105 | 99, 100, 102 | divcld 10801 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
106 | 105, 101,
103 | divrecd 10804 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑛) / 𝑛) / 𝑚) = (((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) |
107 | 104, 106 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / (𝑛 · 𝑚)) = (((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) |
108 | 107 | sumeq2dv 14433 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) |
109 | 101, 103 | reccld 10794 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℂ) |
110 | 79, 93, 109 | fsummulc2 14516 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑛) / 𝑛) · (1 / 𝑚))) |
111 | 108, 110 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) = (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚))) |
112 | 111 | oveq1d 6665 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
113 | 98, 112 | eqtr4d 2659 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
114 | 113 | sumeq2dv 14433 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
115 | | vmasum 24941 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ →
Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) = (log‘𝑘)) |
116 | 3, 115 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) = (log‘𝑘)) |
117 | 116 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) / 𝑘) = ((log‘𝑘) / 𝑘)) |
118 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (1...𝑘) ∈ Fin) |
119 | | dvdsssfz1 15040 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
120 | 3, 119 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
121 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
⊢
(((1...𝑘) ∈ Fin
∧ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) |
122 | 118, 120,
121 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) |
123 | 3 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℂ) |
124 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
125 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
126 | 124, 125 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ) |
127 | 126, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (Λ‘𝑛) ∈ ℝ) |
128 | 127 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (Λ‘𝑛) ∈ ℂ) |
129 | 128 | anassrs 680 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘𝑛) ∈ ℂ) |
130 | 3 | nnne0d 11065 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ≠ 0) |
131 | 122, 123,
129, 130 | fsumdivc 14518 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) / 𝑘) = Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘)) |
132 | 117, 131 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘𝑘) / 𝑘) = Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘)) |
133 | 132 | sumeq2dv 14433 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘)) |
134 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 · 𝑚) → ((Λ‘𝑛) / 𝑘) = ((Λ‘𝑛) / (𝑛 · 𝑚))) |
135 | 2 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ) |
136 | 135 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℂ) |
137 | 135 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ≠ 0) |
138 | 128, 136,
137 | divcld 10801 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((Λ‘𝑛) / 𝑘) ∈ ℂ) |
139 | 134, 10, 138 | dvdsflsumcom 24914 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚))) |
140 | 133, 139 | eqtrd 2656 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚))) |
141 | 140 | oveq1d 6665 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
142 | 89, 114, 141 | 3eqtr4rd 2667 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) |
143 | 142 | oveq1d 6665 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) |
144 | 77, 78, 143 | 3eqtr2d 2662 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) |
145 | 144 | mpteq2dva 4744 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) = (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))) |
146 | | 1red 10055 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) |
147 | 1, 65 | fsumrecl 14465 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
148 | 147, 24 | rerpdivcld 11903 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ) |
149 | | ioossre 12235 |
. . . . . . . . . . 11
⊢
(1(,)+∞) ⊆ ℝ |
150 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
151 | | o1const 14350 |
. . . . . . . . . . 11
⊢
(((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1)) |
152 | 149, 150,
151 | mp2an 708 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1) |
153 | 152 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ 1) ∈ 𝑂(1)) |
154 | 148 | recnd 10068 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ) |
155 | 12 | rpcnd 11874 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℂ) |
156 | 147 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
157 | 156, 23, 23, 25 | divsubdird 10840 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥)))) |
158 | 156, 23 | subcld 10392 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
159 | 158, 23, 25 | divrecd 10804 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) |
160 | 23, 25 | dividd 10799 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1) |
161 | 160 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) |
162 | 157, 159,
161 | 3eqtr3rd 2665 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) |
163 | 162 | mpteq2dva 4744 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))) |
164 | 147, 19 | resubcld 10458 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) |
165 | | vmadivsum 25171 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
166 | 165 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
167 | 46, 166 | o1res2 14294 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
168 | 164, 44, 167, 55 | o1mul2 14355 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈
𝑂(1)) |
169 | 163, 168 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈
𝑂(1)) |
170 | 154, 155,
169 | o1dif 14360 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1))) |
171 | 153, 170 | mpbird 247 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1)) |
172 | 148, 171 | o1lo1d 14270 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ ≤𝑂(1)) |
173 | 95, 69 | resubcld 10458 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ) |
174 | 65, 173 | remulcld 10070 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
175 | 1, 174 | fsumrecl 14465 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
176 | 175, 24 | rerpdivcld 11903 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ∈ ℝ) |
177 | | 1red 10055 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
178 | | vmage0 24847 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
179 | 62, 178 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) |
180 | 64, 67, 179 | divge0d 11912 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
181 | 68 | rpred 11872 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ) |
182 | 91 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛) |
183 | | fznnfl 12661 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
184 | 10, 183 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥))) |
185 | 184 | simplbda 654 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥) |
186 | 182, 185 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥) |
187 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) |
188 | 177, 187,
67 | lemuldivd 11921 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
189 | 186, 188 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛)) |
190 | | harmonicubnd 24736 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1)) |
191 | 181, 189,
190 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1)) |
192 | 95, 69, 177 | lesubadd2d 10626 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ≤ 1 ↔ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1))) |
193 | 191, 192 | mpbird 247 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ≤ 1) |
194 | 173, 177,
65, 180, 193 | lemul2ad 10964 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ (((Λ‘𝑛) / 𝑛) · 1)) |
195 | 93 | mulid1d 10057 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · 1) =
((Λ‘𝑛) / 𝑛)) |
196 | 194, 195 | breqtrd 4679 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) / 𝑛)) |
197 | 1, 174, 65, 196 | fsumle 14531 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
198 | 175, 147,
24, 197 | lediv1dd 11930 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) |
199 | 198 | adantrr 753 |
. . . . . . 7
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) |
200 | 146, 172,
148, 176, 199 | lo1le 14382 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ ≤𝑂(1)) |
201 | | 0red 10041 |
. . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) |
202 | | harmoniclbnd 24735 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ+ →
(log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚)) |
203 | 68, 202 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) |
204 | 95, 69 | subge0d 10617 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ↔ (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚))) |
205 | 203, 204 | mpbird 247 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) |
206 | 65, 173, 180, 205 | mulge0d 10604 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(((Λ‘𝑛) /
𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) |
207 | 1, 174, 206 | fsumge0 14527 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) |
208 | 175, 24, 207 | divge0d 11912 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) |
209 | 176, 201,
208 | o1lo12 14269 |
. . . . . 6
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈
≤𝑂(1))) |
210 | 200, 209 | mpbird 247 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1)) |
211 | 145, 210 | eqeltrd 2701 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈
𝑂(1)) |
212 | 60, 76, 211 | o1dif 14360 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1))) |
213 | 57, 212 | mpbid 222 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) |
214 | 213 | trud 1493 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) |