Metamath Proof Explorer

Definition df-zeta

Description: Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except 1 , but going from the alternating zeta function to the regular zeta function requires dividing by 1 - 2 ^ ( 1 - s ) , which has zeroes other than 1 . To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014)

Ref Expression
Assertion df-zeta 
|- zeta = ( iota_ f e. ( ( CC \ { 1 } ) -cn-> CC ) A. s e. ( CC \ { 1 } ) ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) ) = sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czeta 
 |-  zeta
1 vf 
 |-  f
2 cc 
 |-  CC
3 c1 
 |-  1
4 3 csn 
 |-  { 1 }
5 2 4 cdif 
 |-  ( CC \ { 1 } )
6 ccncf 
 |-  -cn->
7 5 2 6 co 
 |-  ( ( CC \ { 1 } ) -cn-> CC )
8 vs 
 |-  s
9 cmin 
 |-  -
10 c2 
 |-  2
11 ccxp 
 |-  ^c
12 8 cv 
 |-  s
13 3 12 9 co 
 |-  ( 1 - s )
14 10 13 11 co 
 |-  ( 2 ^c ( 1 - s ) )
15 3 14 9 co 
 |-  ( 1 - ( 2 ^c ( 1 - s ) ) )
16 cmul 
 |-  x.
17 1 cv 
 |-  f
18 12 17 cfv 
 |-  ( f ` s )
19 15 18 16 co 
 |-  ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) )
20 vn 
 |-  n
21 cn0 
 |-  NN0
22 vk 
 |-  k
23 cc0 
 |-  0
24 cfz 
 |-  ...
25 20 cv 
 |-  n
26 23 25 24 co 
 |-  ( 0 ... n )
27 3 cneg 
 |-  -u 1
28 cexp 
 |-  ^
29 22 cv 
 |-  k
30 27 29 28 co 
 |-  ( -u 1 ^ k )
31 cbc 
 |-  _C
32 25 29 31 co 
 |-  ( n _C k )
33 30 32 16 co 
 |-  ( ( -u 1 ^ k ) x. ( n _C k ) )
34 caddc 
 |-  +
35 29 3 34 co 
 |-  ( k + 1 )
36 35 12 11 co 
 |-  ( ( k + 1 ) ^c s )
37 33 36 16 co 
 |-  ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) )
38 26 37 22 csu 
 |-  sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) )
39 cdiv 
 |-  /
40 25 3 34 co 
 |-  ( n + 1 )
41 10 40 28 co 
 |-  ( 2 ^ ( n + 1 ) )
42 38 41 39 co 
 |-  ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) )
43 21 42 20 csu 
 |-  sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) )
44 19 43 wceq 
 |-  ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) ) = sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) )
45 44 8 5 wral 
 |-  A. s e. ( CC \ { 1 } ) ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) ) = sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) )
46 45 1 7 crio 
 |-  ( iota_ f e. ( ( CC \ { 1 } ) -cn-> CC ) A. s e. ( CC \ { 1 } ) ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) ) = sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) ) )
47 0 46 wceq 
 |-  zeta = ( iota_ f e. ( ( CC \ { 1 } ) -cn-> CC ) A. s e. ( CC \ { 1 } ) ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) ) = sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) ) )