pntsf

Description: Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016)

		Ref	Expression
	Hypothesis	pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
	Assertion	pntsf	$⊢ S : ℝ ⟶ ℝ$

Step	Hyp	Ref	Expression
1		pntsval.1	$⊢ S = (a \in ℝ ⟼ \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})))$
2		fzfid	$⊢ a \in ℝ \to (1 \dots ⌊a⌋) \in Fin$
3		elfznn	$⊢ i \in (1 \dots ⌊a⌋) \to i \in ℕ$
4	3	adantl	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to i \in ℕ$
5		vmacl	$⊢ i \in ℕ \to Λ (i) \in ℝ$
6	4 5	syl	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to Λ (i) \in ℝ$
7	4	nnrpd	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to i \in ℝ^{+}$
8	7	relogcld	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to \log i \in ℝ$
9		simpl	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to a \in ℝ$
10	9 4	nndivred	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to \frac{a}{i} \in ℝ$
11		chpcl	$⊢ \frac{a}{i} \in ℝ \to ψ (\frac{a}{i}) \in ℝ$
12	10 11	syl	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to ψ (\frac{a}{i}) \in ℝ$
13	8 12	readdcld	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to \log i + ψ (\frac{a}{i}) \in ℝ$
14	6 13	remulcld	$⊢ (a \in ℝ \land i \in (1 \dots ⌊a⌋)) \to Λ (i) (\log i + ψ (\frac{a}{i})) \in ℝ$
15	2 14	fsumrecl	$⊢ a \in ℝ \to \sum_{i = 1}^{⌊a⌋} Λ (i) (\log i + ψ (\frac{a}{i})) \in ℝ$
16	1 15	fmpti	$⊢ S : ℝ ⟶ ℝ$

Metamath Proof Explorer