# Metamath Proof Explorer

## Theorem 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 ∈ ℝ + ⟼ ψ ⁡ x ⁢ log ⁡ x + ∑ n = 1 x Λ ⁡ n ⁢ ψ ⁡ x n x − 2 ⁢ log ⁡ x ∈ 𝑂⁡1$

### Proof

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