Definition df-zeta 27083

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 27082	. 2 class ζ
2		c1 11163	. . . . . . 7 class 1
3		c2 12328	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1538	. . . . . . . . 9 class 𝑠
6		cmin 11499	. . . . . . . . 9 class −
7	2, 5, 6	co 7438	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26623	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7438	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7438	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1538	. . . . . . 7 class 𝑓
13	5, 12	cfv 6569	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11167	. . . . . 6 class ·
15	10, 13, 14	co 7438	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12533	. . . . . 6 class ℕ0
17		cc0 11162	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1538	. . . . . . . . 9 class 𝑛
20		cfz 13553	. . . . . . . . 9 class ...
21	17, 19, 20	co 7438	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11500	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1538	. . . . . . . . . . 11 class 𝑘
25		cexp 14108	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7438	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14347	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7438	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7438	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11165	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7438	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7438	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7438	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15728	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7438	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7438	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11927	. . . . . . 7 class /
38	34, 36, 37	co 7438	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15728	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1539	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11160	. . . . 5 class ℂ
42	2	csn 4634	. . . . 5 class {1}
43	41, 42	cdif 3963	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3061	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24927	. . . 4 class –cn→
46	43, 41, 45	co 7438	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7394	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1539	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)