Definition df-zeta 27341

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 27340	. 2 class ζ
2		c1 11201	. . . . . . 7 class 1
3		c2 12397	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1568	. . . . . . . . 9 class 𝑠
6		cmin 11541	. . . . . . . . 9 class −
7	2, 5, 6	co 7420	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26883	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7420	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7420	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1568	. . . . . . 7 class 𝑓
13	5, 12	cfv 6538	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11205	. . . . . 6 class ·
15	10, 13, 14	co 7420	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12606	. . . . . 6 class ℕ0
17		cc0 11200	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1568	. . . . . . . . 9 class 𝑛
20		cfz 13639	. . . . . . . . 9 class ...
21	17, 19, 20	co 7420	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11542	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1568	. . . . . . . . . . 11 class 𝑘
25		cexp 14204	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7420	. . . . . . . . . 10 class ( -1↑𝑘)
27		cbc 14446	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7420	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7420	. . . . . . . . 9 class (( -1↑𝑘) · (𝑛C𝑘))
30		caddc 11203	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7420	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7420	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7420	. . . . . . . 8 class ((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15853	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7420	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7420	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11973	. . . . . . 7 class /
38	34, 36, 37	co 7420	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15853	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1569	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11198	. . . . 5 class ℂ
42	2	csn 4583	. . . . 5 class {1}
43	41, 42	cdif 4045	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3076	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 25197	. . . 4 class –cn→
46	43, 41, 45	co 7420	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7376	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1569	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)((( -1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is used by: (None)