Definition df-zeta 26931

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 26930	. 2 class ζ
2		c1 11076	. . . . . . 7 class 1
3		c2 12248	. . . . . . . 8 class 2
4		vs	. . . . . . . . . 10 setvar 𝑠
5	4	cv 1539	. . . . . . . . 9 class 𝑠
6		cmin 11412	. . . . . . . . 9 class −
7	2, 5, 6	co 7390	. . . . . . . 8 class (1 − 𝑠)
8		ccxp 26471	. . . . . . . 8 class ↑𝑐
9	3, 7, 8	co 7390	. . . . . . 7 class (2↑𝑐(1 − 𝑠))
10	2, 9, 6	co 7390	. . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1539	. . . . . . 7 class 𝑓
13	5, 12	cfv 6514	. . . . . 6 class (𝑓‘𝑠)
14		cmul 11080	. . . . . 6 class ·
15	10, 13, 14	co 7390	. . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠))
16		cn0 12449	. . . . . 6 class ℕ0
17		cc0 11075	. . . . . . . . 9 class 0
18		vn	. . . . . . . . . 10 setvar 𝑛
19	18	cv 1539	. . . . . . . . 9 class 𝑛
20		cfz 13475	. . . . . . . . 9 class ...
21	17, 19, 20	co 7390	. . . . . . . 8 class (0...𝑛)
22	2	cneg 11413	. . . . . . . . . . 11 class -1
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1539	. . . . . . . . . . 11 class 𝑘
25		cexp 14033	. . . . . . . . . . 11 class ↑
26	22, 24, 25	co 7390	. . . . . . . . . 10 class (-1↑𝑘)
27		cbc 14274	. . . . . . . . . . 11 class C
28	19, 24, 27	co 7390	. . . . . . . . . 10 class (𝑛C𝑘)
29	26, 28, 14	co 7390	. . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30		caddc 11078	. . . . . . . . . . 11 class +
31	24, 2, 30	co 7390	. . . . . . . . . 10 class (𝑘 + 1)
32	31, 5, 8	co 7390	. . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
33	29, 32, 14	co 7390	. . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
34	21, 33, 23	csu 15659	. . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
35	19, 2, 30	co 7390	. . . . . . . 8 class (𝑛 + 1)
36	3, 35, 25	co 7390	. . . . . . 7 class (2↑(𝑛 + 1))
37		cdiv 11842	. . . . . . 7 class /
38	34, 36, 37	co 7390	. . . . . 6 class (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
39	16, 38, 18	csu 15659	. . . . 5 class Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
40	15, 39	wceq 1540	. . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41		cc 11073	. . . . 5 class ℂ
42	2	csn 4592	. . . . 5 class {1}
43	41, 42	cdif 3914	. . . 4 class (ℂ ∖ {1})
44	40, 4, 43	wral 3045	. . 3 wff ∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45		ccncf 24776	. . . 4 class –cn→
46	43, 41, 45	co 7390	. . 3 class ((ℂ ∖ {1})–cn→ℂ)
47	44, 11, 46	crio 7346	. 2 class (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
48	1, 47	wceq 1540	1 wff ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))

This definition is referenced by: (None)