mulog2sumlem3

	Ref	Expression
Hypotheses	logdivsum.1	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
	mulog2sumlem.1	$⊢ φ \to F \underset{ℝ}{⇝} L$
Assertion	mulog2sumlem3	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		logdivsum.1	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
2		mulog2sumlem.1	$⊢ φ \to F \underset{ℝ}{⇝} L$
3		2cn	$⊢ 2 \in ℂ$
4	3	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
5		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
6		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
7	6	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
8		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
9	7 8	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
10	9	zred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
11	10 7	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
12	11	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
13		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
14	6	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
15		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
16	13 14 15	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
17	16	relogcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
18	17	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
19	18	sqcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} \in ℂ$
20	19	halfcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{{\log (\frac{x}{n})}^{2}}{2} \in ℂ$
21	12 20	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) \in ℂ$
22	5 21	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) \in ℂ$
23		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
24	23	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
25	24	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
26	4 22 25	subdid	$⊢ (φ \land x \in ℝ^{+}) \to 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x) = 2 \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - 2 \log x$
27	5 4 21	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) = \sum_{n = 1}^{⌊x⌋} 2 (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2})$
28	3	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
29	28 12 20	mul12d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) = (\frac{μ (n)}{n}) 2 (\frac{{\log (\frac{x}{n})}^{2}}{2})$
30		2ne0	$⊢ 2 \neq 0$
31	30	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 \neq 0$
32	19 28 31	divcan2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{{\log (\frac{x}{n})}^{2}}{2}) = {\log (\frac{x}{n})}^{2}$
33	32	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) 2 (\frac{{\log (\frac{x}{n})}^{2}}{2}) = (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2}$
34	29 33	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) = (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2}$
35	34	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} 2 (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2}$
36	27 35	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2}$
37	36	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - 2 \log x = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x$
38	26 37	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x$
39	38	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x)$
40	22 25	subcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x \in ℂ$
41		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
42		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 2 \in ℂ) \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
43	41 3 42	mp2an	$⊢ (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
44	43	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
45		emre	$⊢ γ \in ℝ$
46	45	recni	$⊢ γ \in ℂ$
47		mulcl	$⊢ (γ \in ℂ \land \log (\frac{x}{n}) \in ℂ) \to γ \log (\frac{x}{n}) \in ℂ$
48	46 18 47	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \log (\frac{x}{n}) \in ℂ$
49		rlimcl	$⊢ F \underset{ℝ}{⇝} L \to L \in ℂ$
50	2 49	syl	$⊢ φ \to L \in ℂ$
51	50	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to L \in ℂ$
52	48 51	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \log (\frac{x}{n}) - L \in ℂ$
53	20 52	addcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L \in ℂ$
54	12 53	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) \in ℂ$
55	5 54	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) \in ℂ$
56	12 52	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) \in ℂ$
57	5 56	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) \in ℂ$
58	55 25 57	sub32d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \log x - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) - \log x$
59	5 54 56	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)$
60	12 53 52	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + (γ \log (\frac{x}{n}) - L) - (γ \log (\frac{x}{n}) - L)) = (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)$
61	20 52	pncand	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{{\log (\frac{x}{n})}^{2}}{2}) + (γ \log (\frac{x}{n}) - L) - (γ \log (\frac{x}{n}) - L) = \frac{{\log (\frac{x}{n})}^{2}}{2}$
62	61	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + (γ \log (\frac{x}{n}) - L) - (γ \log (\frac{x}{n}) - L)) = (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2})$
63	60 62	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) = (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2})$
64	63	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2})$
65	59 64	eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2})$
66	65	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) - \log x = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x$
67	58 66	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \log x - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x$
68	67	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \log x - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x)$
69	55 25	subcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \log x \in ℂ$
70		eqid	$⊢ (\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L = (\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L$
71		eqid	$⊢ (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m}) = (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
72	1 2 70 71	mulog2sumlem2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \log x) \in 𝑂 (1)$
73	46	a1i	$⊢ (φ \land x \in ℝ^{+}) \to γ \in ℂ$
74	12 18	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
75	5 73 74	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} γ (\frac{μ (n)}{n}) \log (\frac{x}{n})$
76	50	adantr	$⊢ (φ \land x \in ℝ^{+}) \to L \in ℂ$
77	5 76 12	fsummulc1	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L$
78	75 77	oveq12d	$⊢ (φ \land x \in ℝ^{+}) \to γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L = \sum_{n = 1}^{⌊x⌋} γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L$
79		mulcl	$⊢ (γ \in ℂ \land (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ) \to γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
80	46 74 79	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
81	12 51	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) L \in ℂ$
82	5 80 81	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) - (\frac{μ (n)}{n}) L) = \sum_{n = 1}^{⌊x⌋} γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L$
83	46	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \in ℂ$
84	83 12 18	mul12d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) = (\frac{μ (n)}{n}) γ \log (\frac{x}{n})$
85	84	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) - (\frac{μ (n)}{n}) L = (\frac{μ (n)}{n}) γ \log (\frac{x}{n}) - (\frac{μ (n)}{n}) L$
86	12 48 51	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L) = (\frac{μ (n)}{n}) γ \log (\frac{x}{n}) - (\frac{μ (n)}{n}) L$
87	85 86	eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) - (\frac{μ (n)}{n}) L = (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)$
88	87	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (γ (\frac{μ (n)}{n}) \log (\frac{x}{n}) - (\frac{μ (n)}{n}) L) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)$
89	78 82 88	3eqtr2d	$⊢ (φ \land x \in ℝ^{+}) \to γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)$
90	89	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L))$
91	5 74	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
92		mulcl	$⊢ (γ \in ℂ \land \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ) \to γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
93	46 91 92	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) \in ℂ$
94	5 12	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \in ℂ$
95	94 76	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L \in ℂ$
96	46	a1i	$⊢ φ \to γ \in ℂ$
97		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land γ \in ℂ) \to (x \in ℝ^{+} ⟼ γ) \in 𝑂 (1)$
98	41 96 97	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ γ) \in 𝑂 (1)$
99		mulogsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
100	99	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
101	73 91 98 100	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n})) \in 𝑂 (1)$
102		mudivsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$
103	102	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n})) \in 𝑂 (1)$
104		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land L \in ℂ) \to (x \in ℝ^{+} ⟼ L) \in 𝑂 (1)$
105	41 50 104	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ L) \in 𝑂 (1)$
106	94 76 103 105	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L) \in 𝑂 (1)$
107	93 95 101 106	o1sub2	$⊢ φ \to (x \in ℝ^{+} ⟼ γ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \log (\frac{x}{n}) - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) L) \in 𝑂 (1)$
108	90 107	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)) \in 𝑂 (1)$
109	69 57 72 108	o1sub2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L) - \log x - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (γ \log (\frac{x}{n}) - L)) \in 𝑂 (1)$
110	68 109	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x) \in 𝑂 (1)$
111	4 40 44 110	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 (\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) (\frac{{\log (\frac{x}{n})}^{2}}{2}) - \log x)) \in 𝑂 (1)$
112	39 111	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) {\log (\frac{x}{n})}^{2} - 2 \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem mulog2sumlem3

Proof