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	mulridd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 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	mulridd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 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	mulridd	⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 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)