Metamath Proof Explorer

Theorem pntsval2

Description: The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (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 pntsval2 
|- ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )

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 1 pntsval 
 |-  ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) )
3 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
4 3 adantl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
5 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
6 4 5 syl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) e. RR )
7 6 recnd 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) e. CC )
8 4 nnrpd 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR+ )
9 8 relogcld 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. RR )
10 9 recnd 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. CC )
11 simpl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
12 11 4 nndivred 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( A / n ) e. RR )
13 chpcl 
 |-  ( ( A / n ) e. RR -> ( psi ` ( A / n ) ) e. RR )
14 12 13 syl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( psi ` ( A / n ) ) e. RR )
15 14 recnd 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( psi ` ( A / n ) ) e. CC )
16 7 10 15 adddid 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) ) )
17 16 sumeq2dv 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( A / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) ) )
18 fveq2 
 |-  ( n = m -> ( Lam ` n ) = ( Lam ` m ) )
19 oveq2 
 |-  ( n = m -> ( A / n ) = ( A / m ) )
20 19 fveq2d 
 |-  ( n = m -> ( psi ` ( A / n ) ) = ( psi ` ( A / m ) ) )
21 18 20 oveq12d 
 |-  ( n = m -> ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) = ( ( Lam ` m ) x. ( psi ` ( A / m ) ) ) )
22 21 cbvsumv 
 |-  sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` m ) x. ( psi ` ( A / m ) ) )
23 fzfid 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... ( |_ ` ( A / m ) ) ) e. Fin )
24 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. NN )
25 24 adantl 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. NN )
26 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
27 25 26 syl 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` m ) e. RR )
28 27 recnd 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` m ) e. CC )
29 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( A / m ) ) ) -> k e. NN )
30 29 adantl 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> k e. NN )
31 vmacl 
 |-  ( k e. NN -> ( Lam ` k ) e. RR )
32 30 31 syl 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> ( Lam ` k ) e. RR )
33 32 recnd 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> ( Lam ` k ) e. CC )
34 23 28 33 fsummulc2 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( Lam ` k ) ) = sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( ( Lam ` m ) x. ( Lam ` k ) ) )
35 simpl 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
36 35 25 nndivred 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( A / m ) e. RR )
37 chpval 
 |-  ( ( A / m ) e. RR -> ( psi ` ( A / m ) ) = sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( Lam ` k ) )
38 36 37 syl 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( psi ` ( A / m ) ) = sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( Lam ` k ) )
39 38 oveq2d 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( A / m ) ) ) = ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( Lam ` k ) ) )
40 30 nncnd 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> k e. CC )
41 24 ad2antlr 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> m e. NN )
42 41 nncnd 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> m e. CC )
43 41 nnne0d 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> m =/= 0 )
44 40 42 43 divcan3d 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> ( ( m x. k ) / m ) = k )
45 44 fveq2d 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> ( Lam ` ( ( m x. k ) / m ) ) = ( Lam ` k ) )
46 45 oveq2d 
 |-  ( ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) /\ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ) -> ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) = ( ( Lam ` m ) x. ( Lam ` k ) ) )
47 46 sumeq2dv 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) = sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( ( Lam ` m ) x. ( Lam ` k ) ) )
48 34 39 47 3eqtr4d 
 |-  ( ( A e. RR /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( A / m ) ) ) = sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) )
49 48 sumeq2dv 
 |-  ( A e. RR -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` m ) x. ( psi ` ( A / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` A ) ) sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) )
50 fvoveq1 
 |-  ( n = ( m x. k ) -> ( Lam ` ( n / m ) ) = ( Lam ` ( ( m x. k ) / m ) ) )
51 50 oveq2d 
 |-  ( n = ( m x. k ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) = ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) )
52 id 
 |-  ( A e. RR -> A e. RR )
53 ssrab2 
 |-  { y e. NN | y || n } C_ NN
54 simpr 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> m e. { y e. NN | y || n } )
55 53 54 sselid 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> m e. NN )
56 55 26 syl 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> ( Lam ` m ) e. RR )
57 dvdsdivcl 
 |-  ( ( n e. NN /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. { y e. NN | y || n } )
58 4 57 sylan 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. { y e. NN | y || n } )
59 53 58 sselid 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. NN )
60 vmacl 
 |-  ( ( n / m ) e. NN -> ( Lam ` ( n / m ) ) e. RR )
61 59 60 syl 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> ( Lam ` ( n / m ) ) e. RR )
62 56 61 remulcld 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
63 62 recnd 
 |-  ( ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ m e. { y e. NN | y || n } ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. CC )
64 63 anasss 
 |-  ( ( A e. RR /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. { y e. NN | y || n } ) ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. CC )
65 51 52 64 dvdsflsumcom 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` A ) ) sum_ k e. ( 1 ... ( |_ ` ( A / m ) ) ) ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) )
66 49 65 eqtr4d 
 |-  ( A e. RR -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` m ) x. ( psi ` ( A / m ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
67 22 66 syl5eq 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
68 67 oveq2d 
 |-  ( A e. RR -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
69 fzfid 
 |-  ( A e. RR -> ( 1 ... ( |_ ` A ) ) e. Fin )
70 7 10 mulcld 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
71 7 15 mulcld 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) e. CC )
72 69 70 71 fsumadd 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) ) )
73 fzfid 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 ... n ) e. Fin )
74 dvdsssfz1 
 |-  ( n e. NN -> { y e. NN | y || n } C_ ( 1 ... n ) )
75 4 74 syl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> { y e. NN | y || n } C_ ( 1 ... n ) )
76 73 75 ssfid 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> { y e. NN | y || n } e. Fin )
77 76 62 fsumrecl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
78 77 recnd 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. CC )
79 69 70 78 fsumadd 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
80 68 72 79 3eqtr4d 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( A / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
81 2 17 80 3eqtrd 
 |-  ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )