Metamath Proof Explorer

Theorem mudivsum

Description: Asymptotic formula for sum_ n <_ x , mmu ( n ) / n = O(1) . Equation 10.2.1 of Shapiro, p. 405. (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Assertion mudivsum ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 1red ⊢ ( ⊤ → 1 ∈ ℝ )
2 reex ⊢ ℝ ∈ V
3 rpssre ⊢ ℝ+ ⊆ ℝ
4 2 3 ssexi ⊢ ℝ+ ∈ V
5 4 a1i ⊢ ( ⊤ → ℝ+ ∈ V )
6 fzfid ⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
7 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
8 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
9 nndivre ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
10 7 8 9 syl2an ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
11 10 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
12 reflcl ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
13 10 12 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
15 11 14 subcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
16 8 adantl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
17 mucl ⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
18 16 17 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
19 18 zcnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
20 15 19 mulcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ )
21 6 20 fsumcl ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ )
22 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
23 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
24 21 22 23 divcld ⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ∈ ℂ )
25 24 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ∈ ℂ )
26 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ V )
27 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) )
28 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
29 5 25 26 27 28 offval2 ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
30 3 a1i ⊢ ( ⊤ → ℝ+ ⊆ ℝ )
31 21 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ )
32 22 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℂ )
33 23 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ≠ 0 )
34 31 32 33 absdivd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) / ( abs ‘ 𝑥 ) ) )
35 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
36 absid ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
37 35 36 syl ⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ 𝑥 ) = 𝑥 )
38 37 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
39 38 oveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) / ( abs ‘ 𝑥 ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) / 𝑥 ) )
40 34 39 eqtrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) / 𝑥 ) )
41 31 abscld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ∈ ℝ )
42 fzfid ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
43 20 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ )
44 43 abscld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ∈ ℝ )
45 42 44 fsumrecl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ∈ ℝ )
46 7 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
47 42 43 fsumabs ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) )
48 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
49 46 48 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
50 1red ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
51 15 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
52 fz1ssnn ⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ
53 52 a1i ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ )
54 53 sselda ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
55 54 17 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
56 55 zcnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
57 51 56 absmuld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) = ( ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( abs ‘ ( μ ‘ 𝑛 ) ) ) )
58 51 abscld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
59 56 abscld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑛 ) ) ∈ ℝ )
60 51 absge0d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
61 56 absge0d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( μ ‘ 𝑛 ) ) )
62 simpl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℝ+ )
63 8 nnrpd ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
64 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
65 62 63 64 syl2an ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
66 3 65 sselid ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
67 66 12 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
68 flle ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( 𝑥 / 𝑛 ) )
69 66 68 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( 𝑥 / 𝑛 ) )
70 67 66 69 abssubge0d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) )
71 fracle1 ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ 1 )
72 66 71 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ 1 )
73 70 72 eqbrtrd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ 1 )
74 mule1 ⊢ ( 𝑛 ∈ ℕ → ( abs ‘ ( μ ‘ 𝑛 ) ) ≤ 1 )
75 54 74 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑛 ) ) ≤ 1 )
76 58 50 59 50 60 61 73 75 lemul12ad ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( abs ‘ ( μ ‘ 𝑛 ) ) ) ≤ ( 1 · 1 ) )
77 1t1e1 ⊢ ( 1 · 1 ) = 1
78 76 77 breqtrdi ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( abs ‘ ( μ ‘ 𝑛 ) ) ) ≤ 1 )
79 57 78 eqbrtrd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ 1 )
80 42 44 50 79 fsumle ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 1 )
81 1cnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 1 ∈ ℂ )
82 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 1 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · 1 ) )
83 42 81 82 syl2anc ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 1 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · 1 ) )
84 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
85 7 84 sylan ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
86 85 nnnn0d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
87 hashfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
88 86 87 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
89 88 oveq1d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · 1 ) = ( ( ⌊ ‘ 𝑥 ) · 1 ) )
90 49 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
91 90 mulid1d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( ⌊ ‘ 𝑥 ) · 1 ) = ( ⌊ ‘ 𝑥 ) )
92 83 89 91 3eqtrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 1 = ( ⌊ ‘ 𝑥 ) )
93 80 92 breqtrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ ( ⌊ ‘ 𝑥 ) )
94 flle ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
95 46 94 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
96 45 49 46 93 95 letrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ 𝑥 )
97 41 45 46 47 96 letrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ 𝑥 )
98 32 mulid1d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 𝑥 · 1 ) = 𝑥 )
99 97 98 breqtrrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ ( 𝑥 · 1 ) )
100 1red ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 1 ∈ ℝ )
101 41 100 62 ledivmuld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) / 𝑥 ) ≤ 1 ↔ ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) ≤ ( 𝑥 · 1 ) ) )
102 99 101 mpbird ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ) / 𝑥 ) ≤ 1 )
103 40 102 eqbrtrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ≤ 1 )
104 103 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ≤ 1 )
105 30 25 1 1 104 elo1d ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ∈ 𝑂(1) )
106 ax-1cn ⊢ 1 ∈ ℂ
107 divrcnv ⊢ ( 1 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 )
108 106 107 ax-mp ⊢ ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0
109 rlimo1 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ 𝑂(1) )
110 108 109 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ 𝑂(1) )
111 o1add ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) ∈ 𝑂(1) )
112 105 110 111 syl2anc ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) ∈ 𝑂(1) )
113 29 112 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) ∈ 𝑂(1) )
114 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) ∈ V )
115 18 zred ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
116 115 16 nndivred ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
117 116 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
118 6 117 fsumcl ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
119 118 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
120 118 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
121 120 abscld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
122 117 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
123 42 32 122 fsummulc2 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
124 14 19 mulcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ )
125 124 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ )
126 42 43 125 fsumadd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ) )
127 11 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
128 14 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
129 127 128 npcand ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) = ( 𝑥 / 𝑛 ) )
130 129 oveq1d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) = ( ( 𝑥 / 𝑛 ) · ( μ ‘ 𝑛 ) ) )
131 51 128 56 adddird ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) = ( ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ) )
132 32 adantr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
133 54 nnrpd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
134 rpcnne0 ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
135 133 134 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
136 div23 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑥 · ( μ ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑥 / 𝑛 ) · ( μ ‘ 𝑛 ) ) )
137 divass ⊢ ( ( 𝑥 ∈ ℂ ∧ ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑥 · ( μ ‘ 𝑛 ) ) / 𝑛 ) = ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
138 136 137 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑥 / 𝑛 ) · ( μ ‘ 𝑛 ) ) = ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
139 132 56 135 138 syl3anc ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / 𝑛 ) · ( μ ‘ 𝑛 ) ) = ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
140 130 131 139 3eqtr3d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ) = ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
141 140 sumeq2dv ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
142 eqidd ⊢ ( 𝑘 = ( 𝑛 · 𝑚 ) → ( μ ‘ 𝑛 ) = ( μ ‘ 𝑛 ) )
143 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ℕ
144 simprr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } )
145 143 144 sselid ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ ℕ )
146 145 17 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
147 146 zcnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
148 142 46 147 dvdsflsumcom ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( μ ‘ 𝑛 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( μ ‘ 𝑛 ) )
149 147 3impb ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( μ ‘ 𝑛 ) ∈ ℂ )
150 149 mulid1d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( ( μ ‘ 𝑛 ) · 1 ) = ( μ ‘ 𝑛 ) )
151 150 2sumeq2dv ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( μ ‘ 𝑛 ) · 1 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( μ ‘ 𝑛 ) )
152 eqidd ⊢ ( 𝑘 = 1 → 1 = 1 )
153 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
154 85 153 eleqtrdi ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
155 eluzfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
156 154 155 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
157 1cnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
158 152 42 53 156 157 musumsum ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( μ ‘ 𝑛 ) · 1 ) = 1 )
159 151 158 eqtr3d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( μ ‘ 𝑛 ) = 1 )
160 fzfid ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
161 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin ∧ ( μ ‘ 𝑛 ) ∈ ℂ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( μ ‘ 𝑛 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( μ ‘ 𝑛 ) ) )
162 160 56 161 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( μ ‘ 𝑛 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( μ ‘ 𝑛 ) ) )
163 rprege0 ⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 / 𝑛 ) ) )
164 flge0nn0 ⊢ ( ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 / 𝑛 ) ) → ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℕ0 )
165 hashfz1 ⊢ ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) )
166 65 163 164 165 4syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) )
167 166 oveq1d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( μ ‘ 𝑛 ) ) = ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) )
168 162 167 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( μ ‘ 𝑛 ) = ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) )
169 168 sumeq2dv ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( μ ‘ 𝑛 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) )
170 148 159 169 3eqtr3rd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) = 1 )
171 170 oveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) · ( μ ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + 1 ) )
172 126 141 171 3eqtr3d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + 1 ) )
173 123 172 eqtrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + 1 ) )
174 173 oveq1d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + 1 ) / 𝑥 ) )
175 120 32 33 divcan3d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( 𝑥 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) )
176 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
177 176 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
178 divdir ⊢ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + 1 ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
179 31 81 177 178 syl3anc ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) + 1 ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
180 174 175 179 3eqtr3d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
181 180 fveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) = ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
182 121 181 eqled ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ≤ ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
183 182 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ≤ ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑥 / 𝑛 ) − ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) · ( μ ‘ 𝑛 ) ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
184 1 113 114 119 183 o1le ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) )
185 184 mptru ⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1)