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(\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(\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(\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 \log i=\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 \log i+\psi \left(\frac{a}{i}\right)=\log n+\psi \left(\frac{a}{n}\right)$$
7	2 6	oveq12d	$$⊢i=n\to \Lambda \left(i\right)\left(\log i+\psi \left(\frac{a}{i}\right)\right)=\Lambda \left(n\right)\left(\log n+\psi \left(\frac{a}{n}\right)\right)$$
8	7	cbvsumv	$$⊢\sum _{i=1}^{⌊a⌋}\Lambda \left(i\right)\left(\log i+\psi \left(\frac{a}{i}\right)\right)=\sum _{n=1}^{⌊a⌋}\Lambda \left(n\right)\left(\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 \log n+\psi \left(\frac{a}{n}\right)=\log n+\psi \left(\frac{A}{n}\right)$$
13	12	oveq2d	$$⊢a=A\to \Lambda \left(n\right)\left(\log n+\psi \left(\frac{a}{n}\right)\right)=\Lambda \left(n\right)\left(\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(\log n+\psi \left(\frac{a}{n}\right)\right)=\Lambda \left(n\right)\left(\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(\log n+\psi \left(\frac{a}{n}\right)\right)=\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)\left(\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(\log i+\psi \left(\frac{a}{i}\right)\right)=\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)\left(\log n+\psi \left(\frac{A}{n}\right)\right)$$
17		sumex	$$⊢\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)\left(\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(\log n+\psi \left(\frac{A}{n}\right)\right)$$