MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-zeta Structured version   Visualization version   GIF version

Definition df-zeta 25597
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
StepHypRef Expression
1 czeta 25596 . 2 class ζ
2 c1 10527 . . . . . . 7 class 1
3 c2 11680 . . . . . . . 8 class 2
4 vs . . . . . . . . . 10 setvar 𝑠
54cv 1537 . . . . . . . . 9 class 𝑠
6 cmin 10859 . . . . . . . . 9 class
72, 5, 6co 7140 . . . . . . . 8 class (1 − 𝑠)
8 ccxp 25145 . . . . . . . 8 class 𝑐
93, 7, 8co 7140 . . . . . . 7 class (2↑𝑐(1 − 𝑠))
102, 9, 6co 7140 . . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11 vf . . . . . . . 8 setvar 𝑓
1211cv 1537 . . . . . . 7 class 𝑓
135, 12cfv 6334 . . . . . 6 class (𝑓𝑠)
14 cmul 10531 . . . . . 6 class ·
1510, 13, 14co 7140 . . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠))
16 cn0 11885 . . . . . 6 class 0
17 cc0 10526 . . . . . . . . 9 class 0
18 vn . . . . . . . . . 10 setvar 𝑛
1918cv 1537 . . . . . . . . 9 class 𝑛
20 cfz 12885 . . . . . . . . 9 class ...
2117, 19, 20co 7140 . . . . . . . 8 class (0...𝑛)
222cneg 10860 . . . . . . . . . . 11 class -1
23 vk . . . . . . . . . . . 12 setvar 𝑘
2423cv 1537 . . . . . . . . . . 11 class 𝑘
25 cexp 13425 . . . . . . . . . . 11 class
2622, 24, 25co 7140 . . . . . . . . . 10 class (-1↑𝑘)
27 cbc 13658 . . . . . . . . . . 11 class C
2819, 24, 27co 7140 . . . . . . . . . 10 class (𝑛C𝑘)
2926, 28, 14co 7140 . . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30 caddc 10529 . . . . . . . . . . 11 class +
3124, 2, 30co 7140 . . . . . . . . . 10 class (𝑘 + 1)
3231, 5, 8co 7140 . . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
3329, 32, 14co 7140 . . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
3421, 33, 23csu 15033 . . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
3519, 2, 30co 7140 . . . . . . . 8 class (𝑛 + 1)
363, 35, 25co 7140 . . . . . . 7 class (2↑(𝑛 + 1))
37 cdiv 11286 . . . . . . 7 class /
3834, 36, 37co 7140 . . . . . 6 class 𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
3916, 38, 18csu 15033 . . . . 5 class Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
4015, 39wceq 1538 . . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41 cc 10524 . . . . 5 class
422csn 4539 . . . . 5 class {1}
4341, 42cdif 3905 . . . 4 class (ℂ ∖ {1})
4440, 4, 43wral 3130 . . 3 wff 𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45 ccncf 23479 . . . 4 class cn
4643, 41, 45co 7140 . . 3 class ((ℂ ∖ {1})–cn→ℂ)
4744, 11, 46crio 7097 . 2 class (𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
481, 47wceq 1538 1 wff ζ = (𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator