Definition df-zeta 24740

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 24739	. 2 class ζ
2		c1 9937	. . . . . . 7 class 1
3		c2 11070	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1482	. . . . . . . . 9 class 𝑠
6		cmin 10266	. . . . . . . . 9 class −
7	2, 5, 6	co 6650	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 24302	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 6650	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 6650	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1482	. . . . . . 7 class 𝑓
13	5, 12	cfv 5888	. . . . . 6 class (𝑓‘𝑠)
14		cmul 9941	. . . . . 6 class ·
15	10, 13, 14	co 6650	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 11292	. . . . . 6 class ℕ0
17		cc0 9936	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1482	. . . . . . . . 9 class 𝑛
20		cfz 12326	. . . . . . . . 9 class ...
21	17, 19, 20	co 6650	. . . . . . . 8 class (0...𝑛)
22	2	cneg 10267	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1482	. . . . . . . . . . 11 class 𝑘
25		cexp 12860	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 6650	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 13089	. . . . . . . . . . 11 class C
28	19, 24, 27	co 6650	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 6650	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 9939	. . . . . . . . . . 11 class +
31	24, 2, 30	co 6650	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 6650	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 6650	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 14416	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 6650	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 6650	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 10684	. . . . . . 7 class /
38	34, 36, 37	co 6650	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 14416	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1483	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 9934	. . . . 5 class ℂ
42	2	csn 4177	. . . . 5 class {1}
43	41, 42	cdif 3571	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 2912	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 22679	. . . 4 class –cn→
46	43, 41, 45	co 6650	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 6610	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1483	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)