Theorem pntsf

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

	Ref	Expression
Hypothesis	pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
Assertion	pntsf	⊢ 𝑆 : ℝ ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2		fzfid	⊢ ( 𝑎 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝑎 ) ) ∈ Fin )
3		elfznn	⊢ ( 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) → 𝑖 ∈ ℕ )
4	3	adantl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → 𝑖 ∈ ℕ )
5		vmacl	⊢ ( 𝑖 ∈ ℕ → ( Λ ‘ 𝑖 ) ∈ ℝ )
6	4 5	syl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
7	4	nnrpd	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → 𝑖 ∈ ℝ+ )
8	7	relogcld	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → ( log ‘ 𝑖 ) ∈ ℝ )
9		simpl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → 𝑎 ∈ ℝ )
10	9 4	nndivred	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → ( 𝑎 / 𝑖 ) ∈ ℝ )
11		chpcl	⊢ ( ( 𝑎 / 𝑖 ) ∈ ℝ → ( ψ ‘ ( 𝑎 / 𝑖 ) ) ∈ ℝ )
12	10 11	syl	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → ( ψ ‘ ( 𝑎 / 𝑖 ) ) ∈ ℝ )
13	8 12	readdcld	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ∈ ℝ )
14	6 13	remulcld	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ) → ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) ∈ ℝ )
15	2 14	fsumrecl	⊢ ( 𝑎 ∈ ℝ → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) ∈ ℝ )
16	1 15	fmpti	⊢ 𝑆 : ℝ ⟶ ℝ