Theorem selbergs

Description: Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016)

	Ref	Expression
Hypothesis	pntsval.1	$$⊢S=\left(a\in ℝ⟼\sum _{i=1}^{⌊a⌋}\Lambda \left(i\right)\left(\log i+\psi \left(\frac{a}{i}\right)\right)\right)$$
Assertion	selbergs	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{S\left(x\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	$$⊢S=\left(a\in ℝ⟼\sum _{i=1}^{⌊a⌋}\Lambda \left(i\right)\left(\log i+\psi \left(\frac{a}{i}\right)\right)\right)$$
2		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
3	1	pntsval	$$⊢x\in ℝ\to S\left(x\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)$$
4	2 3	syl	$$⊢x\in {ℝ}^{+}\to S\left(x\right)=\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)$$
5	4	oveq1d	$$⊢x\in {ℝ}^{+}\to \frac{S\left(x\right)}{x}=\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}$$
6	5	oveq1d	$$⊢x\in {ℝ}^{+}\to \left(\frac{S\left(x\right)}{x}\right)-2\log x=\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x$$
7	6	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{S\left(x\right)}{x}\right)-2\log x\right)=\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right)$$
8		selberg	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{\sum _{n=1}^{⌊x⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{x}{n}\right)\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$
9	7 8	eqeltri	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{S\left(x\right)}{x}\right)-2\log x\right)\in 𝑂\left(1\right)$$