Metamath Proof Explorer

Theorem pntsf

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

Ref Expression
Hypothesis pntsval.1 
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
Assertion pntsf 
|- S : RR --> RR

Proof

Step Hyp Ref Expression
1 pntsval.1 
 |-  S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2 fzfid 
 |-  ( a e. RR -> ( 1 ... ( |_ ` a ) ) e. Fin )
3 elfznn 
 |-  ( i e. ( 1 ... ( |_ ` a ) ) -> i e. NN )
4 3 adantl 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> i e. NN )
5 vmacl 
 |-  ( i e. NN -> ( Lam ` i ) e. RR )
6 4 5 syl 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> ( Lam ` i ) e. RR )
7 4 nnrpd 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> i e. RR+ )
8 7 relogcld 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> ( log ` i ) e. RR )
9 simpl 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> a e. RR )
10 9 4 nndivred 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> ( a / i ) e. RR )
11 chpcl 
 |-  ( ( a / i ) e. RR -> ( psi ` ( a / i ) ) e. RR )
12 10 11 syl 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> ( psi ` ( a / i ) ) e. RR )
13 8 12 readdcld 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> ( ( log ` i ) + ( psi ` ( a / i ) ) ) e. RR )
14 6 13 remulcld 
 |-  ( ( a e. RR /\ i e. ( 1 ... ( |_ ` a ) ) ) -> ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) e. RR )
15 2 14 fsumrecl 
 |-  ( a e. RR -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) e. RR )
16 1 15 fmpti 
 |-  S : RR --> RR