Definition df-zeta 27144

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 27143	. 2 class ζ
2		c1 11101	. . . . . . 7 class 1
3		c2 12295	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1566	. . . . . . . . 9 class 𝑠
6		cmin 11441	. . . . . . . . 9 class −
7	2, 5, 6	co 7411	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26686	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7411	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7411	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1566	. . . . . . 7 class 𝑓
13	5, 12	cfv 6537	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11105	. . . . . 6 class ·
15	10, 13, 14	co 7411	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12504	. . . . . 6 class ℕ0
17		cc0 11100	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1566	. . . . . . . . 9 class 𝑛
20		cfz 13535	. . . . . . . . 9 class ...
21	17, 19, 20	co 7411	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11442	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1566	. . . . . . . . . . 11 class 𝑘
25		cexp 14097	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7411	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14338	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7411	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7411	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11103	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7411	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7411	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7411	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15737	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7411	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7411	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11871	. . . . . . 7 class /
38	34, 36, 37	co 7411	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15737	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1567	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11098	. . . . 5 class ℂ
42	2	csn 4594	. . . . 5 class {1}
43	41, 42	cdif 3910	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3085	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 25004	. . . 4 class –cn→
46	43, 41, 45	co 7411	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7367	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1567	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)