Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-zeta Structured version   Unicode version

Definition df-zeta 24803
 Description: Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except , but going from the alternating zeta function to the regular zeta function requires dividing by , which has zeroes other than . 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.)
Assertion
Ref Expression
df-zeta
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-zeta
StepHypRef Expression
1 czeta 24802 . 2
2 c1 8996 . . . . . . 7
3 c2 10054 . . . . . . . 8
4 vs . . . . . . . . . 10
54cv 1652 . . . . . . . . 9
6 cmin 9296 . . . . . . . . 9
72, 5, 6co 6084 . . . . . . . 8
8 ccxp 20458 . . . . . . . 8
93, 7, 8co 6084 . . . . . . 7
102, 9, 6co 6084 . . . . . 6
11 vf . . . . . . . 8
1211cv 1652 . . . . . . 7
135, 12cfv 5457 . . . . . 6
14 cmul 9000 . . . . . 6
1510, 13, 14co 6084 . . . . 5
16 cn0 10226 . . . . . 6
17 cc0 8995 . . . . . . . . 9
18 vn . . . . . . . . . 10
1918cv 1652 . . . . . . . . 9
20 cfz 11048 . . . . . . . . 9
2117, 19, 20co 6084 . . . . . . . 8
222cneg 9297 . . . . . . . . . . 11
23 vk . . . . . . . . . . . 12
2423cv 1652 . . . . . . . . . . 11
25 cexp 11387 . . . . . . . . . . 11
2622, 24, 25co 6084 . . . . . . . . . 10
27 cbc 11598 . . . . . . . . . . 11
2819, 24, 27co 6084 . . . . . . . . . 10
2926, 28, 14co 6084 . . . . . . . . 9
30 caddc 8998 . . . . . . . . . . 11
3124, 2, 30co 6084 . . . . . . . . . 10
3231, 5, 8co 6084 . . . . . . . . 9
3329, 32, 14co 6084 . . . . . . . 8
3421, 33, 23csu 12484 . . . . . . 7
3519, 2, 30co 6084 . . . . . . . 8
363, 35, 25co 6084 . . . . . . 7
37 cdiv 9682 . . . . . . 7
3834, 36, 37co 6084 . . . . . 6
3916, 38, 18csu 12484 . . . . 5
4015, 39wceq 1653 . . . 4
41 cc 8993 . . . . 5
422csn 3816 . . . . 5
4341, 42cdif 3319 . . . 4
4440, 4, 43wral 2707 . . 3
45 ccncf 18911 . . . 4
4643, 41, 45co 6084 . . 3
4744, 11, 46crio 6545 . 2
481, 47wceq 1653 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator