Definition df-zeta 26949

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 26948	. 2 class ζ
2		c1 11004	. . . . . . 7 class 1
3		c2 12177	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1540	. . . . . . . . 9 class 𝑠
6		cmin 11341	. . . . . . . . 9 class −
7	2, 5, 6	co 7346	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26489	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7346	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7346	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1540	. . . . . . 7 class 𝑓
13	5, 12	cfv 6481	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11008	. . . . . 6 class ·
15	10, 13, 14	co 7346	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12378	. . . . . 6 class ℕ0
17		cc0 11003	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1540	. . . . . . . . 9 class 𝑛
20		cfz 13404	. . . . . . . . 9 class ...
21	17, 19, 20	co 7346	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11342	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1540	. . . . . . . . . . 11 class 𝑘
25		cexp 13965	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7346	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14206	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7346	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7346	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11006	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7346	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7346	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7346	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15590	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7346	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7346	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11771	. . . . . . 7 class /
38	34, 36, 37	co 7346	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15590	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1541	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11001	. . . . 5 class ℂ
42	2	csn 4576	. . . . 5 class {1}
43	41, 42	cdif 3899	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3047	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24794	. . . 4 class –cn→
46	43, 41, 45	co 7346	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7302	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1541	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)