Definition df-zeta 27075

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 27074	. 2 class ζ
2		c1 11185	. . . . . . 7 class 1
3		c2 12348	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1536	. . . . . . . . 9 class 𝑠
6		cmin 11520	. . . . . . . . 9 class −
7	2, 5, 6	co 7448	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26615	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7448	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7448	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1536	. . . . . . 7 class 𝑓
13	5, 12	cfv 6573	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11189	. . . . . 6 class ·
15	10, 13, 14	co 7448	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12553	. . . . . 6 class ℕ0
17		cc0 11184	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1536	. . . . . . . . 9 class 𝑛
20		cfz 13567	. . . . . . . . 9 class ...
21	17, 19, 20	co 7448	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11521	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1536	. . . . . . . . . . 11 class 𝑘
25		cexp 14112	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7448	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14351	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7448	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7448	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11187	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7448	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7448	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7448	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15734	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7448	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7448	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11947	. . . . . . 7 class /
38	34, 36, 37	co 7448	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15734	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1537	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11182	. . . . 5 class ℂ
42	2	csn 4648	. . . . 5 class {1}
43	41, 42	cdif 3973	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3067	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24921	. . . 4 class –cn→
46	43, 41, 45	co 7448	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7403	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1537	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)