# Metamath Proof Explorer

## Theorem pntsval

Description: Define the "Selberg function", whose asymptotic behavior is the content of selberg . (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 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)$

### 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 fveq2 ${⊢}{i}={n}\to \Lambda \left({i}\right)=\Lambda \left({n}\right)$
3 fveq2 ${⊢}{i}={n}\to \mathrm{log}{i}=\mathrm{log}{n}$
4 oveq2 ${⊢}{i}={n}\to \frac{{a}}{{i}}=\frac{{a}}{{n}}$
5 4 fveq2d ${⊢}{i}={n}\to \psi \left(\frac{{a}}{{i}}\right)=\psi \left(\frac{{a}}{{n}}\right)$
6 3 5 oveq12d ${⊢}{i}={n}\to \mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)=\mathrm{log}{n}+\psi \left(\frac{{a}}{{n}}\right)$
7 2 6 oveq12d ${⊢}{i}={n}\to \Lambda \left({i}\right)\left(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)=\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{a}}{{n}}\right)\right)$
8 7 cbvsumv ${⊢}\sum _{{i}=1}^{⌊{a}⌋}\Lambda \left({i}\right)\left(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)=\sum _{{n}=1}^{⌊{a}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{a}}{{n}}\right)\right)$
9 fveq2 ${⊢}{a}={A}\to ⌊{a}⌋=⌊{A}⌋$
10 9 oveq2d ${⊢}{a}={A}\to \left(1\dots ⌊{a}⌋\right)=\left(1\dots ⌊{A}⌋\right)$
11 fvoveq1 ${⊢}{a}={A}\to \psi \left(\frac{{a}}{{n}}\right)=\psi \left(\frac{{A}}{{n}}\right)$
12 11 oveq2d ${⊢}{a}={A}\to \mathrm{log}{n}+\psi \left(\frac{{a}}{{n}}\right)=\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)$
13 12 oveq2d ${⊢}{a}={A}\to \Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{a}}{{n}}\right)\right)=\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)$
14 13 adantr ${⊢}\left({a}={A}\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)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)$
15 10 14 sumeq12dv ${⊢}{a}={A}\to \sum _{{n}=1}^{⌊{a}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{a}}{{n}}\right)\right)=\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)$
16 8 15 syl5eq ${⊢}{a}={A}\to \sum _{{i}=1}^{⌊{a}⌋}\Lambda \left({i}\right)\left(\mathrm{log}{i}+\psi \left(\frac{{a}}{{i}}\right)\right)=\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)$
17 sumex ${⊢}\sum _{{n}=1}^{⌊{A}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{A}}{{n}}\right)\right)\in \mathrm{V}$
18 16 1 17 fvmpt ${⊢}{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)$