Metamath Proof Explorer

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 ⊢ S = a ∈ ℝ ⟼ ∑ i = 1 a Λ ⁡ i ⁢ log ⁡ i + ψ ⁡ a i
Assertion selbergsb ⊢ ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ S ⁡ x x − 2 ⁢ log ⁡ x ≤ c

Proof

Step Hyp Ref Expression
1 pntsval.1 ⊢ S = a ∈ ℝ ⟼ ∑ i = 1 a Λ ⁡ i ⁢ log ⁡ i + ψ ⁡ a i
2 selbergb ⊢ ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n x − 2 ⁢ log ⁡ x ≤ c
3 1re ⊢ 1 ∈ ℝ
4 elicopnf ⊢ 1 ∈ ℝ → x ∈ 1 +∞ ↔ x ∈ ℝ ∧ 1 ≤ x
5 3 4 ax-mp ⊢ x ∈ 1 +∞ ↔ x ∈ ℝ ∧ 1 ≤ x
6 5 simplbi ⊢ x ∈ 1 +∞ → x ∈ ℝ
7 1 pntsval ⊢ x ∈ ℝ → S ⁡ x = ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n
8 6 7 syl ⊢ x ∈ 1 +∞ → S ⁡ x = ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n
9 8 oveq1d ⊢ x ∈ 1 +∞ → S ⁡ x x = ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n x
10 9 fvoveq1d ⊢ x ∈ 1 +∞ → S ⁡ x x − 2 ⁢ log ⁡ x = ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n x − 2 ⁢ log ⁡ x
11 10 breq1d ⊢ x ∈ 1 +∞ → S ⁡ x x − 2 ⁢ log ⁡ x ≤ c ↔ ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n x − 2 ⁢ log ⁡ x ≤ c
12 11 ralbiia ⊢ ∀ x ∈ 1 +∞ S ⁡ x x − 2 ⁢ log ⁡ x ≤ c ↔ ∀ x ∈ 1 +∞ ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n x − 2 ⁢ log ⁡ x ≤ c
13 12 rexbii ⊢ ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ S ⁡ x x − 2 ⁢ log ⁡ x ≤ c ↔ ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ ∑ n = 1 x Λ ⁡ n ⁢ log ⁡ n + ψ ⁡ x n x − 2 ⁢ log ⁡ x ≤ c
14 2 13 mpbir ⊢ ∃ c ∈ ℝ + ∀ x ∈ 1 +∞ S ⁡ x x − 2 ⁢ log ⁡ x ≤ c