selberg3

Description: Introduce a log weighting on the summands of sum_ m x. n <_ x , Lam ( m ) Lam ( n ) , the core of selberg2 (written here as sum_ n <_ x , Lam ( n ) psi ( x / n ) ). Equation 10.6.7 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
2	1	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ$
3		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
4	2 3	syl	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \in ℝ$
5		1rp	$⊢ 1 \in ℝ^{+}$
6	5	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ^{+}$
7		1red	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \in ℝ$
8		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
9	8	adantl	$⊢ (⊤ \land x \in (1, +∞)) \to (1 < x \land x < +∞)$
10	9	simpld	$⊢ (⊤ \land x \in (1, +∞)) \to 1 < x$
11	7 2 10	ltled	$⊢ (⊤ \land x \in (1, +∞)) \to 1 \leq x$
12	2 6 11	rpgecld	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℝ^{+}$
13	12	relogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ$
14	4 13	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℝ$
15	14	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x \in ℂ$
16		fzfid	$⊢ (⊤ \land x \in (1, +∞)) \to (1 \dots ⌊x⌋) \in Fin$
17		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
18	17	adantl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
19		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
20	18 19	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
21	2	adantr	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
22	21 18	nndivred	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
23		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
24	22 23	syl	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
25	20 24	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℝ$
26	16 25	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℝ$
27	26	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℂ$
28		2re	$⊢ 2 \in ℝ$
29	28	a1i	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℝ$
30	2 10	rplogcld	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℝ^{+}$
31	29 30	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℝ$
32	18	nnrpd	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
33	32	relogcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
34	25 33	remulcld	$⊢ ((⊤ \land x \in (1, +∞)) \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
35	16 34	fsumrecl	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
36	31 35	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℝ$
37	36 26	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℝ$
38	37	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℂ$
39	15 27 38	addassd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})) = ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}))$
40		2cnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \in ℂ$
41	13	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \in ℂ$
42	30	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to \log x \neq 0$
43	40 41 42	divcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{2}{\log x} \in ℂ$
44	35	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
45	43 44	mulcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n \in ℂ$
46	27 45	pncan3d	$⊢ (⊤ \land x \in (1, +∞)) \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) = (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
47	46	oveq2d	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})) = ψ (x) \log x + (\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n$
48	39 47	eqtr2d	$⊢ (⊤ \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 + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}))$
49	48	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} = \frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}))}{x}$
50	14 26	readdcld	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℝ$
51	50	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℂ$
52	2	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to x \in ℂ$
53	12	rpne0d	$⊢ (⊤ \land x \in (1, +∞)) \to x \neq 0$
54	51 38 52 53	divdird	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ((\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}))}{x} = (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x})$
55	49 54	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} = (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x})$
56	55	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{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x$
57	50 12	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x} \in ℝ$
58	57	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x} \in ℂ$
59	37 12	rerpdivcld	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x} \in ℝ$
60	59	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x} \in ℂ$
61	29 13	remulcld	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℝ$
62	61	recnd	$⊢ (⊤ \land x \in (1, +∞)) \to 2 \log x \in ℂ$
63	58 60 62	addsubd	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x = (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x})$
64	56 63	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}) - 2 \log x = (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x})$
65	64	mpteq2dva	$⊢ ⊤ \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) = (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}))$
66	57 61	resubcld	$⊢ (⊤ \land x \in (1, +∞)) \to (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x \in ℝ$
67	12	ex	$⊢ ⊤ \to (x \in (1, +∞) \to x \in ℝ^{+})$
68	67	ssrdv	$⊢ ⊤ \to (1, +∞) \subseteq ℝ^{+}$
69		selberg2	$⊢ (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x) \in 𝑂 (1)$
70	69	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x) \in 𝑂 (1)$
71	68 70	o1res2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x) \in 𝑂 (1)$
72		selberg3lem2	$⊢ (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) \in 𝑂 (1)$
73	72	a1i	$⊢ ⊤ \to (x \in (1, +∞) ⟼ \frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) \in 𝑂 (1)$
74	66 59 71 73	o1add2	$⊢ ⊤ \to (x \in (1, +∞) ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x + (\frac{(\frac{2}{\log x}) \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \log n - \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x})) \in 𝑂 (1)$
75	65 74	eqeltrd	$⊢ ⊤ \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)$
76	75	mptru	$⊢ (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)$

Metamath Proof Explorer

Theorem selberg3

Proof