Definition df-zeta 26996

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 26995	. 2 class ζ
2		c1 11031	. . . . . . 7 class 1
3		c2 12228	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1546	. . . . . . . . 9 class 𝑠
6		cmin 11369	. . . . . . . . 9 class −
7	2, 5, 6	co 7357	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26538	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7357	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7357	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1546	. . . . . . 7 class 𝑓
13	5, 12	cfv 6486	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11035	. . . . . 6 class ·
15	10, 13, 14	co 7357	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12429	. . . . . 6 class ℕ0
17		cc0 11030	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1546	. . . . . . . . 9 class 𝑛
20		cfz 13453	. . . . . . . . 9 class ...
21	17, 19, 20	co 7357	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11370	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1546	. . . . . . . . . . 11 class 𝑘
25		cexp 14015	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7357	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14256	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7357	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7357	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11033	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7357	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7357	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7357	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15640	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7357	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7357	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11799	. . . . . . 7 class /
38	34, 36, 37	co 7357	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15640	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1547	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11028	. . . . 5 class ℂ
42	2	csn 4556	. . . . 5 class {1}
43	41, 42	cdif 3880	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3053	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24862	. . . 4 class –cn→
46	43, 41, 45	co 7357	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7313	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1547	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)