selberg2

Description: Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
3	1 2	ssexi	$⊢ ℝ^{+} \in V$
4	3	a1i	$⊢ ⊤ \to ℝ^{+} \in V$
5		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x \in V$
6		ovexd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x} \in V$
7		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) = (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x)$
8		eqidd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x})$
9	4 5 6 7 8	offval2	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) -_{f} (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}))$
10	9	mptru	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) -_{f} (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}))$
11		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
12		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
13	12	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
14		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
15	13 14	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
16	15	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
17	13	nnrpd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
18		relogcl	$⊢ n \in ℝ^{+} \to \log n \in ℝ$
19	17 18	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
20	19	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
21		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
22		nndivre	$⊢ (x \in ℝ \land n \in ℕ) \to \frac{x}{n} \in ℝ$
23	21 12 22	syl2an	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
24		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
25	23 24	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
26	25	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℂ$
27	20 26	addcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n + ψ (\frac{x}{n}) \in ℂ$
28	16 27	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) \in ℂ$
29	11 28	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \in ℂ$
30		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
31		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
32	29 30 31	divcld	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} \in ℂ$
33		2cn	$⊢ 2 \in ℂ$
34		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
35	34	recnd	$⊢ x \in ℝ^{+} \to \log x \in ℂ$
36		mulcl	$⊢ (2 \in ℂ \land \log x \in ℂ) \to 2 \log x \in ℂ$
37	33 35 36	sylancr	$⊢ x \in ℝ^{+} \to 2 \log x \in ℂ$
38	16 20	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℂ$
39	11 38	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) \log n \in ℂ$
40		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
41	21 40	syl	$⊢ x \in ℝ^{+} \to ψ (x) \in ℝ$
42	41	recnd	$⊢ x \in ℝ^{+} \to ψ (x) \in ℂ$
43	42 35	mulcld	$⊢ x \in ℝ^{+} \to ψ (x) \log x \in ℂ$
44	39 43	subcld	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x \in ℂ$
45	44 30 31	divcld	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x} \in ℂ$
46	32 37 45	sub32d	$⊢ x \in ℝ^{+} \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) - 2 \log x$
47		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
48		divsubdir	$⊢ (\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) \in ℂ \land \sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x)}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x})$
49	29 44 47 48	syl3anc	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x)}{x} = (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x})$
50	16 20 26	adddid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) = Λ (n) \log n + Λ (n) ψ (\frac{x}{n})$
51	50	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (Λ (n) \log n + Λ (n) ψ (\frac{x}{n}))$
52	16 26	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℂ$
53	11 38 52	fsumadd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (Λ (n) \log n + Λ (n) ψ (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} Λ (n) \log n + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
54	51 53	eqtrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} Λ (n) \log n + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
55	54	oveq1d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x) = \sum_{n = 1}^{⌊x⌋} Λ (n) \log n + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x)$
56	11 52	fsumcl	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) \in ℂ$
57	39 56 43	pnncand	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) \log n + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x) = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ψ (x) \log x$
58	56 43	addcomd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + ψ (x) \log x = ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
59	55 57 58	3eqtrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x) = ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})$
60	59	oveq1d	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) - (\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x)}{x} = \frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}$
61	49 60	eqtr3d	$⊢ x \in ℝ^{+} \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = \frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}$
62	61	oveq1d	$⊢ x \in ℝ^{+} \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) - 2 \log x = (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x$
63	46 62	eqtrd	$⊢ x \in ℝ^{+} \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x$
64	63	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x - (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x})) = (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x)$
65	10 64	eqtri	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) -_{f} (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) = (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x)$
66		selberg	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1)$
67		selberg2lem	$⊢ (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)$
68		o1sub	$⊢ ((x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1) \land (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)) \to (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) -_{f} (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)$
69	66 67 68	mp2an	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) -_{f} (x \in ℝ^{+} ⟼ \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) \log n - ψ (x) \log x}{x}) \in 𝑂 (1)$
70	65 69	eqeltrri	$⊢ (x \in ℝ^{+} ⟼ (\frac{ψ (x) \log x + \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n})}{x}) - 2 \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg2

Proof