# Metamath Proof Explorer

## Theorem pntsval2

Description: The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (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(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)\right)$
Assertion pntsval2 ${⊢}{A}\in ℝ\to {S}\left({A}\right)=\sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 pntsval.1 ${⊢}{S}=\left({a}\in ℝ⟼\sum _{{i}=1}^{⌊{a}⌋}\Lambda \left({i}\right)\left(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)\right)$
2 1 pntsval ${⊢}{A}\in ℝ\to {S}\left({A}\right)=\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)$
3 elfznn ${⊢}{n}\in \left(1\dots ⌊{A}⌋\right)\to {n}\in ℕ$
4 3 adantl ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to {n}\in ℕ$
5 vmacl ${⊢}{n}\in ℕ\to \Lambda \left({n}\right)\in ℝ$
6 4 5 syl ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({n}\right)\in ℝ$
7 6 recnd ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({n}\right)\in ℂ$
8 4 nnrpd ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to {n}\in {ℝ}^{+}$
9 8 relogcld ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}{n}\in ℝ$
10 9 recnd ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \mathrm{log}{n}\in ℂ$
11 simpl ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to {A}\in ℝ$
12 11 4 nndivred ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{{A}}{{n}}\in ℝ$
13 chpcl ${⊢}\frac{{A}}{{n}}\in ℝ\to \psi \left(\frac{{A}}{{n}}\right)\in ℝ$
14 12 13 syl ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \psi \left(\frac{{A}}{{n}}\right)\in ℝ$
15 14 recnd ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \psi \left(\frac{{A}}{{n}}\right)\in ℂ$
16 7 10 15 adddid ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)=\Lambda \left({n}\right)\mathrm{log}{n}+\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)$
17 16 sumeq2dv ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)\right)$
18 fveq2 ${⊢}{n}={m}\to \Lambda \left({n}\right)=\Lambda \left({m}\right)$
19 oveq2 ${⊢}{n}={m}\to \frac{{A}}{{n}}=\frac{{A}}{{m}}$
20 19 fveq2d ${⊢}{n}={m}\to \psi \left(\frac{{A}}{{n}}\right)=\psi \left(\frac{{A}}{{m}}\right)$
21 18 20 oveq12d ${⊢}{n}={m}\to \Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)=\Lambda \left({m}\right)\psi \left(\frac{{A}}{{m}}\right)$
22 21 cbvsumv ${⊢}\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\Lambda \left({m}\right)\psi \left(\frac{{A}}{{m}}\right)$
23 fzfid ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\in \mathrm{Fin}$
24 elfznn ${⊢}{m}\in \left(1\dots ⌊{A}⌋\right)\to {m}\in ℕ$
25 24 adantl ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to {m}\in ℕ$
26 vmacl ${⊢}{m}\in ℕ\to \Lambda \left({m}\right)\in ℝ$
27 25 26 syl ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({m}\right)\in ℝ$
28 27 recnd ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({m}\right)\in ℂ$
29 elfznn ${⊢}{k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\to {k}\in ℕ$
30 29 adantl ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to {k}\in ℕ$
31 vmacl ${⊢}{k}\in ℕ\to \Lambda \left({k}\right)\in ℝ$
32 30 31 syl ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to \Lambda \left({k}\right)\in ℝ$
33 32 recnd ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to \Lambda \left({k}\right)\in ℂ$
34 23 28 33 fsummulc2 ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({m}\right)\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({k}\right)=\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({m}\right)\Lambda \left({k}\right)$
35 simpl ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to {A}\in ℝ$
36 35 25 nndivred ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \frac{{A}}{{m}}\in ℝ$
37 chpval ${⊢}\frac{{A}}{{m}}\in ℝ\to \psi \left(\frac{{A}}{{m}}\right)=\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({k}\right)$
38 36 37 syl ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \psi \left(\frac{{A}}{{m}}\right)=\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({k}\right)$
39 38 oveq2d ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({m}\right)\psi \left(\frac{{A}}{{m}}\right)=\Lambda \left({m}\right)\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({k}\right)$
40 30 nncnd ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to {k}\in ℂ$
41 24 ad2antlr ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to {m}\in ℕ$
42 41 nncnd ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to {m}\in ℂ$
43 41 nnne0d ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to {m}\ne 0$
44 40 42 43 divcan3d ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to \frac{{m}{k}}{{m}}={k}$
45 44 fveq2d ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to \Lambda \left(\frac{{m}{k}}{{m}}\right)=\Lambda \left({k}\right)$
46 45 oveq2d ${⊢}\left(\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {k}\in \left(1\dots ⌊\frac{{A}}{{m}}⌋\right)\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{m}{k}}{{m}}\right)=\Lambda \left({m}\right)\Lambda \left({k}\right)$
47 46 sumeq2dv ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({m}\right)\Lambda \left(\frac{{m}{k}}{{m}}\right)=\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({m}\right)\Lambda \left({k}\right)$
48 34 39 47 3eqtr4d ${⊢}\left({A}\in ℝ\wedge {m}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({m}\right)\psi \left(\frac{{A}}{{m}}\right)=\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({m}\right)\Lambda \left(\frac{{m}{k}}{{m}}\right)$
49 48 sumeq2dv ${⊢}{A}\in ℝ\to \sum _{{m}=1}^{⌊{A}⌋}\Lambda \left({m}\right)\psi \left(\frac{{A}}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({m}\right)\Lambda \left(\frac{{m}{k}}{{m}}\right)$
50 fvoveq1 ${⊢}{n}={m}{k}\to \Lambda \left(\frac{{n}}{{m}}\right)=\Lambda \left(\frac{{m}{k}}{{m}}\right)$
51 50 oveq2d ${⊢}{n}={m}{k}\to \Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)=\Lambda \left({m}\right)\Lambda \left(\frac{{m}{k}}{{m}}\right)$
52 id ${⊢}{A}\in ℝ\to {A}\in ℝ$
53 ssrab2 ${⊢}\left\{{y}\in ℕ|{y}\parallel {n}\right\}\subseteq ℕ$
54 simpr ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}$
55 53 54 sseldi ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to {m}\in ℕ$
56 55 26 syl ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left({m}\right)\in ℝ$
57 dvdsdivcl ${⊢}\left({n}\in ℕ\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \frac{{n}}{{m}}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}$
58 4 57 sylan ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \frac{{n}}{{m}}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}$
59 53 58 sseldi ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \frac{{n}}{{m}}\in ℕ$
60 vmacl ${⊢}\frac{{n}}{{m}}\in ℕ\to \Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
61 59 60 syl ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
62 56 61 remulcld ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
63 62 recnd ${⊢}\left(\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℂ$
64 63 anasss ${⊢}\left({A}\in ℝ\wedge \left({n}\in \left(1\dots ⌊{A}⌋\right)\wedge {m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}\right)\right)\to \Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℂ$
65 51 52 64 dvdsflsumcom ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)=\sum _{{m}=1}^{⌊{A}⌋}\sum _{{k}=1}^{⌊\frac{{A}}{{m}}⌋}\Lambda \left({m}\right)\Lambda \left(\frac{{m}{k}}{{m}}\right)$
66 49 65 eqtr4d ${⊢}{A}\in ℝ\to \sum _{{m}=1}^{⌊{A}⌋}\Lambda \left({m}\right)\psi \left(\frac{{A}}{{m}}\right)=\sum _{{n}=1}^{⌊{A}⌋}\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
67 22 66 syl5eq ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)=\sum _{{n}=1}^{⌊{A}⌋}\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
68 67 oveq2d ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)=\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{n}=1}^{⌊{A}⌋}\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
69 fzfid ${⊢}{A}\in ℝ\to \left(1\dots ⌊{A}⌋\right)\in \mathrm{Fin}$
70 7 10 mulcld ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({n}\right)\mathrm{log}{n}\in ℂ$
71 7 15 mulcld ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)\in ℂ$
72 69 70 71 fsumadd ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)$
73 fzfid ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \left(1\dots {n}\right)\in \mathrm{Fin}$
74 dvdsssfz1 ${⊢}{n}\in ℕ\to \left\{{y}\in ℕ|{y}\parallel {n}\right\}\subseteq \left(1\dots {n}\right)$
75 4 74 syl ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {n}\right\}\subseteq \left(1\dots {n}\right)$
76 73 75 ssfid ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \left\{{y}\in ℕ|{y}\parallel {n}\right\}\in \mathrm{Fin}$
77 76 62 fsumrecl ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℝ$
78 77 recnd ${⊢}\left({A}\in ℝ\wedge {n}\in \left(1\dots ⌊{A}⌋\right)\right)\to \sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\in ℂ$
79 69 70 78 fsumadd ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right)=\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{n}=1}^{⌊{A}⌋}\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)$
80 68 72 79 3eqtr4d ${⊢}{A}\in ℝ\to \sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\Lambda \left({n}\right)\psi \left(\frac{{A}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right)$
81 2 17 80 3eqtrd ${⊢}{A}\in ℝ\to {S}\left({A}\right)=\sum _{{n}=1}^{⌊{A}⌋}\left(\Lambda \left({n}\right)\mathrm{log}{n}+\sum _{{m}\in \left\{{y}\in ℕ|{y}\parallel {n}\right\}}\Lambda \left({m}\right)\Lambda \left(\frac{{n}}{{m}}\right)\right)$