Step | Hyp | Ref
| Expression |
1 | | 1red 10364 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
2 | | reex 10350 |
. . . . . . 7
⊢ ℝ
∈ V |
3 | | rpssre 12126 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
4 | 2, 3 | ssexi 5030 |
. . . . . 6
⊢
ℝ+ ∈ V |
5 | 4 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
6 | | fzfid 13074 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
7 | | rpre 12127 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
8 | | elfznn 12670 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
9 | | nndivre 11399 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ) |
10 | 7, 8, 9 | syl2an 589 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
11 | 10 | recnd 10392 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
12 | | reflcl 12899 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ) |
13 | 10, 12 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) |
14 | 13 | recnd 10392 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) |
15 | 11, 14 | subcld 10720 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ) |
16 | 8 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
17 | | mucl 25287 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) |
19 | 18 | zcnd 11818 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) |
20 | 15, 19 | mulcld 10384 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
21 | 6, 20 | fsumcl 14848 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
22 | | rpcn 12131 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
23 | | rpne0 12137 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
24 | 21, 22, 23 | divcld 11134 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ) |
25 | 24 | adantl 475 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ) |
26 | | ovexd 6944 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ V) |
27 | | eqidd 2826 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥))) |
28 | | eqidd 2826 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
29 | 5, 25, 26, 27, 28 | offval2 7179 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
30 | 3 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
31 | 21 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
32 | 22 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℂ) |
33 | 23 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ≠ 0) |
34 | 31, 32, 33 | absdivd 14578 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥))) |
35 | | rprege0 12136 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
36 | | absid 14420 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (abs‘𝑥) =
𝑥) |
38 | 37 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘𝑥) = 𝑥) |
39 | 38 | oveq2d 6926 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥)) |
40 | 34, 39 | eqtrd 2861 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥)) |
41 | 31 | abscld 14559 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ) |
42 | | fzfid 13074 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(1...(⌊‘𝑥))
∈ Fin) |
43 | 20 | adantlr 706 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) |
44 | 43 | abscld 14559 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈
ℝ) |
45 | 42, 44 | fsumrecl 14849 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ) |
46 | 7 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℝ) |
47 | 42, 43 | fsumabs 14914 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)))) |
48 | | reflcl 12899 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℝ) |
50 | | 1red 10364 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
51 | 15 | adantlr 706 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ) |
52 | | elfznn 12670 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
53 | 52 | ssriv 3831 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...(⌊‘𝑥)) ⊆ ℕ |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(1...(⌊‘𝑥))
⊆ ℕ) |
55 | 54 | sselda 3827 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
56 | 55, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) |
57 | 56 | zcnd 11818 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) |
58 | 51, 57 | absmuld 14577 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛)))) |
59 | 51 | abscld 14559 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ∈
ℝ) |
60 | 57 | abscld 14559 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ∈ ℝ) |
61 | 51 | absge0d 14567 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))) |
62 | 57 | absge0d 14567 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(μ‘𝑛))) |
63 | | simpl 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℝ+) |
64 | 8 | nnrpd 12161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
65 | | rpdivcl 12146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
66 | 63, 64, 65 | syl2an 589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
67 | 3, 66 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
68 | 67, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) |
69 | | flle 12902 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛)) |
70 | 67, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ≤ (𝑥 / 𝑛)) |
71 | 68, 67, 70 | abssubge0d 14554 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) |
72 | | fracle1 12906 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) |
73 | 67, 72 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) |
74 | 71, 73 | eqbrtrd 4897 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ≤ 1) |
75 | | mule1 25294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(abs‘(μ‘𝑛))
≤ 1) |
76 | 55, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ≤ 1) |
77 | 59, 50, 60, 50, 61, 62, 74, 76 | lemul12ad 11303 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ·
(abs‘(μ‘𝑛)))
≤ (1 · 1)) |
78 | | 1t1e1 11527 |
. . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 |
79 | 77, 78 | syl6breq 4916 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ·
(abs‘(μ‘𝑛)))
≤ 1) |
80 | 58, 79 | eqbrtrd 4897 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1) |
81 | 42, 44, 50, 80 | fsumle 14912 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1) |
82 | | 1cnd 10358 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ ℂ) |
83 | | fsumconst 14903 |
. . . . . . . . . . . . . . 15
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
((♯‘(1...(⌊‘𝑥))) · 1)) |
84 | 42, 82, 83 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
((♯‘(1...(⌊‘𝑥))) · 1)) |
85 | | flge1nn 12924 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
86 | 7, 85 | sylan 575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℕ) |
87 | 86 | nnnn0d 11685 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
88 | | hashfz1 13433 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
90 | 89 | oveq1d 6925 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((♯‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1)) |
91 | 49 | recnd 10392 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℂ) |
92 | 91 | mulid1d 10381 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((⌊‘𝑥) ·
1) = (⌊‘𝑥)) |
93 | 84, 90, 92 | 3eqtrd 2865 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
(⌊‘𝑥)) |
94 | 81, 93 | breqtrd 4901 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥)) |
95 | | flle 12902 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
96 | 46, 95 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ≤
𝑥) |
97 | 45, 49, 46, 94, 96 | letrd 10520 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥) |
98 | 41, 45, 46, 47, 97 | letrd 10520 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥) |
99 | 32 | mulid1d 10381 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · 1) = 𝑥) |
100 | 98, 99 | breqtrrd 4903 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)) |
101 | | 1red 10364 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ ℝ) |
102 | 41, 101, 63 | ledivmuld 12216 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(((abs‘Σ𝑛
∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))) |
103 | 100, 102 | mpbird 249 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1) |
104 | 40, 103 | eqbrtrd 4897 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1) |
105 | 104 | adantl 475 |
. . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1) |
106 | 30, 25, 1, 1, 105 | elo1d 14651 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1)) |
107 | | ax-1cn 10317 |
. . . . . . 7
⊢ 1 ∈
ℂ |
108 | | divrcnv 14965 |
. . . . . . 7
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
109 | 107, 108 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 |
110 | | rlimo1 14731 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
𝑂(1)) |
111 | 109, 110 | mp1i 13 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) |
112 | | o1add 14728 |
. . . . 5
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (1 / 𝑥)) ∈
𝑂(1)) → ((𝑥
∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) ∈
𝑂(1)) |
113 | 106, 111,
112 | syl2anc 579 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) ∈
𝑂(1)) |
114 | 29, 113 | eqeltrrd 2907 |
. . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1)) |
115 | | ovexd 6944 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V) |
116 | 18 | zred 11817 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℝ) |
117 | 116, 16 | nndivred 11412 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℝ) |
118 | 117 | recnd 10392 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) |
119 | 6, 118 | fsumcl 14848 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) |
120 | 119 | adantl 475 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) |
121 | 119 | adantr 474 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) |
122 | 121 | abscld 14559 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ) |
123 | 118 | adantlr 706 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) |
124 | 42, 32, 123 | fsummulc2 14897 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛))) |
125 | 14, 19 | mulcld 10384 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘(𝑥 /
𝑛)) ·
(μ‘𝑛)) ∈
ℂ) |
126 | 125 | adantlr 706 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘(𝑥 /
𝑛)) ·
(μ‘𝑛)) ∈
ℂ) |
127 | 42, 43, 126 | fsumadd 14854 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))) |
128 | 11 | adantlr 706 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
129 | 14 | adantlr 706 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) |
130 | 128, 129 | npcand 10724 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛)) |
131 | 130 | oveq1d 6925 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛))) |
132 | 51, 129, 57 | adddird 10389 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))) |
133 | 32 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
134 | 55 | nnrpd 12161 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
135 | | rpcnne0 12139 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
137 | | div23 11036 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 ·
(μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛))) |
138 | | divass 11035 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 ·
(μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
139 | 137, 138 | eqtr3d 2863 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
140 | 133, 57, 136, 139 | syl3anc 1494 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
141 | 131, 132,
140 | 3eqtr3d 2869 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛))) |
142 | 141 | sumeq2dv 14817 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛))) |
143 | | eqidd 2826 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛)) |
144 | | ssrab2 3914 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
145 | | simprr 789 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
146 | 144, 145 | sseldi 3825 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ) |
147 | 146, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ) |
148 | 147 | zcnd 11818 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℂ) |
149 | 143, 46, 148 | dvdsflsumcom 25334 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛)) |
150 | 148 | 3impb 1147 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (μ‘𝑛) ∈ ℂ) |
151 | 150 | mulid1d 10381 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛)) |
152 | 151 | 2sumeq2dv 14820 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛)) |
153 | | eqidd 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → 1 =
1) |
154 | | nnuz 12012 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
155 | 86, 154 | syl6eleq 2916 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) |
156 | | eluzfz1 12648 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘𝑥)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝑥))) |
157 | 155, 156 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ (1...(⌊‘𝑥))) |
158 | | 1cnd 10358 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
159 | 153, 42, 54, 157, 158 | musumsum 25338 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = 1) |
160 | 152, 159 | eqtr3d 2863 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = 1) |
161 | | fzfid 13074 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) |
162 | | fsumconst 14903 |
. . . . . . . . . . . . . . 15
⊢
(((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) →
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) =
((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛))) |
163 | 161, 57, 162 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) =
((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛))) |
164 | | rprege0 12136 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛))) |
165 | | flge0nn0 12923 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈
ℕ0) |
166 | | hashfz1 13433 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑥 /
𝑛)) ∈
ℕ0 → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛))) |
167 | 66, 164, 165, 166 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛))) |
168 | 167 | oveq1d 6925 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) |
169 | 163, 168 | eqtrd 2861 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) |
170 | 169 | sumeq2dv 14817 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) |
171 | 149, 160,
170 | 3eqtr3rd 2870 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1) |
172 | 171 | oveq2d 6926 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) |
173 | 127, 142,
172 | 3eqtr3d 2869 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) |
174 | 124, 173 | eqtrd 2861 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) |
175 | 174 | oveq1d 6925 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥)) |
176 | 121, 32, 33 | divcan3d 11139 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) |
177 | | rpcnne0 12139 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
178 | 177 | adantr 474 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) |
179 | | divdir 11042 |
. . . . . . . 8
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝑥 ∈ ℂ
∧ 𝑥 ≠ 0)) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) |
180 | 31, 82, 178, 179 | syl3anc 1494 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) |
181 | 175, 176,
180 | 3eqtr3d 2869 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) |
182 | 181 | fveq2d 6441 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
183 | | eqle 10465 |
. . . . 5
⊢
(((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ ∧
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
184 | 122, 182,
183 | syl2anc 579 |
. . . 4
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
185 | 184 | adantl 475 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) |
186 | 1, 114, 115, 120, 185 | o1le 14767 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
187 | 186 | mptru 1664 |
1
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) |