Definition df-zeta 27248

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 27247	. 2 class ζ
2		c1 11128	. . . . . . 7 class 1
3		c2 12322	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1569	. . . . . . . . 9 class 𝑠
6		cmin 11468	. . . . . . . . 9 class −
7	2, 5, 6	co 7416	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26790	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7416	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7416	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1569	. . . . . . 7 class 𝑓
13	5, 12	cfv 6537	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11132	. . . . . 6 class ·
15	10, 13, 14	co 7416	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12531	. . . . . 6 class ℕ0
17		cc0 11127	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1569	. . . . . . . . 9 class 𝑛
20		cfz 13563	. . . . . . . . 9 class ...
21	17, 19, 20	co 7416	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11469	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1569	. . . . . . . . . . 11 class 𝑘
25		cexp 14127	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7416	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14368	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7416	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7416	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11130	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7416	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7416	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7416	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15775	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7416	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7416	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11898	. . . . . . 7 class /
38	34, 36, 37	co 7416	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15775	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1570	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11125	. . . . 5 class ℂ
42	2	csn 4587	. . . . 5 class {1}
43	41, 42	cdif 3899	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3078	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 25105	. . . 4 class –cn→
46	43, 41, 45	co 7416	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7372	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1570	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is used by: (None)