Definition df-zeta 25599

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 25598	. 2 class ζ
2		c1 10527	. . . . . . 7 class 1
3		c2 11680	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1537	. . . . . . . . 9 class 𝑠
6		cmin 10859	. . . . . . . . 9 class −
7	2, 5, 6	co 7135	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 25147	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7135	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7135	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1537	. . . . . . 7 class 𝑓
13	5, 12	cfv 6324	. . . . . 6 class (𝑓‘𝑠)
14		cmul 10531	. . . . . 6 class ·
15	10, 13, 14	co 7135	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 11885	. . . . . 6 class ℕ0
17		cc0 10526	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1537	. . . . . . . . 9 class 𝑛
20		cfz 12885	. . . . . . . . 9 class ...
21	17, 19, 20	co 7135	. . . . . . . 8 class (0...𝑛)
22	2	cneg 10860	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1537	. . . . . . . . . . 11 class 𝑘
25		cexp 13425	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7135	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 13658	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7135	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7135	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 10529	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7135	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7135	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7135	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15034	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7135	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7135	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11286	. . . . . . 7 class /
38	34, 36, 37	co 7135	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15034	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1538	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 10524	. . . . 5 class ℂ
42	2	csn 4525	. . . . 5 class {1}
43	41, 42	cdif 3878	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3106	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 23481	. . . 4 class –cn→
46	43, 41, 45	co 7135	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7092	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1538	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)