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 26445
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 26444 . 2 class ζ
2 c1 11093 . . . . . . 7 class 1
3 c2 12249 . . . . . . . 8 class 2
4 vs . . . . . . . . . 10 setvar 𝑠
54cv 1540 . . . . . . . . 9 class 𝑠
6 cmin 11426 . . . . . . . . 9 class
72, 5, 6co 7393 . . . . . . . 8 class (1 − 𝑠)
8 ccxp 25993 . . . . . . . 8 class 𝑐
93, 7, 8co 7393 . . . . . . 7 class (2↑𝑐(1 − 𝑠))
102, 9, 6co 7393 . . . . . 6 class (1 − (2↑𝑐(1 − 𝑠)))
11 vf . . . . . . . 8 setvar 𝑓
1211cv 1540 . . . . . . 7 class 𝑓
135, 12cfv 6532 . . . . . 6 class (𝑓𝑠)
14 cmul 11097 . . . . . 6 class ·
1510, 13, 14co 7393 . . . . 5 class ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠))
16 cn0 12454 . . . . . 6 class 0
17 cc0 11092 . . . . . . . . 9 class 0
18 vn . . . . . . . . . 10 setvar 𝑛
1918cv 1540 . . . . . . . . 9 class 𝑛
20 cfz 13466 . . . . . . . . 9 class ...
2117, 19, 20co 7393 . . . . . . . 8 class (0...𝑛)
222cneg 11427 . . . . . . . . . . 11 class -1
23 vk . . . . . . . . . . . 12 setvar 𝑘
2423cv 1540 . . . . . . . . . . 11 class 𝑘
25 cexp 14009 . . . . . . . . . . 11 class
2622, 24, 25co 7393 . . . . . . . . . 10 class (-1↑𝑘)
27 cbc 14244 . . . . . . . . . . 11 class C
2819, 24, 27co 7393 . . . . . . . . . 10 class (𝑛C𝑘)
2926, 28, 14co 7393 . . . . . . . . 9 class ((-1↑𝑘) · (𝑛C𝑘))
30 caddc 11095 . . . . . . . . . . 11 class +
3124, 2, 30co 7393 . . . . . . . . . 10 class (𝑘 + 1)
3231, 5, 8co 7393 . . . . . . . . 9 class ((𝑘 + 1)↑𝑐𝑠)
3329, 32, 14co 7393 . . . . . . . 8 class (((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
3421, 33, 23csu 15614 . . . . . . 7 class Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠))
3519, 2, 30co 7393 . . . . . . . 8 class (𝑛 + 1)
363, 35, 25co 7393 . . . . . . 7 class (2↑(𝑛 + 1))
37 cdiv 11853 . . . . . . 7 class /
3834, 36, 37co 7393 . . . . . 6 class 𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
3916, 38, 18csu 15614 . . . . 5 class Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
4015, 39wceq 1541 . . . 4 wff ((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41 cc 11090 . . . . 5 class
422csn 4622 . . . . 5 class {1}
4341, 42cdif 3941 . . . 4 class (ℂ ∖ {1})
4440, 4, 43wral 3060 . . 3 wff 𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45 ccncf 24321 . . . 4 class cn
4643, 41, 45co 7393 . . 3 class ((ℂ ∖ {1})–cn→ℂ)
4744, 11, 46crio 7348 . 2 class (𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓𝑠)) = Σ𝑛 ∈ ℕ0𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
481, 47wceq 1541 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