Definition df-zeta 26163

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 26162	. 2 class ζ
2		c1 10872	. . . . . . 7 class 1
3		c2 12028	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1538	. . . . . . . . 9 class 𝑠
6		cmin 11205	. . . . . . . . 9 class −
7	2, 5, 6	co 7275	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 25711	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7275	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7275	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1538	. . . . . . 7 class 𝑓
13	5, 12	cfv 6433	. . . . . 6 class (𝑓‘𝑠)
14		cmul 10876	. . . . . 6 class ·
15	10, 13, 14	co 7275	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12233	. . . . . 6 class ℕ0
17		cc0 10871	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1538	. . . . . . . . 9 class 𝑛
20		cfz 13239	. . . . . . . . 9 class ...
21	17, 19, 20	co 7275	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11206	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1538	. . . . . . . . . . 11 class 𝑘
25		cexp 13782	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7275	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14016	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7275	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7275	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 10874	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7275	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7275	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7275	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15397	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7275	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7275	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11632	. . . . . . 7 class /
38	34, 36, 37	co 7275	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15397	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1539	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 10869	. . . . 5 class ℂ
42	2	csn 4561	. . . . 5 class {1}
43	41, 42	cdif 3884	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3064	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24039	. . . 4 class –cn→
46	43, 41, 45	co 7275	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7231	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1539	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)