Theorem pntsf

Description: Functionality of the Selberg function. (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	pntsf	$$⊢S:ℝ⟶ℝ$$

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		fzfid	$$⊢a\in ℝ\to \left(1\dots ⌊a⌋\right)\in \mathrm{Fin}$$
3		elfznn	$$⊢i\in \left(1\dots ⌊a⌋\right)\to i\in \mathbb{N}$$
4	3	adantl	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to i\in \mathbb{N}$$
5		vmacl	$$⊢i\in \mathbb{N}\to \Lambda \left(i\right)\in ℝ$$
6	4 5	syl	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to \Lambda \left(i\right)\in ℝ$$
7	4	nnrpd	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to i\in {ℝ}^{+}$$
8	7	relogcld	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to \log i\in ℝ$$
9		simpl	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to a\in ℝ$$
10	9 4	nndivred	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to \frac{a}{i}\in ℝ$$
11		chpcl	$$⊢\frac{a}{i}\in ℝ\to \psi \left(\frac{a}{i}\right)\in ℝ$$
12	10 11	syl	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to \psi \left(\frac{a}{i}\right)\in ℝ$$
13	8 12	readdcld	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to \log i+\psi \left(\frac{a}{i}\right)\in ℝ$$
14	6 13	remulcld	$$⊢\left(a\in ℝ\wedge i\in \left(1\dots ⌊a⌋\right)\right)\to \Lambda \left(i\right)\left(\log i+\psi \left(\frac{a}{i}\right)\right)\in ℝ$$
15	2 14	fsumrecl	$$⊢a\in ℝ\to \sum _{i=1}^{⌊a⌋}\Lambda \left(i\right)\left(\log i+\psi \left(\frac{a}{i}\right)\right)\in ℝ$$
16	1 15	fmpti	$$⊢S:ℝ⟶ℝ$$