Definition df-zeta 25593

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 25592	. 2 class ζ
2		c1 10540	. . . . . . 7 class 1
3		c2 11695	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1536	. . . . . . . . 9 class 𝑠
6		cmin 10872	. . . . . . . . 9 class −
7	2, 5, 6	co 7158	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 25141	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7158	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7158	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1536	. . . . . . 7 class 𝑓
13	5, 12	cfv 6357	. . . . . 6 class (𝑓‘𝑠)
14		cmul 10544	. . . . . 6 class ·
15	10, 13, 14	co 7158	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 11900	. . . . . 6 class ℕ0
17		cc0 10539	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1536	. . . . . . . . 9 class 𝑛
20		cfz 12895	. . . . . . . . 9 class ...
21	17, 19, 20	co 7158	. . . . . . . 8 class (0...𝑛)
22	2	cneg 10873	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1536	. . . . . . . . . . 11 class 𝑘
25		cexp 13432	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7158	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 13665	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7158	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7158	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 10542	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7158	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7158	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7158	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15044	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7158	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7158	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11299	. . . . . . 7 class /
38	34, 36, 37	co 7158	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15044	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1537	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 10537	. . . . 5 class ℂ
42	2	csn 4569	. . . . 5 class {1}
43	41, 42	cdif 3935	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3140	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 23486	. . . 4 class –cn→
46	43, 41, 45	co 7158	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7115	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1537	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)