selberg3r

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

		Ref	Expression
	Hypothesis	pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	selberg3r	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{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	11	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
13	12	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
14	13	2timesd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x = \log x + \log x$
15	14	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - (\log x + \log x)$
16		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
17	3 16	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \in ℝ$
18	17 12	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℝ$
19		2re	$⊢ 2 \in ℝ$
20	19	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ$
21	3 9	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
22	20 21	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
23		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
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		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
27	25 26	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
28	3	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
29	28 25	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
30		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
31	29 30	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
32	27 31	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℝ$
33	25	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
34	33	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
35	32 34	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
36	23 35	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
37	22 36	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
38	18 37	readdcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
39	38 11	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x} \in ℝ$
40	39	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x} \in ℂ$
41	40 13 13	subsub4d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x - \log x = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - (\log x + \log x)$
42	15 41	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x - \log x$
43	42	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x) = ((\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x) - \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x)$
44	40 13	subcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x \in ℂ$
45		2cn	$⊢ 2 \in ℂ$
46	45	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
47	21	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
48	46 13 47	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
49	27 25	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
50	49 34	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log n \in ℝ$
51	23 50	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℝ$
52	51	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℂ$
53	48 52	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℂ$
54	44 53 13	nnncan2d	$⊢ (⊤ \land x \in (1, +∞)) \to ((\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x) - \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x) = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
55	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
56	55	ffvelrni	$⊢ x \in ℝ^{+} \to R (x) \in ℝ$
57	11 56	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℝ$
58	57	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \in ℂ$
59	58 13	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x \in ℂ$
60	37	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
61	59 60	addcld	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
62	3	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
63	62 53	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℂ$
64	11	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
65	61 63 62 64	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{x} = (\frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - (\frac{x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{x})$
66	59 60 63	addsubassd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
67	36	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
68	62 52	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℂ$
69	48 67 68	subdid	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - (\frac{2}{\log x}) x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
70	50	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to (\frac{Λ (n)}{n}) \log n \in ℂ$
71	23 62 70	fsummulc2	$⊢ (⊤ \land x \in (1, +∞)) \to x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = \sum_{n = 1}^{⌊x⌋} x (\frac{Λ (n)}{n}) \log n$
72	71	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} x (\frac{Λ (n)}{n}) \log n$
73	35	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
74	62	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
75	74 70	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x (\frac{Λ (n)}{n}) \log n \in ℂ$
76	23 73 75	fsumsub	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{Λ (n)}{n}) \log n) = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} x (\frac{Λ (n)}{n}) \log n$
77	72 76	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = \sum_{n = 1}^{⌊x⌋} (Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{Λ (n)}{n}) \log n)$
78	27	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
79	31	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℂ$
80	34	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
81	78 79 80	mul32d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n = Λ (n) \log n ψ (\frac{x}{n})$
82	25	nncnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
83	25	nnne0d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
84	78 80 82 83	div23d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n) \log n}{n} = (\frac{Λ (n)}{n}) \log n$
85	84	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x (\frac{Λ (n) \log n}{n}) = x (\frac{Λ (n)}{n}) \log n$
86	78 80	mulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℂ$
87	74 86 82 83	div12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x (\frac{Λ (n) \log n}{n}) = Λ (n) \log n (\frac{x}{n})$
88	85 87	eqtr3d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x (\frac{Λ (n)}{n}) \log n = Λ (n) \log n (\frac{x}{n})$
89	81 88	oveq12d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{Λ (n)}{n}) \log n = Λ (n) \log n ψ (\frac{x}{n}) - Λ (n) \log n (\frac{x}{n})$
90	11	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
91	90 33	rpdivcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
92	1	pntrval	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) = ψ (\frac{x}{n}) - (\frac{x}{n})$
93	91 92	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) = ψ (\frac{x}{n}) - (\frac{x}{n})$
94	93	oveq2d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n R (\frac{x}{n}) = Λ (n) \log n (ψ (\frac{x}{n}) - (\frac{x}{n}))$
95	29	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℂ$
96	86 79 95	subdid	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n (ψ (\frac{x}{n}) - (\frac{x}{n})) = Λ (n) \log n ψ (\frac{x}{n}) - Λ (n) \log n (\frac{x}{n})$
97	94 96	eqtrd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n R (\frac{x}{n}) = Λ (n) \log n ψ (\frac{x}{n}) - Λ (n) \log n (\frac{x}{n})$
98	89 97	eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{Λ (n)}{n}) \log n = Λ (n) \log n R (\frac{x}{n})$
99	55	ffvelrni	$⊢ \frac{x}{n} \in ℝ^{+} \to R (\frac{x}{n}) \in ℝ$
100	91 99	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℝ$
101	100	recnd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to R (\frac{x}{n}) \in ℂ$
102	78 101 80	mul32d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) R (\frac{x}{n}) \log n = Λ (n) \log n R (\frac{x}{n})$
103	98 102	eqtr4d	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{Λ (n)}{n}) \log n = Λ (n) R (\frac{x}{n}) \log n$
104	103	sumeq2dv	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} (Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{Λ (n)}{n}) \log n) = \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
105	77 104	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
106	105	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) (\sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
107	48 62 52	mul12d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
108	107	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - (\frac{2}{\log x}) x \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
109	69 106 108	3eqtr3rd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
110	109	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
111	66 110	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n$
112	111	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{x} = \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}$
113	1	pntrval	$⊢ x \in ℝ^{+} \to R (x) = ψ (x) - x$
114	11 113	syl	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) = ψ (x) - x$
115	114	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x = (ψ (x) - x) \log x$
116	17	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \in ℂ$
117	116 62 13	subdird	$⊢ (⊤ \land x \in (1, +∞)) \to (ψ (x) - x) \log x = ψ (x) \log x - x \log x$
118	115 117	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x = ψ (x) \log x - x \log x$
119	118	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = ψ (x) \log x - x \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
120	18	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℂ$
121	62 13	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to x \log x \in ℂ$
122	120 60 121	addsubd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \log x = ψ (x) \log x - x \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
123	119 122	eqtr4d	$⊢ (⊤ \land x \in (1, +∞)) \to R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n = ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \log x$
124	123	oveq1d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x} = \frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \log x}{x}$
125	38	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
126	125 121 62 64	divsubdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \log x}{x} = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - (\frac{x \log x}{x})$
127	13 62 64	divcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x \log x}{x} = \log x$
128	127	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - (\frac{x \log x}{x}) = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x$
129	126 128	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - x \log x}{x} = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x$
130	124 129	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x} = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x$
131	53 62 64	divcan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{x} = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
132	130 131	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - (\frac{x (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{x}) = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
133	65 112 132	3eqtr3rd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - \log x - (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}$
134	43 54 133	3eqtrrd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x} = (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x)$
135	134	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) = (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x))$
136	20 12	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℝ$
137	39 136	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x \in ℝ$
138	22 51	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n \in ℝ$
139	138 12	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x \in ℝ$
140		selberg3	$⊢ (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x) \in 𝑂 (1)$
141	140	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x) \in 𝑂 (1)$
142	20	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
143	51 21	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x} \in ℝ$
144	143	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x} \in ℂ$
145	12	rehalfcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℝ$
146	145	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{\log x}{2} \in ℂ$
147	142 144 146	subdid	$⊢ (⊤ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - 2 (\frac{\log x}{2})$
148	142 13 52 47	div32d	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n = 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x})$
149	148	eqcomd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n$
150		2ne0	$⊢ 2 \neq 0$
151	150	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \neq 0$
152	13 142 151	divcan2d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 (\frac{\log x}{2}) = \log x$
153	149 152	oveq12d	$⊢ (⊤ \land x \in (1, +∞)) \to 2 (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - 2 (\frac{\log x}{2}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x$
154	147 153	eqtrd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x$
155	154	mpteq2dva	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}))) = (x \in (1, +∞) ⟼ (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x)$
156	143 145	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}) \in ℝ$
157		ioossre	$⊢ (1, +∞) \subseteq ℝ$
158		o1const	$⊢ ((1, +∞) \subseteq ℝ \land 2 \in ℂ) \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
159	157 45 158	mp2an	$⊢ (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
160	159	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2) \in 𝑂 (1)$
161		vmalogdivsum	$⊢ (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
162	161	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2})) \in 𝑂 (1)$
163	20 156 160 162	o1mul2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ 2 ((\frac{\sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n}{\log x}) - (\frac{\log x}{2}))) \in 𝑂 (1)$
164	155 163	eqeltrrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x) \in 𝑂 (1)$
165	137 139 141 164	o1sub2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n}{x}) - 2 \log x - ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} (\frac{Λ (n)}{n}) \log n - \log x)) \in 𝑂 (1)$
166	135 165	eqeltrd	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) \in 𝑂 (1)$
167	166	mptru	$⊢ (x \in (1, +∞) ⟼ \frac{R (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) R (\frac{x}{n}) \log n}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg3r

Proof