MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mudivsum Structured version   Visualization version   GIF version

Theorem mudivsum 24909
Description: Asymptotic formula for Σ𝑛𝑥, μ(𝑛) / 𝑛 = 𝑂(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)
Assertion
Ref Expression
mudivsum (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)
Distinct variable group:   𝑥,𝑛

Proof of Theorem mudivsum
Dummy variables 𝑘 𝑚 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1red 9809 . . 3 (⊤ → 1 ∈ ℝ)
2 reex 9781 . . . . . . 7 ℝ ∈ V
3 rpssre 11584 . . . . . . 7 + ⊆ ℝ
42, 3ssexi 4630 . . . . . 6 + ∈ V
54a1i 11 . . . . 5 (⊤ → ℝ+ ∈ V)
6 fzfid 12501 . . . . . . . 8 (𝑥 ∈ ℝ+ → (1...(⌊‘𝑥)) ∈ Fin)
7 rpre 11580 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
8 elfznn 12108 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9 nndivre 10810 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
107, 8, 9syl2an 492 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
1110recnd 9822 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
12 reflcl 12326 . . . . . . . . . . . 12 ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
1310, 12syl 17 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
1413recnd 9822 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
1511, 14subcld 10142 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
168adantl 480 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
17 mucl 24557 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
1918zcnd 11222 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
2015, 19mulcld 9814 . . . . . . . 8 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
216, 20fsumcl 14178 . . . . . . 7 (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
22 rpcn 11582 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
23 rpne0 11589 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ≠ 0)
2421, 22, 23divcld 10549 . . . . . 6 (𝑥 ∈ ℝ+ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
2524adantl 480 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
26 ovex 6453 . . . . . 6 (1 / 𝑥) ∈ V
2726a1i 11 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ V)
28 eqidd 2515 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)))
29 eqidd 2515 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
305, 25, 27, 28, 29offval2 6687 . . . 4 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
313a1i 11 . . . . . 6 (⊤ → ℝ+ ⊆ ℝ)
3221adantr 479 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
3322adantr 479 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℂ)
3423adantr 479 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ≠ 0)
3532, 33, 34absdivd 13899 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)))
36 rprege0 11588 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
37 absid 13741 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
3836, 37syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (abs‘𝑥) = 𝑥)
3938adantr 479 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
4039oveq2d 6441 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
4135, 40eqtrd 2548 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
4232abscld 13880 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
43 fzfid 12501 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ∈ Fin)
4420adantlr 746 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
4544abscld 13880 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
4643, 45fsumrecl 14179 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
477adantr 479 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ)
4843, 44fsumabs 14241 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))))
49 reflcl 12326 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
5047, 49syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℝ)
51 1red 9809 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
5215adantlr 746 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
53 elfznn 12108 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
5453ssriv 3476 . . . . . . . . . . . . . . . . . . . 20 (1...(⌊‘𝑥)) ⊆ ℕ
5554a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ⊆ ℕ)
5655sselda 3472 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
5756, 17syl 17 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
5857zcnd 11222 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
5952, 58absmuld 13898 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))))
6052abscld 13880 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ∈ ℝ)
6158abscld 13880 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
6252absge0d 13888 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))))
6358absge0d 13888 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(μ‘𝑛)))
64 simpl 471 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ+)
658nnrpd 11611 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
66 rpdivcl 11597 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
6764, 65, 66syl2an 492 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
683, 67sseldi 3470 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
6968, 12syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
70 flle 12329 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
7168, 70syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
7269, 68, 71abssubge0d 13875 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))
73 fracle1 12333 . . . . . . . . . . . . . . . . . . 19 ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
7468, 73syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
7572, 74eqbrtrd 4503 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ 1)
76 mule1 24564 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
7756, 76syl 17 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
7860, 51, 61, 51, 62, 63, 75, 77lemul12ad 10715 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ (1 · 1))
79 1t1e1 10929 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
8078, 79syl6breq 4522 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ 1)
8159, 80eqbrtrd 4503 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1)
8243, 45, 51, 81fsumle 14239 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1)
83 1cnd 9810 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 1 ∈ ℂ)
84 fsumconst 14231 . . . . . . . . . . . . . . 15 (((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((#‘(1...(⌊‘𝑥))) · 1))
8543, 83, 84syl2anc 690 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((#‘(1...(⌊‘𝑥))) · 1))
86 flge1nn 12351 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
877, 86sylan 486 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
8887nnnn0d 11105 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
89 hashfz1 12860 . . . . . . . . . . . . . . . 16 ((⌊‘𝑥) ∈ ℕ0 → (#‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
9088, 89syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (#‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
9190oveq1d 6440 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((#‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1))
9250recnd 9822 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℂ)
9392mulid1d 9811 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((⌊‘𝑥) · 1) = (⌊‘𝑥))
9485, 91, 933eqtrd 2552 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = (⌊‘𝑥))
9582, 94breqtrd 4507 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥))
96 flle 12329 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
9747, 96syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ≤ 𝑥)
9846, 50, 47, 95, 97letrd 9944 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
9942, 46, 47, 48, 98letrd 9944 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
10033mulid1d 9811 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 · 1) = 𝑥)
10199, 100breqtrrd 4509 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))
102 1red 9809 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 1 ∈ ℝ)
10342, 102, 64ledivmuld 11666 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)))
104101, 103mpbird 245 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1)
10541, 104eqbrtrd 4503 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
106105adantl 480 . . . . . 6 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
10731, 25, 1, 1, 106elo1d 13979 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1))
108 ax-1cn 9748 . . . . . . 7 1 ∈ ℂ
109 divrcnv 14290 . . . . . . 7 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
110108, 109ax-mp 5 . . . . . 6 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
111 rlimo1 14059 . . . . . 6 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
112110, 111mp1i 13 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
113 o1add 14056 . . . . 5 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
114107, 112, 113syl2anc 690 . . . 4 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
11530, 114eqeltrrd 2593 . . 3 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
116 ovex 6453 . . . 4 ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V
117116a1i 11 . . 3 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V)
11818zred 11221 . . . . . . 7 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
119118, 16nndivred 10823 . . . . . 6 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
120119recnd 9822 . . . . 5 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
1216, 120fsumcl 14178 . . . 4 (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
122121adantl 480 . . 3 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
123121adantr 479 . . . . . 6 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
124123abscld 13880 . . . . 5 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ)
125120adantlr 746 . . . . . . . . . 10 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
12643, 33, 125fsummulc2 14225 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
12714, 19mulcld 9814 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
128127adantlr 746 . . . . . . . . . . 11 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
12943, 44, 128fsumadd 14184 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
13011adantlr 746 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
13114adantlr 746 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
132130, 131npcand 10146 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛))
133132oveq1d 6440 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛)))
13452, 131, 58adddird 9819 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
13533adantr 479 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
13656nnrpd 11611 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
137 rpcnne0 11591 . . . . . . . . . . . . . 14 (𝑛 ∈ ℝ+ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
138136, 137syl 17 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
139 div23 10452 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛)))
140 divass 10451 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛)))
141139, 140eqtr3d 2550 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
142135, 58, 138, 141syl3anc 1317 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
143133, 134, 1423eqtr3d 2556 . . . . . . . . . . 11 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛)))
144143sumeq2dv 14148 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
145 eqidd 2515 . . . . . . . . . . . . 13 (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛))
146 ssrab2 3554 . . . . . . . . . . . . . . . 16 {𝑦 ∈ ℕ ∣ 𝑦𝑘} ⊆ ℕ
147 simprr 791 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})
148146, 147sseldi 3470 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑛 ∈ ℕ)
149148, 17syl 17 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (μ‘𝑛) ∈ ℤ)
150149zcnd 11222 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (μ‘𝑛) ∈ ℂ)
151145, 47, 150dvdsflsumcom 24604 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛))
1521503impb 1251 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘}) → (μ‘𝑛) ∈ ℂ)
153152mulid1d 9811 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛))
1541532sumeq2dv 14150 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} (μ‘𝑛))
155 eqidd 2515 . . . . . . . . . . . . . 14 (𝑘 = 1 → 1 = 1)
156 nnuz 11462 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
15787, 156syl6eleq 2602 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ (ℤ‘1))
158 eluzfz1 12086 . . . . . . . . . . . . . . 15 ((⌊‘𝑥) ∈ (ℤ‘1) → 1 ∈ (1...(⌊‘𝑥)))
159157, 158syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 1 ∈ (1...(⌊‘𝑥)))
160 1cnd 9810 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
161155, 43, 55, 159, 160musumsum 24608 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · 1) = 1)
162154, 161eqtr3d 2550 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} (μ‘𝑛) = 1)
163 fzfid 12501 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
164 fsumconst 14231 . . . . . . . . . . . . . . 15 (((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((#‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
165163, 58, 164syl2anc 690 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((#‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
166 rprege0 11588 . . . . . . . . . . . . . . . 16 ((𝑥 / 𝑛) ∈ ℝ+ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)))
167 flge0nn0 12350 . . . . . . . . . . . . . . . 16 (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈ ℕ0)
168 hashfz1 12860 . . . . . . . . . . . . . . . 16 ((⌊‘(𝑥 / 𝑛)) ∈ ℕ0 → (#‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
16967, 166, 167, 1684syl 19 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (#‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
170169oveq1d 6440 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((#‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
171165, 170eqtrd 2548 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
172171sumeq2dv 14148 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
173151, 162, 1723eqtr3rd 2557 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1)
174173oveq2d 6441 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
175129, 144, 1743eqtr3d 2556 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
176126, 175eqtrd 2548 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
177176oveq1d 6440 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥))
178123, 33, 34divcan3d 10554 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛))
179 rpcnne0 11591 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
180179adantr 479 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
181 divdir 10458 . . . . . . . 8 ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
18232, 83, 180, 181syl3anc 1317 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
183177, 178, 1823eqtr3d 2556 . . . . . 6 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
184183fveq2d 5990 . . . . 5 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
185 eqle 9889 . . . . 5 (((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ ∧ (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
186124, 184, 185syl2anc 690 . . . 4 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
187186adantl 480 . . 3 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
1881, 115, 117, 122, 187o1le 14095 . 2 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1))
189188trud 1483 1 (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wa 382  w3a 1030   = wceq 1474  wtru 1475  wcel 1938  wne 2684  {crab 2804  Vcvv 3077  wss 3444   class class class wbr 4481  cmpt 4541  cfv 5689  (class class class)co 6425  𝑓 cof 6668  Fincfn 7716  cc 9688  cr 9689  0cc0 9690  1c1 9691   + caddc 9693   · cmul 9695  cle 9829  cmin 10016   / cdiv 10432  cn 10774  0cn0 11046  cz 11117  cuz 11426  +crp 11573  ...cfz 12064  cfl 12320  #chash 12846  abscabs 13679  𝑟 crli 13928  𝑂(1)co1 13929  Σcsu 14131  cdvds 14688  μcmu 24511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6722  ax-inf2 8296  ax-cnex 9746  ax-resscn 9747  ax-1cn 9748  ax-icn 9749  ax-addcl 9750  ax-addrcl 9751  ax-mulcl 9752  ax-mulrcl 9753  ax-mulcom 9754  ax-addass 9755  ax-mulass 9756  ax-distr 9757  ax-i2m1 9758  ax-1ne0 9759  ax-1rid 9760  ax-rnegex 9761  ax-rrecex 9762  ax-cnre 9763  ax-pre-lttri 9764  ax-pre-lttrn 9765  ax-pre-ltadd 9766  ax-pre-mulgt0 9767  ax-pre-sup 9768
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-disj 4452  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-of 6670  df-om 6833  df-1st 6933  df-2nd 6934  df-wrecs 7168  df-recs 7230  df-rdg 7268  df-1o 7322  df-2o 7323  df-oadd 7326  df-er 7504  df-map 7621  df-pm 7622  df-en 7717  df-dom 7718  df-sdom 7719  df-fin 7720  df-sup 8106  df-inf 8107  df-oi 8173  df-card 8523  df-cda 8748  df-pnf 9830  df-mnf 9831  df-xr 9832  df-ltxr 9833  df-le 9834  df-sub 10018  df-neg 10019  df-div 10433  df-nn 10775  df-2 10833  df-3 10834  df-n0 11047  df-z 11118  df-uz 11427  df-q 11530  df-rp 11574  df-ico 11920  df-fz 12065  df-fzo 12202  df-fl 12322  df-mod 12398  df-seq 12531  df-exp 12590  df-fac 12790  df-bc 12819  df-hash 12847  df-cj 13544  df-re 13545  df-im 13546  df-sqrt 13680  df-abs 13681  df-clim 13931  df-rlim 13932  df-o1 13933  df-lo1 13934  df-sum 14132  df-dvds 14689  df-gcd 14926  df-prm 15098  df-pc 15262  df-mu 24517
This theorem is referenced by:  mulogsumlem  24910  mulog2sumlem3  24915  selberglem1  24924
  Copyright terms: Public domain W3C validator