selberglem1

Description: Lemma for selberg . Estimation of the asymptotic part of selberglem3 . (Contributed by Mario Carneiro, 20-May-2016)

		Ref	Expression
	Hypothesis	selberglem1.t	$⊢ T = \frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n}$
	Assertion	selberglem1	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		selberglem1.t	$⊢ T = \frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n}$
2		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
3		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
4	3	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
5		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
6	4 5	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
7	6	zred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
8	7 4	nndivred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
9	8	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
10	3	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
11		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
12	10 11	sylan2	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
13		relogcl	$⊢ \frac{x}{n} \in ℝ^{+} \to \log (\frac{x}{n}) \in ℝ$
14	12 13	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
15	14	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
16	15	sqcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} \in ℂ$
17	9 16	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} \in ℂ$
18	2 17	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} \in ℂ$
19		2cn	$⊢ 2 \in ℂ$
20	19	a1i	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
21	20 15	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 \log (\frac{x}{n}) \in ℂ$
22	20 21	subcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 - 2 \log (\frac{x}{n}) \in ℂ$
23	9 22	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n})) \in ℂ$
24	2 23	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n})) \in ℂ$
25		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
26	25	recnd	$⊢ x \in ℝ^{+} \to \log x \in ℂ$
27		mulcl	$⊢ (2 \in ℂ \land \log x \in ℂ) \to 2 \log x \in ℂ$
28	19 26 27	sylancr	$⊢ x \in ℝ^{+} \to 2 \log x \in ℂ$
29	18 24 28	addsubd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n})) - 2 \log x = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
30	1	oveq2i	$⊢ μ (n) T = μ (n) (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n})$
31	6	zcnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
32	16 22	addcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ$
33	4	nnrpd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
34	33	rpcnne0d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (n \in ℂ \land n \neq 0)$
35		divass	$⊢ (μ (n) \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{μ (n) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))}{n} = μ (n) (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n})$
36		div23	$⊢ (μ (n) \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{μ (n) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))}{n} = (\frac{μ (n)}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
37	35 36	eqtr3d	$⊢ (μ (n) \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to μ (n) (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n}) = (\frac{μ (n)}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
38	31 32 34 37	syl3anc	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n}) = (\frac{μ (n)}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
39	9 16 22	adddid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})) = (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
40	38 39	eqtrd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n}) = (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
41	30 40	syl5eq	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to μ (n) T = (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
42	41	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} μ (n) T = \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n})))$
43	2 17 23	fsumadd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
44	42 43	eqtrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} μ (n) T = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
45	44	oveq1d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} + \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n})) - 2 \log x$
46	19	a1i	$⊢ x \in ℝ^{+} \to 2 \in ℂ$
47	9 15	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
48	9 47	subcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
49	2 46 48	fsummulc2	$⊢ x \in ℝ^{+} \to 2 \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} 2 ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n}))$
50	2 9 47	fsumsub	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})$
51	50	oveq2d	$⊢ x \in ℝ^{+} \to 2 \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))$
52	20 9	mulcomd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{μ (n)}{n}) = (\frac{μ (n)}{n}) \cdot 2$
53	20 9 15	mul12d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{μ (n)}{n}) \log (\frac{x}{n}) = (\frac{μ (n)}{n}) 2 \log (\frac{x}{n})$
54	52 53	oveq12d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{μ (n)}{n}) - 2 (\frac{μ (n)}{n}) \log (\frac{x}{n}) = (\frac{μ (n)}{n}) \cdot 2 - (\frac{μ (n)}{n}) 2 \log (\frac{x}{n})$
55	20 9 47	subdid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = 2 (\frac{μ (n)}{n}) - 2 (\frac{μ (n)}{n}) \log (\frac{x}{n})$
56	9 20 21	subdid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n})) = (\frac{μ (n)}{n}) \cdot 2 - (\frac{μ (n)}{n}) 2 \log (\frac{x}{n})$
57	54 55 56	3eqtr4d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to 2 ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
58	57	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} 2 ((\frac{μ (n)}{n}) - (\frac{μ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
59	49 51 58	3eqtr3d	$⊢ x \in ℝ^{+} \to 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
60	59	oveq2d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (2 - 2 \log (\frac{x}{n}))$
61	29 45 60	3eqtr4d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))$
62	61	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})))$
63		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x \in V$
64		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in V$
65		mulog2sum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$
66	65	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$
67		2ex	$⊢ 2 \in V$
68	67	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \in V$
69		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in V$
70		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
71		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 2 \in ℂ) \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
72	70 19 71	mp2an	$⊢ (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
73	72	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
74		reex	$⊢ ℝ \in V$
75	74 70	ssexi	$⊢ ℝ^{+} \in V$
76	75	a1i	$⊢ ⊤ \to ℝ^{+} \in V$
77		sumex	$⊢ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in V$
78	77	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in V$
79		sumex	$⊢ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in V$
80	79	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in V$
81		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}))$
82		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))$
83	76 78 80 81 82	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))$
84		mudivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$
85		mulogsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
86		o1sub	$⊢ ((x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
87	84 85 86	mp2an	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) -_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
88	83 87	eqeltrrdi	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
89	68 69 73 88	o1mul2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))) \in 𝑂 (1)$
90	63 64 66 89	o1add2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))) \in 𝑂 (1)$
91	90	mptru	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x + 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}))) \in 𝑂 (1)$
92	62 91	eqeltri	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberglem1

Proof