Definition df-zeta 27158

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 27157	. 2 class ζ
2		c1 11104	. . . . . . 7 class 1
3		c2 12298	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1567	. . . . . . . . 9 class 𝑠
6		cmin 11444	. . . . . . . . 9 class −
7	2, 5, 6	co 7414	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26700	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7414	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7414	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1567	. . . . . . 7 class 𝑓
13	5, 12	cfv 6540	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11108	. . . . . 6 class ·
15	10, 13, 14	co 7414	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12507	. . . . . 6 class ℕ0
17		cc0 11103	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1567	. . . . . . . . 9 class 𝑛
20		cfz 13538	. . . . . . . . 9 class ...
21	17, 19, 20	co 7414	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11445	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1567	. . . . . . . . . . 11 class 𝑘
25		cexp 14100	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7414	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14341	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7414	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7414	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11106	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7414	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7414	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7414	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15740	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7414	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7414	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11874	. . . . . . 7 class /
38	34, 36, 37	co 7414	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15740	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1568	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11101	. . . . 5 class ℂ
42	2	csn 4594	. . . . 5 class {1}
43	41, 42	cdif 3910	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3086	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 25018	. . . 4 class –cn→
46	43, 41, 45	co 7414	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7370	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1568	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)