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	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
Assertion	selbergs	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
3	1	pntsval	⊢ ( 𝑥 ∈ ℝ → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
4	2 3	syl	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
5	4	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) )
6	5	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
7	6	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
8		selberg	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
9	7 8	eqeltri	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)