Definition df-zeta

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 - s ) , 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)

	Ref	Expression
Assertion	df-zeta	⊢ ζ = ( ℩ 𝑓 ∈ ( ( ℂ ∖ { 1 } ) –cn→ ℂ ) ∀ 𝑠 ∈ ( ℂ ∖ { 1 } ) ( ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) ) · ( 𝑓 ‘ 𝑠 ) ) = Σ 𝑛 ∈ ℕ0 ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czeta	⊢ ζ
1		vf	⊢ 𝑓
2		cc	⊢ ℂ
3		c1	⊢ 1
4	3	csn	⊢ { 1 }
5	2 4	cdif	⊢ ( ℂ ∖ { 1 } )
6		ccncf	⊢ –cn→
7	5 2 6	co	⊢ ( ( ℂ ∖ { 1 } ) –cn→ ℂ )
8		vs	⊢ 𝑠
9		cmin	⊢ −
10		c2	⊢ 2
11		ccxp	⊢ ↑𝑐
12	8	cv	⊢ 𝑠
13	3 12 9	co	⊢ ( 1 − 𝑠 )
14	10 13 11	co	⊢ ( 2 ↑𝑐 ( 1 − 𝑠 ) )
15	3 14 9	co	⊢ ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) )
16		cmul	⊢ ·
17	1	cv	⊢ 𝑓
18	12 17	cfv	⊢ ( 𝑓 ‘ 𝑠 )
19	15 18 16	co	⊢ ( ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) ) · ( 𝑓 ‘ 𝑠 ) )
20		vn	⊢ 𝑛
21		cn0	⊢ ℕ0
22		vk	⊢ 𝑘
23		cc0	⊢ 0
24		cfz	⊢ ...
25	20	cv	⊢ 𝑛
26	23 25 24	co	⊢ ( 0 ... 𝑛 )
27	3	cneg	⊢ - 1
28		cexp	⊢ ↑
29	22	cv	⊢ 𝑘
30	27 29 28	co	⊢ ( - 1 ↑ 𝑘 )
31		cbc	⊢ C
32	25 29 31	co	⊢ ( 𝑛 C 𝑘 )
33	30 32 16	co	⊢ ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) )
34		caddc	⊢ +
35	29 3 34	co	⊢ ( 𝑘 + 1 )
36	35 12 11	co	⊢ ( ( 𝑘 + 1 ) ↑𝑐 𝑠 )
37	33 36 16	co	⊢ ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) )
38	26 37 22	csu	⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) )
39		cdiv	⊢ /
40	25 3 34	co	⊢ ( 𝑛 + 1 )
41	10 40 28	co	⊢ ( 2 ↑ ( 𝑛 + 1 ) )
42	38 41 39	co	⊢ ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) )
43	21 42 20	csu	⊢ Σ 𝑛 ∈ ℕ0 ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) )
44	19 43	wceq	⊢ ( ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) ) · ( 𝑓 ‘ 𝑠 ) ) = Σ 𝑛 ∈ ℕ0 ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) )
45	44 8 5	wral	⊢ ∀ 𝑠 ∈ ( ℂ ∖ { 1 } ) ( ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) ) · ( 𝑓 ‘ 𝑠 ) ) = Σ 𝑛 ∈ ℕ0 ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) )
46	45 1 7	crio	⊢ ( ℩ 𝑓 ∈ ( ( ℂ ∖ { 1 } ) –cn→ ℂ ) ∀ 𝑠 ∈ ( ℂ ∖ { 1 } ) ( ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) ) · ( 𝑓 ‘ 𝑠 ) ) = Σ 𝑛 ∈ ℕ0 ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) ) )
47	0 46	wceq	⊢ ζ = ( ℩ 𝑓 ∈ ( ( ℂ ∖ { 1 } ) –cn→ ℂ ) ∀ 𝑠 ∈ ( ℂ ∖ { 1 } ) ( ( 1 − ( 2 ↑𝑐 ( 1 − 𝑠 ) ) ) · ( 𝑓 ‘ 𝑠 ) ) = Σ 𝑛 ∈ ℕ0 ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( ( - 1 ↑ 𝑘 ) · ( 𝑛 C 𝑘 ) ) · ( ( 𝑘 + 1 ) ↑𝑐 𝑠 ) ) / ( 2 ↑ ( 𝑛 + 1 ) ) ) )