Definition df-zeta 27079

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 − 𝑠), 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.)

Assertion

Ref	Expression
df-zeta	⊢ ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

Distinct variable group:   𝑓,𝑘,𝑛,𝑠

Detailed syntax breakdown of Definition df-zeta

Step	Hyp	Ref	Expression
1		czeta 27078	. 2 class ζ
2		c1 11075	. . . . . . 7 class 1
3		c2 12273	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1560	. . . . . . . . 9 class 𝑠
6		cmin 11415	. . . . . . . . 9 class −
7	2, 5, 6	co 7397	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26621	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7397	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7397	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1560	. . . . . . 7 class 𝑓
13	5, 12	cfv 6522	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11079	. . . . . 6 class ·
15	10, 13, 14	co 7397	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12482	. . . . . 6 class ℕ0
17		cc0 11074	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1560	. . . . . . . . 9 class 𝑛
20		cfz 13513	. . . . . . . . 9 class ...
21	17, 19, 20	co 7397	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11416	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1560	. . . . . . . . . . 11 class 𝑘
25		cexp 14075	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7397	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14316	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7397	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7397	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11077	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7397	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7397	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7397	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15714	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7397	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7397	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11845	. . . . . . 7 class /
38	34, 36, 37	co 7397	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15714	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1561	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11072	. . . . 5 class ℂ
42	2	csn 4583	. . . . 5 class {1}
43	41, 42	cdif 3902	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3077	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24939	. . . 4 class –cn→
46	43, 41, 45	co 7397	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7353	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1561	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)