Step | Hyp | Ref
| Expression |
1 | | 1red 9934 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
2 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
3 | | rpssre 11719 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
4 | 2, 3 | ssexi 4731 |
. . . . . 6
⊢
ℝ+ ∈ V |
5 | 4 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
6 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
7 | | rpre 11715 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
8 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
9 | | nndivre 10933 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ) |
10 | 7, 8, 9 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
11 | 10 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
12 | | reflcl 12459 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ) |
13 | 10, 12 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) |
14 | 13 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) |
15 | 11, 14 | subcld 10271 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ) |
16 | 8 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
17 | | mucl 24667 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) |
19 | 18 | zcnd 11359 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) |
20 | 15, 19 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
21 | 6, 20 | fsumcl 14311 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
22 | | rpcn 11717 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
23 | | rpne0 11724 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
24 | 21, 22, 23 | divcld 10680 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ) |
25 | 24 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ) |
26 | | ovex 6577 |
. . . . . 6
⊢ (1 /
𝑥) ∈
V |
27 | 26 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ V) |
28 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥))) |
29 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
30 | 5, 25, 27, 28, 29 | offval2 6812 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
31 | 3 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
32 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
33 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℂ) |
34 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ≠ 0) |
35 | 32, 33, 34 | absdivd 14042 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥))) |
36 | | rprege0 11723 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
37 | | absid 13884 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (abs‘𝑥) =
𝑥) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘𝑥) = 𝑥) |
40 | 39 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥)) |
41 | 35, 40 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥)) |
42 | 32 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ) |
43 | | fzfid 12634 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(1...(⌊‘𝑥))
∈ Fin) |
44 | 20 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
45 | 44 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈
ℝ) |
46 | 43, 45 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ) |
47 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℝ) |
48 | 43, 44 | fsumabs 14374 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)))) |
49 | | reflcl 12459 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℝ) |
51 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
52 | 15 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ) |
53 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
54 | 53 | ssriv 3572 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...(⌊‘𝑥)) ⊆ ℕ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(1...(⌊‘𝑥))
⊆ ℕ) |
56 | 55 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
57 | 56, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) |
58 | 57 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) |
59 | 52, 58 | absmuld 14041 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛)))) |
60 | 52 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ∈
ℝ) |
61 | 58 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ∈ ℝ) |
62 | 52 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))) |
63 | 58 | absge0d 14031 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(μ‘𝑛))) |
64 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℝ+) |
65 | 8 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
66 | | rpdivcl 11732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
67 | 64, 65, 66 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
68 | 3, 67 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
69 | 68, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) |
70 | | flle 12462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛)) |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ≤ (𝑥 / 𝑛)) |
72 | 69, 68, 71 | abssubge0d 14018 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) |
73 | | fracle1 12466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) |
74 | 68, 73 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) |
75 | 72, 74 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ≤ 1) |
76 | | mule1 24674 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(abs‘(μ‘𝑛))
≤ 1) |
77 | 56, 76 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ≤ 1) |
78 | 60, 51, 61, 51, 62, 63, 75, 77 | lemul12ad 10845 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ·
(abs‘(μ‘𝑛)))
≤ (1 · 1)) |
79 | | 1t1e1 11052 |
. . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 |
80 | 78, 79 | syl6breq 4624 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ·
(abs‘(μ‘𝑛)))
≤ 1) |
81 | 59, 80 | eqbrtrd 4605 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1) |
82 | 43, 45, 51, 81 | fsumle 14372 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1) |
83 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ ℂ) |
84 | | fsumconst 14364 |
. . . . . . . . . . . . . . 15
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
((#‘(1...(⌊‘𝑥))) · 1)) |
85 | 43, 83, 84 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
((#‘(1...(⌊‘𝑥))) · 1)) |
86 | | flge1nn 12484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
87 | 7, 86 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℕ) |
88 | 87 | nnnn0d 11228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
89 | | hashfz1 12996 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℕ0 → (#‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(#‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
91 | 90 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((#‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1)) |
92 | 50 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℂ) |
93 | 92 | mulid1d 9936 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((⌊‘𝑥) ·
1) = (⌊‘𝑥)) |
94 | 85, 91, 93 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
(⌊‘𝑥)) |
95 | 82, 94 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥)) |
96 | | flle 12462 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
97 | 47, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ≤
𝑥) |
98 | 46, 50, 47, 95, 97 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥) |
99 | 42, 46, 47, 48, 98 | letrd 10073 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥) |
100 | 33 | mulid1d 9936 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · 1) = 𝑥) |
101 | 99, 100 | breqtrrd 4611 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)) |
102 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ ℝ) |
103 | 42, 102, 64 | ledivmuld 11801 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(((abs‘Σ𝑛
∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))) |
104 | 101, 103 | mpbird 246 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1) |
105 | 41, 104 | eqbrtrd 4605 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1) |
106 | 105 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1) |
107 | 31, 25, 1, 1, 106 | elo1d 14115 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1)) |
108 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
109 | | divrcnv 14423 |
. . . . . . 7
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
110 | 108, 109 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 |
111 | | rlimo1 14195 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
𝑂(1)) |
112 | 110, 111 | mp1i 13 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) |
113 | | o1add 14192 |
. . . . 5
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (1 / 𝑥)) ∈
𝑂(1)) → ((𝑥
∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) ∈
𝑂(1)) |
114 | 107, 112,
113 | syl2anc 691 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) ∈
𝑂(1)) |
115 | 30, 114 | eqeltrrd 2689 |
. . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1)) |
116 | | ovex 6577 |
. . . 4
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V |
117 | 116 | a1i 11 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V) |
118 | 18 | zred 11358 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℝ) |
119 | 118, 16 | nndivred 10946 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℝ) |
120 | 119 | recnd 9947 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) |
121 | 6, 120 | fsumcl 14311 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) |
122 | 121 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) |
123 | 121 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) |
124 | 123 | abscld 14023 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ) |
125 | 120 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) |
126 | 43, 33, 125 | fsummulc2 14358 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛))) |
127 | 14, 19 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘(𝑥 /
𝑛)) ·
(μ‘𝑛)) ∈
ℂ) |
128 | 127 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘(𝑥 /
𝑛)) ·
(μ‘𝑛)) ∈
ℂ) |
129 | 43, 44, 128 | fsumadd 14317 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))) |
130 | 11 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
131 | 14 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) |
132 | 130, 131 | npcand 10275 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛)) |
133 | 132 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛))) |
134 | 52, 131, 58 | adddird 9944 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))) |
135 | 33 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
136 | 56 | nnrpd 11746 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
137 | | rpcnne0 11726 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
139 | | div23 10583 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 ·
(μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛))) |
140 | | divass 10582 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 ·
(μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
141 | 139, 140 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
142 | 135, 58, 138, 141 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
143 | 133, 134,
142 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
144 | 143 | sumeq2dv 14281 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛))) |
145 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛)) |
146 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
147 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
148 | 146, 147 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ) |
149 | 148, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ) |
150 | 149 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℂ) |
151 | 145, 47, 150 | dvdsflsumcom 24714 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛)) |
152 | 150 | 3impb 1252 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (μ‘𝑛) ∈ ℂ) |
153 | 152 | mulid1d 9936 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛)) |
154 | 153 | 2sumeq2dv 14283 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛)) |
155 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → 1 =
1) |
156 | | nnuz 11599 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
157 | 87, 156 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) |
158 | | eluzfz1 12219 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘𝑥)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝑥))) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ (1...(⌊‘𝑥))) |
160 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
161 | 155, 43, 55, 159, 160 | musumsum 24718 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = 1) |
162 | 154, 161 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = 1) |
163 | | fzfid 12634 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) |
164 | | fsumconst 14364 |
. . . . . . . . . . . . . . 15
⊢
(((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) →
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) =
((#‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛))) |
165 | 163, 58, 164 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) =
((#‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛))) |
166 | | rprege0 11723 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛))) |
167 | | flge0nn0 12483 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈
ℕ0) |
168 | | hashfz1 12996 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑥 /
𝑛)) ∈
ℕ0 → (#‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛))) |
169 | 67, 166, 167, 168 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (#‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛))) |
170 | 169 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((#‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) |
171 | 165, 170 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) |
172 | 171 | sumeq2dv 14281 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) |
173 | 151, 162,
172 | 3eqtr3rd 2653 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1) |
174 | 173 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) |
175 | 129, 144,
174 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) |
176 | 126, 175 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) |
177 | 176 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥)) |
178 | 123, 33, 34 | divcan3d 10685 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) |
179 | | rpcnne0 11726 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
180 | 179 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) |
181 | | divdir 10589 |
. . . . . . . 8
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝑥 ∈ ℂ
∧ 𝑥 ≠ 0)) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) |
182 | 32, 83, 180, 181 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) |
183 | 177, 178,
182 | 3eqtr3d 2652 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) |
184 | 183 | fveq2d 6107 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
185 | | eqle 10018 |
. . . . 5
⊢
(((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ ∧
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
186 | 124, 184,
185 | syl2anc 691 |
. . . 4
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
187 | 186 | adantl 481 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
188 | 1, 115, 117, 122, 187 | o1le 14231 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
189 | 188 | trud 1484 |
1
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) |