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

Theorem mudivsum 27574
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 11262 . . 3 (⊤ → 1 ∈ ℝ)
2 reex 11246 . . . . . . 7 ℝ ∈ V
3 rpssre 13042 . . . . . . 7 + ⊆ ℝ
42, 3ssexi 5322 . . . . . 6 + ∈ V
54a1i 11 . . . . 5 (⊤ → ℝ+ ∈ V)
6 fzfid 14014 . . . . . . . 8 (𝑥 ∈ ℝ+ → (1...(⌊‘𝑥)) ∈ Fin)
7 rpre 13043 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
8 elfznn 13593 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9 nndivre 12307 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
107, 8, 9syl2an 596 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
1110recnd 11289 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
12 reflcl 13836 . . . . . . . . . . . 12 ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
1310, 12syl 17 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
1413recnd 11289 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
1511, 14subcld 11620 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
168adantl 481 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
17 mucl 27184 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
1918zcnd 12723 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
2015, 19mulcld 11281 . . . . . . . 8 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
216, 20fsumcl 15769 . . . . . . 7 (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
22 rpcn 13045 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
23 rpne0 13051 . . . . . . 7 (𝑥 ∈ ℝ+𝑥 ≠ 0)
2421, 22, 23divcld 12043 . . . . . 6 (𝑥 ∈ ℝ+ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
2524adantl 481 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) ∈ ℂ)
26 ovexd 7466 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ V)
27 eqidd 2738 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)))
28 eqidd 2738 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
295, 25, 26, 27, 28offval2 7717 . . . 4 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
303a1i 11 . . . . . 6 (⊤ → ℝ+ ⊆ ℝ)
3121adantr 480 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
3222adantr 480 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℂ)
3323adantr 480 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ≠ 0)
3431, 32, 33absdivd 15494 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)))
35 rprege0 13050 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
36 absid 15335 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
3735, 36syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (abs‘𝑥) = 𝑥)
3837adantr 480 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘𝑥) = 𝑥)
3938oveq2d 7447 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / (abs‘𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
4034, 39eqtrd 2777 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥))
4131abscld 15475 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
42 fzfid 14014 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ∈ Fin)
4320adantlr 715 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ)
4443abscld 15475 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
4542, 44fsumrecl 15770 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ∈ ℝ)
467adantr 480 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ)
4742, 43fsumabs 15837 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))))
48 reflcl 13836 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
4946, 48syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℝ)
50 1red 11262 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
5115adantlr 715 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
52 fz1ssnn 13595 . . . . . . . . . . . . . . . . . . . 20 (1...(⌊‘𝑥)) ⊆ ℕ
5352a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (1...(⌊‘𝑥)) ⊆ ℕ)
5453sselda 3983 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
5554, 17syl 17 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
5655zcnd 12723 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
5751, 56absmuld 15493 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) = ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))))
5851abscld 15475 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ∈ ℝ)
5956abscld 15475 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
6051absge0d 15483 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))))
6156absge0d 15483 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(μ‘𝑛)))
62 simpl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 𝑥 ∈ ℝ+)
638nnrpd 13075 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
64 rpdivcl 13060 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
6562, 63, 64syl2an 596 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
663, 65sselid 3981 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
6766, 12syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
68 flle 13839 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
6966, 68syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
7067, 66, 69abssubge0d 15470 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))
71 fracle1 13843 . . . . . . . . . . . . . . . . . . 19 ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
7266, 71syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
7370, 72eqbrtrd 5165 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ 1)
74 mule1 27191 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
7554, 74syl 17 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
7658, 50, 59, 50, 60, 61, 73, 75lemul12ad 12210 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ (1 · 1))
77 1t1e1 12428 . . . . . . . . . . . . . . . 16 (1 · 1) = 1
7876, 77breqtrdi 5184 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) · (abs‘(μ‘𝑛))) ≤ 1)
7957, 78eqbrtrd 5165 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 1)
8042, 44, 50, 79fsumle 15835 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))1)
81 1cnd 11256 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 1 ∈ ℂ)
82 fsumconst 15826 . . . . . . . . . . . . . . 15 (((1...(⌊‘𝑥)) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
8342, 81, 82syl2anc 584 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = ((♯‘(1...(⌊‘𝑥))) · 1))
84 flge1nn 13861 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
857, 84sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
8685nnnn0d 12587 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
87 hashfz1 14385 . . . . . . . . . . . . . . . 16 ((⌊‘𝑥) ∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
8886, 87syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
8988oveq1d 7446 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((♯‘(1...(⌊‘𝑥))) · 1) = ((⌊‘𝑥) · 1))
9049recnd 11289 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℂ)
9190mulridd 11278 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((⌊‘𝑥) · 1) = (⌊‘𝑥))
9283, 89, 913eqtrd 2781 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))1 = (⌊‘𝑥))
9380, 92breqtrd 5169 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (⌊‘𝑥))
94 flle 13839 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
9546, 94syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ≤ 𝑥)
9645, 49, 46, 93, 95letrd 11418 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
9741, 45, 46, 47, 96letrd 11418 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ 𝑥)
9832mulridd 11278 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 · 1) = 𝑥)
9997, 98breqtrrd 5171 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1))
100 1red 11262 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 1 ∈ ℝ)
10141, 100, 62ledivmuld 13130 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1 ↔ (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) ≤ (𝑥 · 1)))
10299, 101mpbird 257 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛))) / 𝑥) ≤ 1)
10340, 102eqbrtrd 5165 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
104103adantl 481 . . . . . 6 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ≤ 1)
10530, 25, 1, 1, 104elo1d 15572 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1))
106 ax-1cn 11213 . . . . . . 7 1 ∈ ℂ
107 divrcnv 15888 . . . . . . 7 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
108106, 107ax-mp 5 . . . . . 6 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
109 rlimo1 15653 . . . . . 6 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
110108, 109mp1i 13 . . . . 5 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
111 o1add 15650 . . . . 5 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
112105, 110, 111syl2anc 584 . . . 4 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
11329, 112eqeltrrd 2842 . . 3 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
114 ovexd 7466 . . 3 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)) ∈ V)
11518zred 12722 . . . . . . 7 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
116115, 16nndivred 12320 . . . . . 6 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
117116recnd 11289 . . . . 5 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
1186, 117fsumcl 15769 . . . 4 (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
119118adantl 481 . . 3 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
120118adantr 480 . . . . . 6 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) ∈ ℂ)
121120abscld 15475 . . . . 5 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ ℝ)
122117adantlr 715 . . . . . . . . . 10 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
12342, 32, 122fsummulc2 15820 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
12414, 19mulcld 11281 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
125124adantlr 715 . . . . . . . . . . 11 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) ∈ ℂ)
12642, 43, 125fsumadd 15776 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
12711adantlr 715 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
12814adantlr 715 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
129127, 128npcand 11624 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) = (𝑥 / 𝑛))
130129oveq1d 7446 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((𝑥 / 𝑛) · (μ‘𝑛)))
13151, 128, 56adddird 11286 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) + (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) = ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))))
13232adantr 480 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
13354nnrpd 13075 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
134 rpcnne0 13053 . . . . . . . . . . . . . 14 (𝑛 ∈ ℝ+ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
135133, 134syl 17 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
136 div23 11941 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = ((𝑥 / 𝑛) · (μ‘𝑛)))
137 divass 11940 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 · (μ‘𝑛)) / 𝑛) = (𝑥 · ((μ‘𝑛) / 𝑛)))
138136, 137eqtr3d 2779 . . . . . . . . . . . . 13 ((𝑥 ∈ ℂ ∧ (μ‘𝑛) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
139132, 56, 135, 138syl3anc 1373 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) · (μ‘𝑛)) = (𝑥 · ((μ‘𝑛) / 𝑛)))
140130, 131, 1393eqtr3d 2785 . . . . . . . . . . 11 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (𝑥 · ((μ‘𝑛) / 𝑛)))
141140sumeq2dv 15738 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)))
142 eqidd 2738 . . . . . . . . . . . . 13 (𝑘 = (𝑛 · 𝑚) → (μ‘𝑛) = (μ‘𝑛))
143 ssrab2 4080 . . . . . . . . . . . . . . . 16 {𝑦 ∈ ℕ ∣ 𝑦𝑘} ⊆ ℕ
144 simprr 773 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})
145143, 144sselid 3981 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑛 ∈ ℕ)
146145, 17syl 17 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (μ‘𝑛) ∈ ℤ)
147146zcnd 12723 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (μ‘𝑛) ∈ ℂ)
148142, 46, 147dvdsflsumcom 27231 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} (μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛))
1491473impb 1115 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘}) → (μ‘𝑛) ∈ ℂ)
150149mulridd 11278 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘}) → ((μ‘𝑛) · 1) = (μ‘𝑛))
1511502sumeq2dv 15741 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · 1) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} (μ‘𝑛))
152 eqidd 2738 . . . . . . . . . . . . . 14 (𝑘 = 1 → 1 = 1)
153 nnuz 12921 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
15485, 153eleqtrdi 2851 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ (ℤ‘1))
155 eluzfz1 13571 . . . . . . . . . . . . . . 15 ((⌊‘𝑥) ∈ (ℤ‘1) → 1 ∈ (1...(⌊‘𝑥)))
156154, 155syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → 1 ∈ (1...(⌊‘𝑥)))
157 1cnd 11256 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
158152, 42, 53, 156, 157musumsum 27235 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · 1) = 1)
159151, 158eqtr3d 2779 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} (μ‘𝑛) = 1)
160 fzfid 14014 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
161 fsumconst 15826 . . . . . . . . . . . . . . 15 (((1...(⌊‘(𝑥 / 𝑛))) ∈ Fin ∧ (μ‘𝑛) ∈ ℂ) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
162160, 56, 161syl2anc 584 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)))
163 rprege0 13050 . . . . . . . . . . . . . . . 16 ((𝑥 / 𝑛) ∈ ℝ+ → ((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)))
164 flge0nn0 13860 . . . . . . . . . . . . . . . 16 (((𝑥 / 𝑛) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑛)) → (⌊‘(𝑥 / 𝑛)) ∈ ℕ0)
165 hashfz1 14385 . . . . . . . . . . . . . . . 16 ((⌊‘(𝑥 / 𝑛)) ∈ ℕ0 → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
16665, 163, 164, 1654syl 19 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (♯‘(1...(⌊‘(𝑥 / 𝑛)))) = (⌊‘(𝑥 / 𝑛)))
167166oveq1d 7446 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((♯‘(1...(⌊‘(𝑥 / 𝑛)))) · (μ‘𝑛)) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
168162, 167eqtrd 2777 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = ((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
169168sumeq2dv 15738 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(μ‘𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)))
170148, 159, 1693eqtr3rd 2786 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛)) = 1)
171170oveq2d 7447 . . . . . . . . . 10 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((⌊‘(𝑥 / 𝑛)) · (μ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
172126, 141, 1713eqtr3d 2785 . . . . . . . . 9 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑥 · ((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
173123, 172eqtrd 2777 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1))
174173oveq1d 7446 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥))
175120, 32, 33divcan3d 12048 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((𝑥 · Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛))
176 rpcnne0 13053 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
177176adantr 480 . . . . . . . 8 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
178 divdir 11947 . . . . . . . 8 ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
17931, 81, 177, 178syl3anc 1373 . . . . . . 7 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) + 1) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
180174, 175, 1793eqtr3d 2785 . . . . . 6 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥)))
181180fveq2d 6910 . . . . 5 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) = (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
182121, 181eqled 11364 . . . 4 ((𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
183182adantl 481 . . 3 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) · (μ‘𝑛)) / 𝑥) + (1 / 𝑥))))
1841, 113, 114, 119, 183o1le 15689 . 2 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1))
185184mptru 1547 1 (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wa 395  w3a 1087   = wceq 1540  wtru 1541  wcel 2108  wne 2940  {crab 3436  Vcvv 3480  wss 3951   class class class wbr 5143  cmpt 5225  cfv 6561  (class class class)co 7431  f cof 7695  Fincfn 8985  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  cle 11296  cmin 11492   / cdiv 11920  cn 12266  0cn0 12526  cz 12613  cuz 12878  +crp 13034  ...cfz 13547  cfl 13830  chash 14369  abscabs 15273  𝑟 crli 15521  𝑂(1)co1 15522  Σcsu 15722  cdvds 16290  μcmu 27138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-ico 13393  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-o1 15526  df-lo1 15527  df-sum 15723  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-mu 27144
This theorem is referenced by:  mulogsumlem  27575  mulog2sumlem3  27580  selberglem1  27589
  Copyright terms: Public domain W3C validator