selberg4r

Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of Shapiro, p. 430. (Contributed by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Hypothesis	pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	selberg4r	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
3	2	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
4		1rp	$⊢ 1 \in ℝ^{+}$
5	4	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
6		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
7		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
8	7	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
9	8	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
10	6 3 9	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
11	3 5 10	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
12	1	pntrval	$⊢ x \in ℝ^{+} \to R (x) = ψ (x) - x$
13	11 12	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) = ψ (x) - x$
14	13	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x = (ψ (x) - x) \log x$
15		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
16	3 15	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \in ℝ$
17	16	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \in ℂ$
18	3	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
19	11	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
20	19	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
21	17 18 20	subdird	$⊢ (⊤ \land x \in (1, +∞)) \to (ψ (x) - x) \log x = ψ (x) \log x - x \log x$
22	14 21	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x = ψ (x) \log x - x \log x$
23	11	ad2antrr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to x \in ℝ^{+}$
24		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
25	24	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
26	25	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
27	26	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℝ^{+}$
28	23 27	rpdivcld	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x}{n} \in ℝ^{+}$
29		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
30	29	adantl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℕ$
31	30	nnrpd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℝ^{+}$
32	28 31	rpdivcld	$⊢ (((⊤ \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 ℝ^{+}$
33	1	pntrval	$⊢ \frac{\frac{x}{n}}{m} \in ℝ^{+} \to R (\frac{\frac{x}{n}}{m}) = ψ (\frac{\frac{x}{n}}{m}) - (\frac{\frac{x}{n}}{m})$
34	32 33	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to R (\frac{\frac{x}{n}}{m}) = ψ (\frac{\frac{x}{n}}{m}) - (\frac{\frac{x}{n}}{m})$
35	34	oveq2d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) R (\frac{\frac{x}{n}}{m}) = Λ (m) (ψ (\frac{\frac{x}{n}}{m}) - (\frac{\frac{x}{n}}{m}))$
36		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
37	30 36	syl	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℝ$
38	37	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) \in ℂ$
39	3	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
40	39 25	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
41	40	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x}{n} \in ℝ$
42	41 30	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 ℝ$
43		chpcl	$⊢ \frac{\frac{x}{n}}{m} \in ℝ \to ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
44	42 43	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 ℝ$
45	44	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 ℂ$
46	42	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 ℂ$
47	38 45 46	subdid	$⊢ (((⊤ \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}) - (\frac{\frac{x}{n}}{m})) = Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (m) (\frac{\frac{x}{n}}{m})$
48	35 47	eqtrd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to Λ (m) R (\frac{\frac{x}{n}}{m}) = Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (m) (\frac{\frac{x}{n}}{m})$
49	48	sumeq2dv	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (m) (\frac{\frac{x}{n}}{m}))$
50		fzfid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
51	37 44	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 ℝ$
52	51	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 ℂ$
53	38 46	mulcld	$⊢ (((⊤ \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 ℂ$
54	50 52 53	fsumsub	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (m) (\frac{\frac{x}{n}}{m})) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})$
55	49 54	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})$
56	55	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}))$
57		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
58	25 57	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
59	58	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
60	50 51	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 ℝ$
61	60	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 ℂ$
62	50 53	fsumcl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}) \in ℂ$
63	59 61 62	subdid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})) = Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})$
64	56 63	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})$
65	64	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) - Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}))$
66		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
67	58 60	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 ℝ$
68	67	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 ℂ$
69	59 62	mulcld	$⊢ ((⊤ \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 ℂ$
70	66 68 69	fsumsub	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{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) ψ (\frac{\frac{x}{n}}{m}) - \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})$
71	65 70	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = \sum_{n = 1}^{⌊x⌋} Λ (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) (\frac{\frac{x}{n}}{m})$
72	71	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} Λ (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) (\frac{\frac{x}{n}}{m}))$
73		2re	$⊢ 2 \in ℝ$
74	73	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ$
75	3 9	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
76	74 75	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
77	76	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
78	66 67	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℝ$
79	78	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) ψ (\frac{\frac{x}{n}}{m}) \in ℂ$
80	66 69	fsumcl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}) \in ℂ$
81	77 79 80	subdid	$⊢ (⊤ \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}) - \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) ψ (\frac{\frac{x}{n}}{m}) - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})$
82	72 81	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m}) = (\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) (\frac{\frac{x}{n}}{m})$
83	22 82	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{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) (\frac{\frac{x}{n}}{m}))$
84	16 19	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℝ$
85	84	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℂ$
86	18 20	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℂ$
87	76 78	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 ℝ$
88	87	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 ℂ$
89	77 80	mulcld	$⊢ (⊤ \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 ℂ$
90	85 86 88 89	sub4d	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (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) (\frac{\frac{x}{n}}{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}) - (x \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}))$
91	83 90	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{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}) - (x \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}))$
92	91	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m})}{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 \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}))}{x}$
93	84 87	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 ℝ$
94	93	recnd	$⊢ (⊤ \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 ℂ$
95	3 19	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℝ$
96	37 42	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 ℝ$
97	50 96	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 ℝ$
98	58 97	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 ℝ$
99	66 98	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}) \in ℝ$
100	76 99	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 ℝ$
101	95 100	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 ℝ$
102	101	recnd	$⊢ (⊤ \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 ℂ$
103	11	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
104	94 102 18 103	divsubdird	$⊢ (⊤ \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 \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{ψ (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{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})$
105	95	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℂ$
106	99	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m}) \in ℂ$
107	77 106	mulcld	$⊢ (⊤ \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 ℂ$
108	105 107 18 103	divsubdird	$⊢ (⊤ \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} = (\frac{x \log x}{x}) - (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x})$
109	20 18 103	divcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x \log x}{x} = \log x$
110	77 106 18 103	divassd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = (\frac{2}{\log x}) (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x})$
111	98	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 ℂ$
112	66 18 111 103	fsumdivc	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x})$
113	41	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x}{n} \in ℂ$
114	30	nncnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℂ$
115	30	nnne0d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \neq 0$
116	113 38 114 115	div12d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (\frac{x}{n}) (\frac{Λ (m)}{m}) = Λ (m) (\frac{\frac{x}{n}}{m})$
117	18	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
118	117	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to x \in ℂ$
119	25	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
120	119	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℂ$
121	37 30	nndivred	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (m)}{m} \in ℝ$
122	121	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (m)}{m} \in ℂ$
123	25	nnne0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
124	123	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \neq 0$
125	118 120 122 124	div32d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (\frac{x}{n}) (\frac{Λ (m)}{m}) = x (\frac{\frac{Λ (m)}{m}}{n})$
126	116 125	eqtr3d	$⊢ (((⊤ \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}) = x (\frac{\frac{Λ (m)}{m}}{n})$
127	126	oveq1d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (m) (\frac{\frac{x}{n}}{m})}{x} = \frac{x (\frac{\frac{Λ (m)}{m}}{n})}{x}$
128	25	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to n \in ℕ$
129	121 128	nndivred	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{Λ (m)}{m}}{n} \in ℝ$
130	129	recnd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{Λ (m)}{m}}{n} \in ℂ$
131	103	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \neq 0$
132	131	adantr	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to x \neq 0$
133	130 118 132	divcan3d	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x (\frac{\frac{Λ (m)}{m}}{n})}{x} = \frac{\frac{Λ (m)}{m}}{n}$
134	127 133	eqtrd	$⊢ (((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{Λ (m) (\frac{\frac{x}{n}}{m})}{x} = \frac{\frac{Λ (m)}{m}}{n}$
135	134	sumeq2dv	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m) (\frac{\frac{x}{n}}{m})}{x}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\frac{Λ (m)}{m}}{n})$
136	96	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 ℂ$
137	50 117 136 131	fsumdivc	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m) (\frac{\frac{x}{n}}{m})}{x})$
138	50 119 122 123	fsumdivc	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{n} = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\frac{Λ (m)}{m}}{n})$
139	135 137 138	3eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = \frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{n}$
140	139	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x}) = Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{n})$
141	97	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 ℂ$
142	59 141 117 131	divassd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x})$
143	50 121	fsumrecl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
144	143	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℂ$
145	59 119 144 123	div32d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) = Λ (n) (\frac{\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{n})$
146	140 142 145	3eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
147	146	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x}) = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
148	112 147	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
149	148	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
150	110 149	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) (\frac{\frac{x}{n}}{m})}{x} = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
151	109 150	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{x \log x}{x}) - (\frac{(\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⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
152	108 151	eqtrd	$⊢ (⊤ \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} = \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
153	152	oveq2d	$⊢ (⊤ \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}) - (\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{ψ (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⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}))$
154	94 18 103	divcld	$⊢ (⊤ \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 ℂ$
155	58 25	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
156	155 143	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
157	66 156	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
158	76 157	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℝ$
159	158	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℂ$
160	154 20 159	subsub2d	$⊢ (⊤ \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}) - (\log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})) = (\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{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x$
161	153 160	eqtrd	$⊢ (⊤ \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}) - (\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{ψ (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{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x$
162	104 161	eqtrd	$⊢ (⊤ \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 \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{ψ (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{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x$
163	92 162	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m})}{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{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x$
164	163	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m})}{x}) = (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}) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x)$
165	93 11	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 ℝ$
166	158 19	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x \in ℝ$
167		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)$
168	167	a1i	$⊢ ⊤ \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)$
169		2cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
170	157 75	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x} \in ℝ$
171	170	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x} \in ℂ$
172	19	rehalfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℝ$
173	172	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
174	169 171 173	subdid	$⊢ (⊤ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - 2 (\frac{\log x}{2})$
175	157	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) \in ℂ$
176	75	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
177	169 20 175 176	div32d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x})$
178	177	eqcomd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})$
179		2ne0	$⊢ 2 \neq 0$
180	179	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \neq 0$
181	20 169 180	divcan2d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 (\frac{\log x}{2}) = \log x$
182	178 181	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - 2 (\frac{\log x}{2}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x$
183	174 182	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x$
184	183	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}))) = (x \in (1, +∞) ⟼ (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x)$
185	170 172	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}) \in ℝ$
186		ioossre	$⊢ (1, +∞) \subseteq ℝ$
187		2cnd	$⊢ ⊤ \to 2 \in ℂ$
188		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 2 \in ℂ) \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
189	186 187 188	sylancr	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
190		2vmadivsum	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
191	190	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
192	74 185 189 191	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m})}{\log x}) - (\frac{\log x}{2}))) \in 𝑂 (1)$
193	184 192	eqeltrrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x) \in 𝑂 (1)$
194	165 166 168 193	o1add2	$⊢ ⊤ \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}) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{Λ (m)}{m}) - \log x) \in 𝑂 (1)$
195	164 194	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1)$
196	195	mptru	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) \sum_{m = 1}^{⌊\frac{x}{n}⌋} Λ (m) R (\frac{\frac{x}{n}}{m})}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg4r

Proof