Theorem selbergsb

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	selbergsb	⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2		selbergb	⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐
3		1re	⊢ 1 ∈ ℝ
4		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
5	3 4	ax-mp	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
6	5	simplbi	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ )
7	1	pntsval	⊢ ( 𝑥 ∈ ℝ → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
8	6 7	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 𝑆 ‘ 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
9	8	oveq1d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) )
10	9	fvoveq1d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( abs ‘ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
11	10	breq1d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 ↔ ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 ) )
12	11	ralbiia	⊢ ( ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 ↔ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 )
13	12	rexbii	⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 ↔ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 )
14	2 13	mpbir	⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑥 ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐