Definition df-zeta 26992

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 26991	. 2 class ζ
2		c1 11039	. . . . . . 7 class 1
3		c2 12212	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1541	. . . . . . . . 9 class 𝑠
6		cmin 11376	. . . . . . . . 9 class −
7	2, 5, 6	co 7368	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26532	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7368	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7368	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1541	. . . . . . 7 class 𝑓
13	5, 12	cfv 6500	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11043	. . . . . 6 class ·
15	10, 13, 14	co 7368	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12413	. . . . . 6 class ℕ0
17		cc0 11038	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1541	. . . . . . . . 9 class 𝑛
20		cfz 13435	. . . . . . . . 9 class ...
21	17, 19, 20	co 7368	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11377	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1541	. . . . . . . . . . 11 class 𝑘
25		cexp 13996	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7368	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14237	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7368	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7368	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11041	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7368	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7368	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7368	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15621	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7368	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7368	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11806	. . . . . . 7 class /
38	34, 36, 37	co 7368	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15621	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1542	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11036	. . . . 5 class ℂ
42	2	csn 4582	. . . . 5 class {1}
43	41, 42	cdif 3900	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3052	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24837	. . . 4 class –cn→
46	43, 41, 45	co 7368	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7324	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1542	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)