Definition df-zeta 24540

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 24539	. 2 class ζ
2		c1 9816	. . . . . . 7 class 1
3		c2 10947	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1474	. . . . . . . . 9 class 𝑠
6		cmin 10145	. . . . . . . . 9 class −
7	2, 5, 6	co 6549	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 24106	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 6549	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 6549	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1474	. . . . . . 7 class 𝑓
13	5, 12	cfv 5804	. . . . . 6 class (𝑓‘𝑠)
14		cmul 9820	. . . . . 6 class ·
15	10, 13, 14	co 6549	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 11169	. . . . . 6 class ℕ0
17		cc0 9815	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1474	. . . . . . . . 9 class 𝑛
20		cfz 12197	. . . . . . . . 9 class ...
21	17, 19, 20	co 6549	. . . . . . . 8 class (0...𝑛)
22	2	cneg 10146	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1474	. . . . . . . . . . 11 class 𝑘
25		cexp 12722	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 6549	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 12951	. . . . . . . . . . 11 class C
28	19, 24, 27	co 6549	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 6549	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 9818	. . . . . . . . . . 11 class +
31	24, 2, 30	co 6549	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 6549	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 6549	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 14264	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 6549	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 6549	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 10563	. . . . . . 7 class /
38	34, 36, 37	co 6549	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 14264	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1475	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 9813	. . . . 5 class ℂ
42	2	csn 4125	. . . . 5 class {1}
43	41, 42	cdif 3537	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 2896	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 22487	. . . 4 class –cn→
46	43, 41, 45	co 6549	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 6510	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1475	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)