Metamath Proof Explorer

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 = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
Assertion pntsval 
|- ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )

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 fveq2 
 |-  ( i = n -> ( Lam ` i ) = ( Lam ` n ) )
3 fveq2 
 |-  ( i = n -> ( log ` i ) = ( log ` n ) )
4 oveq2 
 |-  ( i = n -> ( a / i ) = ( a / n ) )
5 4 fveq2d 
 |-  ( i = n -> ( psi ` ( a / i ) ) = ( psi ` ( a / n ) ) )
6 3 5 oveq12d 
 |-  ( i = n -> ( ( log ` i ) + ( psi ` ( a / i ) ) ) = ( ( log ` n ) + ( psi ` ( a / n ) ) ) )
7 2 6 oveq12d 
 |-  ( i = n -> ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) = ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( a / n ) ) ) ) )
8 7 cbvsumv 
 |-  sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( a / n ) ) ) )
9 fveq2 
 |-  ( a = A -> ( |_ ` a ) = ( |_ ` A ) )
10 9 oveq2d 
 |-  ( a = A -> ( 1 ... ( |_ ` a ) ) = ( 1 ... ( |_ ` A ) ) )
11 fvoveq1 
 |-  ( a = A -> ( psi ` ( a / n ) ) = ( psi ` ( A / n ) ) )
12 11 oveq2d 
 |-  ( a = A -> ( ( log ` n ) + ( psi ` ( a / n ) ) ) = ( ( log ` n ) + ( psi ` ( A / n ) ) ) )
13 12 oveq2d 
 |-  ( a = A -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( a / n ) ) ) ) = ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )
14 13 adantr 
 |-  ( ( a = A /\ n e. ( 1 ... ( |_ ` a ) ) ) -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( a / n ) ) ) ) = ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )
15 10 14 sumeq12dv 
 |-  ( a = A -> sum_ n e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( a / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )
16 8 15 syl5eq 
 |-  ( a = A -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )
17 sumex 
 |-  sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) e. _V
18 16 1 17 fvmpt 
 |-  ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )