mulogsum

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

		Ref	Expression
	Assertion	mulogsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
2		ax-1cn	$⊢ 1 \in ℂ$
3		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 1 \in ℂ) \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
4	1 2 3	mp2an	$⊢ (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
5		1cnd	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 \in ℂ$
6		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
7		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
8	7	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
9		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
10	8 9	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
11	10	zred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
12	11 8	nndivred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
13	7	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
14		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
15	13 14	sylan2	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
16	15	relogcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
17	12 16	remulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℝ$
18	17	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
19	6 18	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
20	19	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
21		mulogsumlem	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))) \in 𝑂 (1)$
22		sumex	$⊢ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in V$
23	22	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in V$
24	21	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))) \in 𝑂 (1)$
25	23 24	o1mptrcl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) \in ℂ$
26	5 20	subcld	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
27		1red	$⊢ ⊤ \to 1 \in ℝ$
28		fz1ssnn	$⊢ (1 \dots ⌊x⌋) \subseteq ℕ$
29	28	a1i	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to (1 \dots ⌊x⌋) \subseteq ℕ$
30	29	sselda	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
31	30 9	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
32	31	zred	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
33	32 30	nndivred	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
34	33	recnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
35		fzfid	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
36		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
37	36	adantl	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
38	37	nnrpd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℝ^{+}$
39	38	rpcnne0d	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (m \in ℂ \land m \neq 0)$
40		reccl	$⊢ (m \in ℂ \land m \neq 0) \to \frac{1}{m} \in ℂ$
41	39 40	syl	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{1}{m} \in ℂ$
42	35 41	fsumcl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \in ℂ$
43		simpl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \in ℝ^{+}$
44	43 13 14	syl2an	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
45	44	relogcld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
46	45	recnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
47	34 42 46	subdid	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) = (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})$
48	47	sumeq2dv	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\frac{μ (n)}{n}) \log (\frac{x}{n}))$
49		fzfid	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to (1 \dots ⌊x⌋) \in Fin$
50	34 42	mulcld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) \in ℂ$
51	18	adantlr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
52	49 50 51	fsumsub	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})$
53		oveq2	$⊢ k = n m \to \frac{1}{k} = \frac{1}{n m}$
54	53	oveq2d	$⊢ k = n m \to μ (n) (\frac{1}{k}) = μ (n) (\frac{1}{n m})$
55		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
56	55	adantr	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to x \in ℝ$
57		ssrab2	$⊢ \{y \in ℕ \| y ∥ k\} \subseteq ℕ$
58		simprr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in \{y \in ℕ \| y ∥ k\}$
59	57 58	sseldi	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in ℕ$
60	59 9	syl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) \in ℤ$
61	60	zcnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) \in ℂ$
62		elfznn	$⊢ k \in (1 \dots ⌊x⌋) \to k \in ℕ$
63	62	adantl	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land k \in (1 \dots ⌊x⌋)) \to k \in ℕ$
64	63	nnrecred	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land k \in (1 \dots ⌊x⌋)) \to \frac{1}{k} \in ℝ$
65	64	recnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land k \in (1 \dots ⌊x⌋)) \to \frac{1}{k} \in ℂ$
66	65	adantrr	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to \frac{1}{k} \in ℂ$
67	61 66	mulcld	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) (\frac{1}{k}) \in ℂ$
68	54 56 67	dvdsflsumcom	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) (\frac{1}{k}) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{1}{n m})$
69		oveq2	$⊢ k = 1 \to \frac{1}{k} = \frac{1}{1}$
70		1div1e1	$⊢ \frac{1}{1} = 1$
71	69 70	eqtrdi	$⊢ k = 1 \to \frac{1}{k} = 1$
72		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
73	55 72	sylan	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℕ$
74		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
75	73 74	eleqtrdi	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to ⌊x⌋ \in ℤ_{\geq 1}$
76		eluzfz1	$⊢ ⌊x⌋ \in ℤ_{\geq 1} \to 1 \in (1 \dots ⌊x⌋)$
77	75 76	syl	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to 1 \in (1 \dots ⌊x⌋)$
78	71 49 29 77 65	musumsum	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) (\frac{1}{k}) = 1$
79	31	zcnd	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
80	79	adantr	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to μ (n) \in ℂ$
81	30	adantr	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℕ$
82	81	nnrpd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℝ^{+}$
83	82	rpcnne0d	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (n \in ℂ \land n \neq 0)$
84		divdiv1	$⊢ (μ (n) \in ℂ \land (n \in ℂ \land n \neq 0) \land (m \in ℂ \land m \neq 0)) \to \frac{\frac{μ (n)}{n}}{m} = \frac{μ (n)}{n m}$
85	80 83 39 84	syl3anc	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{μ (n)}{n}}{m} = \frac{μ (n)}{n m}$
86	34	adantr	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{μ (n)}{n} \in ℂ$
87	37	nncnd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℂ$
88	37	nnne0d	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \neq 0$
89	86 87 88	divrecd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{μ (n)}{n}}{m} = (\frac{μ (n)}{n}) (\frac{1}{m})$
90		nnmulcl	$⊢ (n \in ℕ \land m \in ℕ) \to n m \in ℕ$
91	30 36 90	syl2an	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n m \in ℕ$
92	91	nncnd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n m \in ℂ$
93	91	nnne0d	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n m \neq 0$
94	80 92 93	divrecd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{μ (n)}{n m} = μ (n) (\frac{1}{n m})$
95	85 89 94	3eqtr3rd	$⊢ (((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to μ (n) (\frac{1}{n m}) = (\frac{μ (n)}{n}) (\frac{1}{m})$
96	95	sumeq2dv	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{1}{n m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{μ (n)}{n}) (\frac{1}{m})$
97	35 34 41	fsummulc2	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{μ (n)}{n}) (\frac{1}{m})$
98	96 97	eqtr4d	$⊢ ((x \in ℝ^{+} \land 1 \leq x) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{1}{n m}) = (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m})$
99	98	sumeq2dv	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{1}{n m}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m})$
100	68 78 99	3eqtr3rd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) = 1$
101	100	oveq1d	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) = 1 - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})$
102	48 52 101	3eqtrd	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) = 1 - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})$
103	102	adantl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n})) = 1 - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})$
104	25 26 27 103	o1eq	$⊢ ⊤ \to ((x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{1}{m}) - \log (\frac{x}{n}))) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ 1 - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1))$
105	21 104	mpbii	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 1 - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
106	5 20 105	o1dif	$⊢ ⊤ \to ((x \in ℝ^{+} ⟼ 1) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1))$
107	4 106	mpbii	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
108	107	mptru	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem mulogsum

Proof