selberglem2

		Ref	Expression
	Hypothesis	selberglem1.t	$⊢ T = \frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n}$
	Assertion	selberglem2	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 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		reex	$⊢ ℝ \in V$
3		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
4	2 3	ssexi	$⊢ ℝ^{+} \in V$
5	4	a1i	$⊢ ⊤ \to ℝ^{+} \in V$
6		fzfid	$⊢ (⊤ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
7		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
8	7	adantl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
9		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
10	8 9	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
11	10	zred	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
12	11	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
13		fzfid	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
14		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
15	14	adantl	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
16	15	nnrpd	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℝ^{+}$
17	16	relogcld	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m \in ℝ$
18	17	resqcld	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to {\log m}^{2} \in ℝ$
19	13 18	fsumrecl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} \in ℝ$
20		simplr	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
21	19 20	rerpdivcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x} \in ℝ$
22	21	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x} \in ℂ$
23		simpr	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
24	7	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
25		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
26	23 24 25	syl2an	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
27	26	relogcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
28	27	resqcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} \in ℝ$
29		2re	$⊢ 2 \in ℝ$
30		remulcl	$⊢ (2 \in ℝ \land \log (\frac{x}{n}) \in ℝ) \to 2 \log (\frac{x}{n}) \in ℝ$
31	29 27 30	sylancr	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 \log (\frac{x}{n}) \in ℝ$
32		resubcl	$⊢ (2 \in ℝ \land 2 \log (\frac{x}{n}) \in ℝ) \to 2 - 2 \log (\frac{x}{n}) \in ℝ$
33	29 31 32	sylancr	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 - 2 \log (\frac{x}{n}) \in ℝ$
34	28 33	readdcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℝ$
35	34 8	nndivred	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n} \in ℝ$
36	1 35	eqeltrid	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to T \in ℝ$
37	36	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to T \in ℂ$
38	22 37	subcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T \in ℂ$
39	12 38	mulcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) \in ℂ$
40	6 39	fsumcl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) \in ℂ$
41	12 37	mulcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) T \in ℂ$
42	6 41	fsumcl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) T \in ℂ$
43		2cn	$⊢ 2 \in ℂ$
44		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
45	44	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \in ℝ$
46	45	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \in ℂ$
47		mulcl	$⊢ (2 \in ℂ \land \log x \in ℂ) \to 2 \log x \in ℂ$
48	43 46 47	sylancr	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \log x \in ℂ$
49	42 48	subcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x \in ℂ$
50		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T))$
51		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x)$
52	5 40 49 50 51	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) +_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x)$
53	40 42 48	addsubassd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x = \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x$
54		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
55	54	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \in ℂ \land x \neq 0)$
56	55	simpld	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℂ$
57	11	adantr	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to μ (n) \in ℝ$
58	57 18	remulcld	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to μ (n) {\log m}^{2} \in ℝ$
59	13 58	fsumrecl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2} \in ℝ$
60	59	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2} \in ℂ$
61	55	simprd	$⊢ (⊤ \land x \in ℝ^{+}) \to x \neq 0$
62	6 56 60 61	fsumdivc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x})$
63	18	recnd	$⊢ (((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to {\log m}^{2} \in ℂ$
64	13 63	fsumcl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} \in ℂ$
65	55	adantr	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (x \in ℂ \land x \neq 0)$
66		divass	$⊢ (μ (n) \in ℂ \land \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{μ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x} = μ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x})$
67	12 64 65 66	syl3anc	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x} = μ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x})$
68	13 12 63	fsummulc2	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} = \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}$
69	68	oveq1d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x} = \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}$
70	22 37	npcand	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T + T = \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}$
71	70	oveq2d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T + T) = μ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x})$
72	12 38 37	adddid	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T + T) = μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + μ (n) T$
73	71 72	eqtr3d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) = μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + μ (n) T$
74	67 69 73	3eqtr3d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x} = μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + μ (n) T$
75	74	sumeq2dv	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) = \sum_{n = 1}^{⌊x⌋} (μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + μ (n) T)$
76	6 39 41	fsumadd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + μ (n) T) = \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T$
77	62 75 76	3eqtrrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T = \frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}$
78	77	oveq1d	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x = (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 2 \log x$
79	53 78	eqtr3d	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x = (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 2 \log x$
80	79	mpteq2dva	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) + \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) = (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 2 \log x)$
81	52 80	eqtrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) +_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) = (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 2 \log x)$
82		1red	$⊢ ⊤ \to 1 \in ℝ$
83	6 28	fsumrecl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} \in ℝ$
84	83 23	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x} \in ℝ$
85	84	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x} \in ℂ$
86		2cnd	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \in ℂ$
87		2nn0	$⊢ 2 \in ℕ_{0}$
88		logexprlim	$⊢ 2 \in ℕ_{0} \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) \underset{ℝ}{⇝} 2!$
89	87 88	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) \underset{ℝ}{⇝} 2!$
90		2cnd	$⊢ ⊤ \to 2 \in ℂ$
91		rlimconst	$⊢ (ℝ^{+} \subseteq ℝ \land 2 \in ℂ) \to (x \in ℝ^{+} ⟼ 2) \underset{ℝ}{⇝} 2$
92	3 90 91	sylancr	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 2) \underset{ℝ}{⇝} 2$
93	85 86 89 92	rlimadd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2) \underset{ℝ}{⇝} (2! + 2)$
94		rlimo1	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2) \underset{ℝ}{⇝} (2! + 2) \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2) \in 𝑂 (1)$
95	93 94	syl	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2) \in 𝑂 (1)$
96		readdcl	$⊢ (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x} \in ℝ \land 2 \in ℝ) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2 \in ℝ$
97	84 29 96	sylancl	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2 \in ℝ$
98	40	abscld	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \in ℝ$
99	97	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2 \in ℂ$
100	99	abscld	$⊢ (⊤ \land x \in ℝ^{+}) \to \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2\| \in ℝ$
101	39	abscld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \in ℝ$
102	6 101	fsumrecl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \in ℝ$
103	6 39	fsumabs	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq \sum_{n = 1}^{⌊x⌋} \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\|$
104		readdcl	$⊢ ({\log (\frac{x}{n})}^{2} \in ℝ \land 2 \in ℝ) \to {\log (\frac{x}{n})}^{2} + 2 \in ℝ$
105	28 29 104	sylancl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} + 2 \in ℝ$
106	105 20	rerpdivcld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{{\log (\frac{x}{n})}^{2} + 2}{x} \in ℝ$
107	6 106	fsumrecl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{{\log (\frac{x}{n})}^{2} + 2}{x}) \in ℝ$
108	38	abscld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \in ℝ$
109	12 38	absmuld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| = \|μ (n)\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
110	12	abscld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \in ℝ$
111		1red	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
112	38	absge0d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
113		mule1	$⊢ n \in ℕ \to \|μ (n)\| \leq 1$
114	8 113	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \leq 1$
115	110 111 108 112 114	lemul1ad	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \leq 1 \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
116	108	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \in ℂ$
117	116	mulid2d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| = \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
118	115 117	breqtrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \leq \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
119	109 118	eqbrtrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
120	65	simpld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
121	120 38	absmuld	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|x ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| = \|x\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
122	120 22 37	subdid	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) = x (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - x T$
123	65	simprd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \neq 0$
124	64 120 123	divcan2d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}$
125	34	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ$
126	8	nnrpd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
127		rpcnne0	$⊢ n \in ℝ^{+} \to (n \in ℂ \land n \neq 0)$
128	126 127	syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (n \in ℂ \land n \neq 0)$
129		divass	$⊢ (x \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{x ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))}{n} = x (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n})$
130	1	oveq2i	$⊢ x T = x (\frac{{\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n})}{n})$
131	129 130	eqtr4di	$⊢ (x \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{x ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))}{n} = x T$
132		div23	$⊢ (x \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{x ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))}{n} = (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
133	131 132	eqtr3d	$⊢ (x \in ℂ \land {\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}) \in ℂ \land (n \in ℂ \land n \neq 0)) \to x T = (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
134	120 125 128 133	syl3anc	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x T = (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
135	124 134	oveq12d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - x T = \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} - (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
136	122 135	eqtrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} - (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))$
137	136	fveq2d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|x ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| = \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} - (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))\|$
138		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
139		absid	$⊢ (x \in ℝ \land 0 \leq x) \to \|x\| = x$
140	20 138 139	3syl	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|x\| = x$
141	140	oveq1d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|x\| \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| = x \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
142	121 137 141	3eqtr3d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} - (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))\| = x \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\|$
143	8	nncnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
144	143	mulid2d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 n = n$
145		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
146	145	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ$
147		fznnfl	$⊢ x \in ℝ \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
148	146 147	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
149	148	simplbda	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \leq x$
150	144 149	eqbrtrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 n \leq x$
151	20	rpred	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
152	111 151 126	lemuldivd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
153	150 152	mpbid	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{n}$
154		log2sumbnd	$⊢ (\frac{x}{n} \in ℝ^{+} \land 1 \leq \frac{x}{n}) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} - (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))\| \leq {\log (\frac{x}{n})}^{2} + 2$
155	26 153 154	syl2anc	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2} - (\frac{x}{n}) ({\log (\frac{x}{n})}^{2} + 2 - 2 \log (\frac{x}{n}))\| \leq {\log (\frac{x}{n})}^{2} + 2$
156	142 155	eqbrtrrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \leq {\log (\frac{x}{n})}^{2} + 2$
157	108 105 20	lemuldiv2d	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (x \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \leq {\log (\frac{x}{n})}^{2} + 2 \leftrightarrow \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \leq \frac{{\log (\frac{x}{n})}^{2} + 2}{x})$
158	156 157	mpbid	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|(\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T\| \leq \frac{{\log (\frac{x}{n})}^{2} + 2}{x}$
159	101 108 106 119 158	letrd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq \frac{{\log (\frac{x}{n})}^{2} + 2}{x}$
160	6 101 106 159	fsumle	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq \sum_{n = 1}^{⌊x⌋} (\frac{{\log (\frac{x}{n})}^{2} + 2}{x})$
161	6 105	fsumrecl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ({\log (\frac{x}{n})}^{2} + 2) \in ℝ$
162		remulcl	$⊢ (x \in ℝ \land 2 \in ℝ) \to x \cdot 2 \in ℝ$
163	146 29 162	sylancl	$⊢ (⊤ \land x \in ℝ^{+}) \to x \cdot 2 \in ℝ$
164	83 163	readdcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2 \in ℝ$
165	28	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} \in ℂ$
166		2cnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
167	6 165 166	fsumadd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ({\log (\frac{x}{n})}^{2} + 2) = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + \sum_{n = 1}^{⌊x⌋} 2$
168		fsumconst	$⊢ ((1 \dots ⌊x⌋) \in Fin \land 2 \in ℂ) \to \sum_{n = 1}^{⌊x⌋} 2 = \|(1 \dots ⌊x⌋)\| \cdot 2$
169	6 43 168	sylancl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} 2 = \|(1 \dots ⌊x⌋)\| \cdot 2$
170	138	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
171		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
172		hashfz1	$⊢ ⌊x⌋ \in ℕ_{0} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
173	170 171 172	3syl	$⊢ (⊤ \land x \in ℝ^{+}) \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
174	173	oveq1d	$⊢ (⊤ \land x \in ℝ^{+}) \to \|(1 \dots ⌊x⌋)\| \cdot 2 = ⌊x⌋ \cdot 2$
175	169 174	eqtrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} 2 = ⌊x⌋ \cdot 2$
176	175	oveq2d	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + \sum_{n = 1}^{⌊x⌋} 2 = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + ⌊x⌋ \cdot 2$
177	167 176	eqtrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ({\log (\frac{x}{n})}^{2} + 2) = \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + ⌊x⌋ \cdot 2$
178		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
179	146 178	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℝ$
180	29	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \in ℝ$
181	179 180	remulcld	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ \cdot 2 \in ℝ$
182		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
183	146 182	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ \leq x$
184		2pos	$⊢ 0 < 2$
185	29 184	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
186	185	a1i	$⊢ (⊤ \land x \in ℝ^{+}) \to (2 \in ℝ \land 0 < 2)$
187		lemul1	$⊢ (⌊x⌋ \in ℝ \land x \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (⌊x⌋ \leq x \leftrightarrow ⌊x⌋ \cdot 2 \leq x \cdot 2)$
188	179 146 186 187	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to (⌊x⌋ \leq x \leftrightarrow ⌊x⌋ \cdot 2 \leq x \cdot 2)$
189	183 188	mpbid	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋ \cdot 2 \leq x \cdot 2$
190	181 163 83 189	leadd2dd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + ⌊x⌋ \cdot 2 \leq \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2$
191	177 190	eqbrtrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ({\log (\frac{x}{n})}^{2} + 2) \leq \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2$
192	161 164 23 191	lediv1dd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} ({\log (\frac{x}{n})}^{2} + 2)}{x} \leq \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2}{x}$
193	105	recnd	$⊢ ((⊤ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} + 2 \in ℂ$
194	6 56 193 61	fsumdivc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} ({\log (\frac{x}{n})}^{2} + 2)}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{{\log (\frac{x}{n})}^{2} + 2}{x})$
195	83	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} \in ℂ$
196	56 86	mulcld	$⊢ (⊤ \land x \in ℝ^{+}) \to x \cdot 2 \in ℂ$
197		divdir	$⊢ (\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} \in ℂ \land x \cdot 2 \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + (\frac{x \cdot 2}{x})$
198	195 196 55 197	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + (\frac{x \cdot 2}{x})$
199	86 56 61	divcan3d	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{x \cdot 2}{x} = 2$
200	199	oveq2d	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + (\frac{x \cdot 2}{x}) = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2$
201	198 200	eqtrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2} + x \cdot 2}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2$
202	192 194 201	3brtr3d	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{{\log (\frac{x}{n})}^{2} + 2}{x}) \leq (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2$
203	102 107 97 160 202	letrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} \|μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2$
204	98 102 97 103 203	letrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2$
205	97	leabsd	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2 \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2\|$
206	98 97 100 204 205	letrd	$⊢ (⊤ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2\|$
207	206	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)\| \leq \|(\frac{\sum_{n = 1}^{⌊x⌋} {\log (\frac{x}{n})}^{2}}{x}) + 2\|$
208	82 95 97 40 207	o1le	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) \in 𝑂 (1)$
209	1	selberglem1	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) \in 𝑂 (1)$
210		o1add	$⊢ ((x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) +_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) \in 𝑂 (1)$
211	208 209 210	sylancl	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) ((\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} {\log m}^{2}}{x}) - T)) +_{f} (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} μ (n) T - 2 \log x) \in 𝑂 (1)$
212	81 211	eqeltrrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 2 \log x) \in 𝑂 (1)$
213	212	mptru	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) {\log m}^{2}}{x}) - 2 \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberglem2

Proof