Definition df-zeta 27368

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 27367	. 2 class ζ
2		c1 11225	. . . . . . 7 class 1
3		c2 12421	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1569	. . . . . . . . 9 class 𝑠
6		cmin 11565	. . . . . . . . 9 class −
7	2, 5, 6	co 7440	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26910	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7440	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7440	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1569	. . . . . . 7 class 𝑓
13	5, 12	cfv 6555	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11229	. . . . . 6 class ·
15	10, 13, 14	co 7440	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12630	. . . . . 6 class ℕ0
17		cc0 11224	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1569	. . . . . . . . 9 class 𝑛
20		cfz 13663	. . . . . . . . 9 class ...
21	17, 19, 20	co 7440	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11566	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1569	. . . . . . . . . . 11 class 𝑘
25		cexp 14228	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7440	. . . . . . . . . 10 class ( -1↑𝑘)
27		cbc 14470	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7440	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7440	. . . . . . . . 9 class (( -1↑𝑘) · (𝑛C𝑘))
30		caddc 11227	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7440	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7440	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7440	. . . . . . . 8 class ((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15879	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7440	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7440	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11997	. . . . . . 7 class /
38	34, 36, 37	co 7440	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15879	. . . . 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 11222	. . . . 5 class ℂ
42	2	csn 4588	. . . . 5 class {1}
43	41, 42	cdif 4048	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3080	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 25224	. . . 4 class –cn→
46	43, 41, 45	co 7440	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7396	. 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)