| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1red 11262 | . . 3
⊢ (⊤
→ 1 ∈ ℝ) | 
| 2 |  | reex 11246 | . . . . . . 7
⊢ ℝ
∈ V | 
| 3 |  | rpssre 13042 | . . . . . . 7
⊢
ℝ+ ⊆ ℝ | 
| 4 | 2, 3 | ssexi 5322 | . . . . . 6
⊢
ℝ+ ∈ V | 
| 5 | 4 | a1i 11 | . . . . 5
⊢ (⊤
→ ℝ+ ∈ V) | 
| 6 |  | fzfid 14014 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) | 
| 7 |  | rpre 13043 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 8 |  | elfznn 13593 | . . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) | 
| 9 |  | nndivre 12307 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ) | 
| 10 | 7, 8, 9 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) | 
| 11 | 10 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) | 
| 12 |  | reflcl 13836 | . . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 13 | 10, 12 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) | 
| 14 | 13 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) | 
| 15 | 11, 14 | subcld 11620 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ) | 
| 16 | 8 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) | 
| 17 |  | mucl 27184 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) | 
| 18 | 16, 17 | syl 17 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) | 
| 19 | 18 | zcnd 12723 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) | 
| 20 | 15, 19 | mulcld 11281 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) | 
| 21 | 6, 20 | fsumcl 15769 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) | 
| 22 |  | rpcn 13045 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) | 
| 23 |  | rpne0 13051 | . . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) | 
| 24 | 21, 22, 23 | divcld 12043 | . . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ) | 
| 25 | 24 | adantl 481 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ) | 
| 26 |  | ovexd 7466 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ V) | 
| 27 |  | eqidd 2738 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥))) | 
| 28 |  | eqidd 2738 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) | 
| 29 | 5, 25, 26, 27, 28 | offval2 7717 | . . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) | 
| 30 | 3 | a1i 11 | . . . . . 6
⊢ (⊤
→ ℝ+ ⊆ ℝ) | 
| 31 | 21 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) | 
| 32 | 22 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℂ) | 
| 33 | 23 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ≠ 0) | 
| 34 | 31, 32, 33 | absdivd 15494 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥))) | 
| 35 |  | rprege0 13050 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) | 
| 36 |  | absid 15335 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) | 
| 37 | 35, 36 | syl 17 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (abs‘𝑥) =
𝑥) | 
| 38 | 37 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘𝑥) = 𝑥) | 
| 39 | 38 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥)) | 
| 40 | 34, 39 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥)) | 
| 41 | 31 | abscld 15475 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ) | 
| 42 |  | fzfid 14014 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(1...(⌊‘𝑥))
∈ Fin) | 
| 43 | 20 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ) | 
| 44 | 43 | abscld 15475 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈
ℝ) | 
| 45 | 42, 44 | fsumrecl 15770 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ) | 
| 46 | 7 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℝ) | 
| 47 | 42, 43 | fsumabs 15837 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)))) | 
| 48 |  | reflcl 13836 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) | 
| 49 | 46, 48 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℝ) | 
| 50 |  | 1red 11262 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) | 
| 51 | 15 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ) | 
| 52 |  | fz1ssnn 13595 | . . . . . . . . . . . . . . . . . . . 20
⊢
(1...(⌊‘𝑥)) ⊆ ℕ | 
| 53 | 52 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(1...(⌊‘𝑥))
⊆ ℕ) | 
| 54 | 53 | sselda 3983 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) | 
| 55 | 54, 17 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) | 
| 56 | 55 | zcnd 12723 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) | 
| 57 | 51, 56 | absmuld 15493 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛)))) | 
| 58 | 51 | abscld 15475 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ∈
ℝ) | 
| 59 | 56 | abscld 15475 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ∈ ℝ) | 
| 60 | 51 | absge0d 15483 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))) | 
| 61 | 56 | absge0d 15483 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(μ‘𝑛))) | 
| 62 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
𝑥 ∈
ℝ+) | 
| 63 | 8 | nnrpd 13075 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) | 
| 64 |  | rpdivcl 13060 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 65 | 62, 63, 64 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) | 
| 66 | 3, 65 | sselid 3981 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) | 
| 67 | 66, 12 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℝ) | 
| 68 |  | flle 13839 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛)) | 
| 69 | 66, 68 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ≤ (𝑥 / 𝑛)) | 
| 70 | 67, 66, 69 | abssubge0d 15470 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) | 
| 71 |  | fracle1 13843 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) | 
| 72 | 66, 71 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1) | 
| 73 | 70, 72 | eqbrtrd 5165 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ≤ 1) | 
| 74 |  | mule1 27191 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ →
(abs‘(μ‘𝑛))
≤ 1) | 
| 75 | 54, 74 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ≤ 1) | 
| 76 | 58, 50, 59, 50, 60, 61, 73, 75 | lemul12ad 12210 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ·
(abs‘(μ‘𝑛)))
≤ (1 · 1)) | 
| 77 |  | 1t1e1 12428 | . . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 | 
| 78 | 76, 77 | breqtrdi 5184 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛)))) ·
(abs‘(μ‘𝑛)))
≤ 1) | 
| 79 | 57, 78 | eqbrtrd 5165 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑥 /
𝑛) −
(⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1) | 
| 80 | 42, 44, 50, 79 | fsumle 15835 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1) | 
| 81 |  | 1cnd 11256 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ ℂ) | 
| 82 |  | fsumconst 15826 | . . . . . . . . . . . . . . 15
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
((♯‘(1...(⌊‘𝑥))) · 1)) | 
| 83 | 42, 81, 82 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
((♯‘(1...(⌊‘𝑥))) · 1)) | 
| 84 |  | flge1nn 13861 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) | 
| 85 | 7, 84 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℕ) | 
| 86 | 85 | nnnn0d 12587 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℕ0) | 
| 87 |  | hashfz1 14385 | . . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) | 
| 88 | 86, 87 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) | 
| 89 | 88 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((♯‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1)) | 
| 90 | 49 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
ℂ) | 
| 91 | 90 | mulridd 11278 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((⌊‘𝑥) ·
1) = (⌊‘𝑥)) | 
| 92 | 83, 89, 91 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))1 =
(⌊‘𝑥)) | 
| 93 | 80, 92 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥)) | 
| 94 |  | flle 13839 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) | 
| 95 | 46, 94 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ≤
𝑥) | 
| 96 | 45, 49, 46, 93, 95 | letrd 11418 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥) | 
| 97 | 41, 45, 46, 47, 96 | letrd 11418 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥) | 
| 98 | 32 | mulridd 11278 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · 1) = 𝑥) | 
| 99 | 97, 98 | breqtrrd 5171 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)) | 
| 100 |  | 1red 11262 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ ℝ) | 
| 101 | 41, 100, 62 | ledivmuld 13130 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(((abs‘Σ𝑛
∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))) | 
| 102 | 99, 101 | mpbird 257 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1) | 
| 103 | 40, 102 | eqbrtrd 5165 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1) | 
| 104 | 103 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1) | 
| 105 | 30, 25, 1, 1, 104 | elo1d 15572 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1)) | 
| 106 |  | ax-1cn 11213 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 107 |  | divrcnv 15888 | . . . . . . 7
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) | 
| 108 | 106, 107 | ax-mp 5 | . . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 | 
| 109 |  | rlimo1 15653 | . . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
𝑂(1)) | 
| 110 | 108, 109 | mp1i 13 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) | 
| 111 |  | o1add 15650 | . . . . 5
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (1 / 𝑥)) ∈
𝑂(1)) → ((𝑥
∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) ∈
𝑂(1)) | 
| 112 | 105, 110,
111 | syl2anc 584 | . . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) ∈
𝑂(1)) | 
| 113 | 29, 112 | eqeltrrd 2842 | . . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1)) | 
| 114 |  | ovexd 7466 | . . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V) | 
| 115 | 18 | zred 12722 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℝ) | 
| 116 | 115, 16 | nndivred 12320 | . . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℝ) | 
| 117 | 116 | recnd 11289 | . . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) | 
| 118 | 6, 117 | fsumcl 15769 | . . . 4
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) | 
| 119 | 118 | adantl 481 | . . 3
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) | 
| 120 | 118 | adantr 480 | . . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ) | 
| 121 | 120 | abscld 15475 | . . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ) | 
| 122 | 117 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) | 
| 123 | 42, 32, 122 | fsummulc2 15820 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛))) | 
| 124 | 14, 19 | mulcld 11281 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘(𝑥 /
𝑛)) ·
(μ‘𝑛)) ∈
ℂ) | 
| 125 | 124 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘(𝑥 /
𝑛)) ·
(μ‘𝑛)) ∈
ℂ) | 
| 126 | 42, 43, 125 | fsumadd 15776 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))) | 
| 127 | 11 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) | 
| 128 | 14 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℂ) | 
| 129 | 127, 128 | npcand 11624 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛)) | 
| 130 | 129 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛))) | 
| 131 | 51, 128, 56 | adddird 11286 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))) | 
| 132 | 32 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) | 
| 133 | 54 | nnrpd 13075 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) | 
| 134 |  | rpcnne0 13053 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) | 
| 135 | 133, 134 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) | 
| 136 |  | div23 11941 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 ·
(μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛))) | 
| 137 |  | divass 11940 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 ·
(μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛))) | 
| 138 | 136, 137 | eqtr3d 2779 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧
(μ‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛))) | 
| 139 | 132, 56, 135, 138 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛))) | 
| 140 | 130, 131,
139 | 3eqtr3d 2785 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛))) | 
| 141 | 140 | sumeq2dv 15738 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛))) | 
| 142 |  | eqidd 2738 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛)) | 
| 143 |  | ssrab2 4080 | . . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ | 
| 144 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) | 
| 145 | 143, 144 | sselid 3981 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ) | 
| 146 | 145, 17 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ) | 
| 147 | 146 | zcnd 12723 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧
(𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℂ) | 
| 148 | 142, 46, 147 | dvdsflsumcom 27231 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛)) | 
| 149 | 147 | 3impb 1115 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (μ‘𝑛) ∈ ℂ) | 
| 150 | 149 | mulridd 11278 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛)) | 
| 151 | 150 | 2sumeq2dv 15741 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛)) | 
| 152 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → 1 =
1) | 
| 153 |  | nnuz 12921 | . . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) | 
| 154 | 85, 153 | eleqtrdi 2851 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) | 
| 155 |  | eluzfz1 13571 | . . . . . . . . . . . . . . 15
⊢
((⌊‘𝑥)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝑥))) | 
| 156 | 154, 155 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) → 1
∈ (1...(⌊‘𝑥))) | 
| 157 |  | 1cnd 11256 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) | 
| 158 | 152, 42, 53, 156, 157 | musumsum 27235 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · 1) = 1) | 
| 159 | 151, 158 | eqtr3d 2779 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (μ‘𝑛) = 1) | 
| 160 |  | fzfid 14014 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) | 
| 161 |  | fsumconst 15826 | . . . . . . . . . . . . . . 15
⊢
(((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) →
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) =
((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛))) | 
| 162 | 160, 56, 161 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) =
((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛))) | 
| 163 |  | rprege0 13050 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛))) | 
| 164 |  | flge0nn0 13860 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈
ℕ0) | 
| 165 |  | hashfz1 14385 | . . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑥 /
𝑛)) ∈
ℕ0 → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛))) | 
| 166 | 65, 163, 164, 165 | 4syl 19 | . . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛))) | 
| 167 | 166 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) | 
| 168 | 162, 167 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) | 
| 169 | 168 | sumeq2dv 15738 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) | 
| 170 | 148, 159,
169 | 3eqtr3rd 2786 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1) | 
| 171 | 170 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) | 
| 172 | 126, 141,
171 | 3eqtr3d 2785 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) | 
| 173 | 123, 172 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1)) | 
| 174 | 173 | oveq1d 7446 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥)) | 
| 175 | 120, 32, 33 | divcan3d 12048 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((𝑥 · Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) | 
| 176 |  | rpcnne0 13053 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) | 
| 177 | 176 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) | 
| 178 |  | divdir 11947 | . . . . . . . 8
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝑥 ∈ ℂ
∧ 𝑥 ≠ 0)) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) | 
| 179 | 31, 81, 177, 178 | syl3anc 1373 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) | 
| 180 | 174, 175,
179 | 3eqtr3d 2785 | . . . . . 6
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) | 
| 181 | 180 | fveq2d 6910 | . . . . 5
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) | 
| 182 | 121, 181 | eqled 11364 | . . . 4
⊢ ((𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) | 
| 183 | 182 | adantl 481 | . . 3
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) | 
| 184 | 1, 113, 114, 119, 183 | o1le 15689 | . 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)) | 
| 185 | 184 | mptru 1547 | 1
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1) |