Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-zeta | Structured version Visualization version Unicode version |
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.) |
Ref | Expression |
---|---|
df-zeta |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | czeta 24739 | . 2 | |
2 | c1 9937 | . . . . . . 7 | |
3 | c2 11070 | . . . . . . . 8 | |
4 | vs | . . . . . . . . . 10 | |
5 | 4 | cv 1482 | . . . . . . . . 9 |
6 | cmin 10266 | . . . . . . . . 9 | |
7 | 2, 5, 6 | co 6650 | . . . . . . . 8 |
8 | ccxp 24302 | . . . . . . . 8 | |
9 | 3, 7, 8 | co 6650 | . . . . . . 7 |
10 | 2, 9, 6 | co 6650 | . . . . . 6 |
11 | vf | . . . . . . . 8 | |
12 | 11 | cv 1482 | . . . . . . 7 |
13 | 5, 12 | cfv 5888 | . . . . . 6 |
14 | cmul 9941 | . . . . . 6 | |
15 | 10, 13, 14 | co 6650 | . . . . 5 |
16 | cn0 11292 | . . . . . 6 | |
17 | cc0 9936 | . . . . . . . . 9 | |
18 | vn | . . . . . . . . . 10 | |
19 | 18 | cv 1482 | . . . . . . . . 9 |
20 | cfz 12326 | . . . . . . . . 9 | |
21 | 17, 19, 20 | co 6650 | . . . . . . . 8 |
22 | 2 | cneg 10267 | . . . . . . . . . . 11 |
23 | vk | . . . . . . . . . . . 12 | |
24 | 23 | cv 1482 | . . . . . . . . . . 11 |
25 | cexp 12860 | . . . . . . . . . . 11 | |
26 | 22, 24, 25 | co 6650 | . . . . . . . . . 10 |
27 | cbc 13089 | . . . . . . . . . . 11 | |
28 | 19, 24, 27 | co 6650 | . . . . . . . . . 10 |
29 | 26, 28, 14 | co 6650 | . . . . . . . . 9 |
30 | caddc 9939 | . . . . . . . . . . 11 | |
31 | 24, 2, 30 | co 6650 | . . . . . . . . . 10 |
32 | 31, 5, 8 | co 6650 | . . . . . . . . 9 |
33 | 29, 32, 14 | co 6650 | . . . . . . . 8 |
34 | 21, 33, 23 | csu 14416 | . . . . . . 7 |
35 | 19, 2, 30 | co 6650 | . . . . . . . 8 |
36 | 3, 35, 25 | co 6650 | . . . . . . 7 |
37 | cdiv 10684 | . . . . . . 7 | |
38 | 34, 36, 37 | co 6650 | . . . . . 6 |
39 | 16, 38, 18 | csu 14416 | . . . . 5 |
40 | 15, 39 | wceq 1483 | . . . 4 |
41 | cc 9934 | . . . . 5 | |
42 | 2 | csn 4177 | . . . . 5 |
43 | 41, 42 | cdif 3571 | . . . 4 |
44 | 40, 4, 43 | wral 2912 | . . 3 |
45 | ccncf 22679 | . . . 4 | |
46 | 43, 41, 45 | co 6650 | . . 3 |
47 | 44, 11, 46 | crio 6610 | . 2 |
48 | 1, 47 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: (None) |
Copyright terms: Public domain | W3C validator |