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	$⊢ ζ = (ι f \in ((ℂ ∖ \{1\}) \underset{cn}{⟶} ℂ) \| \forall s \in (ℂ ∖ \{1\}) (1 - 2^{1 - s}) f (s) = \sum_{n \in ℕ_{0}} (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czeta	$class ζ$
1		vf	$setvar f$
2		cc	$class ℂ$
3		c1	$class 1$
4	3	csn	$class \{1\}$
5	2 4	cdif	$class (ℂ ∖ \{1\})$
6		ccncf	$class \underset{cn}{⟶}$
7	5 2 6	co	$class ((ℂ ∖ \{1\}) \underset{cn}{⟶} ℂ)$
8		vs	$setvar s$
9		cmin	$class -$
10		c2	$class 2$
11		ccxp	$class ↑_{c}$
12	8	cv	$setvar s$
13	3 12 9	co	$class (1 - s)$
14	10 13 11	co	$class 2^{1 - s}$
15	3 14 9	co	$class (1 - 2^{1 - s})$
16		cmul	$class \times$
17	1	cv	$setvar f$
18	12 17	cfv	$class f (s)$
19	15 18 16	co	$class (1 - 2^{1 - s}) f (s)$
20		vn	$setvar n$
21		cn0	$class ℕ_{0}$
22		vk	$setvar k$
23		cc0	$class 0$
24		cfz	$class \dots$
25	20	cv	$setvar n$
26	23 25 24	co	$class (0 \dots n)$
27	3	cneg	$class -1$
28		cexp	$class^$
29	22	cv	$setvar k$
30	27 29 28	co	$class {(- 1)}^{k}$
31		cbc	$class (\binom{.}{.})$
32	25 29 31	co	$class (\binom{n}{k})$
33	30 32 16	co	$class {(- 1)}^{k} (\binom{n}{k})$
34		caddc	$class +$
35	29 3 34	co	$class (k + 1)$
36	35 12 11	co	$class {(k + 1)}^{s}$
37	33 36 16	co	$class {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}$
38	26 37 22	csu	$class \sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}$
39		cdiv	$class \div$
40	25 3 34	co	$class (n + 1)$
41	10 40 28	co	$class 2^{n + 1}$
42	38 41 39	co	$class (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}})$
43	21 42 20	csu	$class \sum_{n \in ℕ_{0}} (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}})$
44	19 43	wceq	$wff (1 - 2^{1 - s}) f (s) = \sum_{n \in ℕ_{0}} (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}})$
45	44 8 5	wral	$wff \forall s \in (ℂ ∖ \{1\}) (1 - 2^{1 - s}) f (s) = \sum_{n \in ℕ_{0}} (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}})$
46	45 1 7	crio	$class (ι f \in ((ℂ ∖ \{1\}) \underset{cn}{⟶} ℂ) \| \forall s \in (ℂ ∖ \{1\}) (1 - 2^{1 - s}) f (s) = \sum_{n \in ℕ_{0}} (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}}))$
47	0 46	wceq	$wff ζ = (ι f \in ((ℂ ∖ \{1\}) \underset{cn}{⟶} ℂ) \| \forall s \in (ℂ ∖ \{1\}) (1 - 2^{1 - s}) f (s) = \sum_{n \in ℕ_{0}} (\frac{\sum_{k = 0}^{n} {(- 1)}^{k} (\binom{n}{k}) {(k + 1)}^{s}}{2^{n + 1}}))$

Metamath Proof Explorer

Definition df-zeta

Detailed syntax breakdown