selberg4

Description: The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form sum_ i j k <_ x , Lam ( i ) Lam ( j ) Lam ( k ) ; we eliminate one of the nested sums by using the definition of psi ( x ) = sum_ k <_ x , Lam ( k ) . This statement can thus equivalently be written psi ( x ) log ^ 2 ( x ) = 2 sum_ i j k <_ x , Lam ( i ) Lam ( j ) Lam ( k ) + O ( x log x ) . Equation 10.4.23 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Assertion	selberg4	$⊢ (x \in (1, +∞) ⟼ \frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2	1	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ$
3		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
4	3	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
5		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
6	5	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
7	6	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
8	4 7	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
9	2 8	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
10		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
11		elfznn	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℕ$
12	11	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
13		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
14	12 13	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℝ$
15	4	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to x \in ℝ$
16	15 12	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \frac{x}{m} \in ℝ$
17		chpcl	$⊢ \frac{x}{m} \in ℝ \to ψ (\frac{x}{m}) \in ℝ$
18	16 17	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) \in ℝ$
19	14 18	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) ψ (\frac{x}{m}) \in ℝ$
20	12	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ^{+}$
21	20	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \log m \in ℝ$
22	19 21	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) ψ (\frac{x}{m}) \log m \in ℝ$
23	10 22	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m \in ℝ$
24	9 23	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m \in ℝ$
25	10 19	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \in ℝ$
26	24 25	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \in ℝ$
27		1rp	$⊢ 1 \in ℝ^{+}$
28	27	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
29		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
30	29 4 7	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
31	4 28 30	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
32	26 31	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x} \in ℝ$
33	32	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x} \in ℂ$
34		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
35	4 34	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \in ℝ$
36	31	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
37	35 36	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℝ$
38	37 25	readdcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \in ℝ$
39	38 31	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x} \in ℝ$
40	39	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x} \in ℂ$
41	2 36	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℝ$
42	41	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℂ$
43	33 40 42	addsubassd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x = (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x$
44	26	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \in ℂ$
45	38	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \in ℂ$
46	4	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
47	31	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
48	44 45 46 47	divdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{((\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})) + ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x} = (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x})$
49	24	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m \in ℂ$
50	25	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \in ℂ$
51	37	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℂ$
52	49 50 51	nppcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to ((\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})) + ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) = (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m + ψ (x) \log x$
53		elfznn	$⊢ n \in (1 \dots ⌊\frac{x}{m}⌋) \to n \in ℕ$
54	53	ad2antll	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to n \in ℕ$
55		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
56	54 55	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (n) \in ℝ$
57	14	adantrr	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (m) \in ℝ$
58	20	adantrr	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to m \in ℝ^{+}$
59	58	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to \log m \in ℝ$
60	57 59	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (m) \log m \in ℝ$
61	56 60	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (n) Λ (m) \log m \in ℝ$
62	61	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land (m \in (1 \dots ⌊x⌋) \land n \in (1 \dots ⌊\frac{x}{m}⌋))) \to Λ (n) Λ (m) \log m \in ℂ$
63	4 62	fsumfldivdiag	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (n) Λ (m) \log m$
64	14	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \in ℂ$
65	18	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) \in ℂ$
66	21	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \log m \in ℂ$
67	64 65 66	mul32d	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) ψ (\frac{x}{m}) \log m = Λ (m) \log m ψ (\frac{x}{m})$
68	64 66	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m \in ℂ$
69	68 65	mulcomd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) \log m ψ (\frac{x}{m}) = ψ (\frac{x}{m}) Λ (m) \log m$
70		chpval	$⊢ \frac{x}{m} \in ℝ \to ψ (\frac{x}{m}) = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n)$
71	16 70	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n)$
72	71	oveq1d	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) Λ (m) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
73		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{m}⌋) \in Fin$
74	56	anassrs	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land n \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (n) \in ℝ$
75	74	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \land n \in (1 \dots ⌊\frac{x}{m}⌋)) \to Λ (n) \in ℂ$
76	73 68 75	fsummulc1	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
77	72 76	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{m}) Λ (m) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
78	67 69 77	3eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to Λ (m) ψ (\frac{x}{m}) \log m = \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
79	78	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m = \sum_{m = 1}^{⌊x⌋} \sum_{n = 1}^{⌊\frac{x}{m}⌋} Λ (n) Λ (m) \log m$
80		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
81		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
82	81	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
83	82 55	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
84	83	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
85		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
86	85	adantl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
87	86 13	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℝ$
88	86	nnrpd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℝ^{+}$
89	88	relogcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m \in ℝ$
90	87 89	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \log m \in ℝ$
91	90	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \log m \in ℂ$
92	80 84 91	fsummulc2	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (n) Λ (m) \log m$
93	92	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (n) Λ (m) \log m$
94	63 79 93	3eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
95	94	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
96	95	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m + ψ (x) \log x = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x$
97	52 96	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to ((\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})) + ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x$
98	97	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{((\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})) + ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x} = \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}$
99	48 98	eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) = \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}$
100	99	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x = (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x$
101	43 100	eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x = (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x$
102	101	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x) = (x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x)$
103	39 41	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x \in ℝ$
104		selberg3lem2	$⊢ (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) \in 𝑂 (1)$
105	104	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) \in 𝑂 (1)$
106	31	ex	$⊢ ⊤ \to (x \in (1, +∞) \to x \in ℝ^{+})$
107	106	ssrdv	$⊢ ⊤ \to (1, +∞) \subseteq ℝ^{+}$
108		selberg2	$⊢ (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x) \in 𝑂 (1)$
109	108	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x) \in 𝑂 (1)$
110	107 109	o1res2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x) \in 𝑂 (1)$
111	32 103 105 110	o1add2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m}) \log m - \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) + (\frac{ψ (x) \log x + \sum_{m = 1}^{⌊x⌋} Λ (m) ψ (\frac{x}{m})}{x}) - 2 \log x) \in 𝑂 (1)$
112	102 111	eqeltrrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x) \in 𝑂 (1)$
113	80 90	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℝ$
114	83 113	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℝ$
115	10 114	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℝ$
116	9 115	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℝ$
117	116 37	readdcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x \in ℝ$
118	117 31	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x} \in ℝ$
119	118 41	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x \in ℝ$
120	119	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x \in ℂ$
121	4	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
122	121 82	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
123	122	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x}{n} \in ℝ$
124	123 86	nndivred	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{x}{n}}{m} \in ℝ$
125		chpcl	$⊢ \frac{\frac{x}{n}}{m} \in ℝ \to ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
126	124 125	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
127	87 126	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
128	80 127	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
129	83 128	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
130	10 129	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
131	9 130	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
132	37 131	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
133	132 31	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x} \in ℝ$
134	133	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x} \in ℂ$
135	116	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℂ$
136	131	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
137	51 135 136	pnncand	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - (ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
138	135 51	addcomd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x = ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m$
139	138	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x - (ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})) = ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m - (ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}))$
140	87	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℂ$
141	89	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m \in ℂ$
142	126	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
143	140 141 142	adddid	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = Λ (m) \log m + Λ (m) ψ (\frac{\frac{x}{n}}{m})$
144	143	sumeq2dv	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (Λ (m) \log m + Λ (m) ψ (\frac{\frac{x}{n}}{m}))$
145	127	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
146	80 91 145	fsumadd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (Λ (m) \log m + Λ (m) ψ (\frac{\frac{x}{n}}{m})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
147	144 146	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
148	147	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}))$
149	113	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℂ$
150	128	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
151	84 149 150	adddid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})) = Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
152	148 151	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
153	152	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}))$
154	114	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℂ$
155	129	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
156	10 154 155	fsumadd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})) = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
157	153 156	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
158	157	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}))$
159	9	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
160	115	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m \in ℂ$
161	130	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
162	159 160 161	adddid	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
163	158 162	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})$
164	137 139 163	3eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x - (ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))$
165	164	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x - (ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}))}{x} = \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}$
166	117	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x \in ℂ$
167	51 136	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
168	166 167 46 47	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x - (ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}))}{x} = (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x})$
169		2cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
170	89 126	readdcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log m + ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
171	87 170	remulcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
172	80 171	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
173	83 172	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
174	10 173	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℝ$
175	174	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℂ$
176	169 175	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m})) \in ℂ$
177	36	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
178	8	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
179	176 177 46 178 47	divdiv1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\log x}}{x} = \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\log x x}$
180	177 46	mulcomd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x x = x \log x$
181	180	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\log x x} = \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}$
182	179 181	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\log x}}{x} = \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}$
183	169 175 177 178	div23d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\log x} = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))$
184	183	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{\log x}}{x} = \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x}$
185	31 8	rpmulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℝ^{+}$
186	185	rpcnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℂ$
187	185	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \neq 0$
188	169 175 186 187	divassd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2 \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x} = 2 (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x})$
189	182 184 188	3eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x} = 2 (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x})$
190	165 168 189	3eqtr3d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x})$
191	190	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) - 2 \log x = 2 (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - 2 \log x$
192	118	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x} \in ℂ$
193	192 42 134	sub32d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) = (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) - 2 \log x$
194	174 185	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x} \in ℝ$
195	194	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x} \in ℂ$
196	169 195 177	subdid	$⊢ (⊤ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - 2 \log x$
197	191 193 196	3eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) = 2 ((\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x)$
198	197	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x})) = (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x))$
199	194 36	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x \in ℝ$
200		ioossre	$⊢ (1, +∞) \subseteq ℝ$
201		2cnd	$⊢ ⊤ \to 2 \in ℂ$
202		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 2 \in ℂ) \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
203	200 201 202	sylancr	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
204		selbergb	$⊢ \exists c \in ℝ^{+} \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq c$
205		simpl	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq c) \to c \in ℝ^{+}$
206		simpr	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq c) \to \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq c$
207	205 206	selberg4lem1	$⊢ (c \in ℝ^{+} \land \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq c) \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) \in 𝑂 (1)$
208	207	rexlimiva	$⊢ \exists c \in ℝ^{+} \forall y \in [1, +∞) \|(\frac{\sum_{i = 1}^{⌊y⌋} Λ (i) (\log i + ψ (\frac{y}{i}))}{y}) - 2 \log y\| \leq c \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) \in 𝑂 (1)$
209	204 208	mp1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x) \in 𝑂 (1)$
210	2 199 203 209	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\log m + ψ (\frac{\frac{x}{n}}{m}))}{x \log x}) - \log x)) \in 𝑂 (1)$
211	198 210	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x - (\frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x})) \in 𝑂 (1)$
212	120 134 211	o1dif	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) \log m + ψ (x) \log x}{x}) - 2 \log x) \in 𝑂 (1) \leftrightarrow (x \in (1, +∞) ⟼ \frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1))$
213	112 212	mpbid	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1)$
214	213	mptru	$⊢ (x \in (1, +∞) ⟼ \frac{ψ (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg4

Proof