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 26515
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 26514 . 2 class ΞΆ
2 c1 11110 . . . . . . 7 class 1
3 c2 12266 . . . . . . . 8 class 2
4 vs . . . . . . . . . 10 setvar 𝑠
54cv 1540 . . . . . . . . 9 class 𝑠
6 cmin 11443 . . . . . . . . 9 class βˆ’
72, 5, 6co 7408 . . . . . . . 8 class (1 βˆ’ 𝑠)
8 ccxp 26063 . . . . . . . 8 class ↑𝑐
93, 7, 8co 7408 . . . . . . 7 class (2↑𝑐(1 βˆ’ 𝑠))
102, 9, 6co 7408 . . . . . 6 class (1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠)))
11 vf . . . . . . . 8 setvar 𝑓
1211cv 1540 . . . . . . 7 class 𝑓
135, 12cfv 6543 . . . . . 6 class (π‘“β€˜π‘ )
14 cmul 11114 . . . . . 6 class Β·
1510, 13, 14co 7408 . . . . 5 class ((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ ))
16 cn0 12471 . . . . . 6 class β„•0
17 cc0 11109 . . . . . . . . 9 class 0
18 vn . . . . . . . . . 10 setvar 𝑛
1918cv 1540 . . . . . . . . 9 class 𝑛
20 cfz 13483 . . . . . . . . 9 class ...
2117, 19, 20co 7408 . . . . . . . 8 class (0...𝑛)
222cneg 11444 . . . . . . . . . . 11 class -1
23 vk . . . . . . . . . . . 12 setvar π‘˜
2423cv 1540 . . . . . . . . . . 11 class π‘˜
25 cexp 14026 . . . . . . . . . . 11 class ↑
2622, 24, 25co 7408 . . . . . . . . . 10 class (-1β†‘π‘˜)
27 cbc 14261 . . . . . . . . . . 11 class C
2819, 24, 27co 7408 . . . . . . . . . 10 class (𝑛Cπ‘˜)
2926, 28, 14co 7408 . . . . . . . . 9 class ((-1β†‘π‘˜) Β· (𝑛Cπ‘˜))
30 caddc 11112 . . . . . . . . . . 11 class +
3124, 2, 30co 7408 . . . . . . . . . 10 class (π‘˜ + 1)
3231, 5, 8co 7408 . . . . . . . . 9 class ((π‘˜ + 1)↑𝑐𝑠)
3329, 32, 14co 7408 . . . . . . . 8 class (((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠))
3421, 33, 23csu 15631 . . . . . . 7 class Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠))
3519, 2, 30co 7408 . . . . . . . 8 class (𝑛 + 1)
363, 35, 25co 7408 . . . . . . 7 class (2↑(𝑛 + 1))
37 cdiv 11870 . . . . . . 7 class /
3834, 36, 37co 7408 . . . . . 6 class (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
3916, 38, 18csu 15631 . . . . 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 11107 . . . . 5 class β„‚
422csn 4628 . . . . 5 class {1}
4341, 42cdif 3945 . . . 4 class (β„‚ βˆ– {1})
4440, 4, 43wral 3061 . . 3 wff βˆ€π‘  ∈ (β„‚ βˆ– {1})((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ )) = Σ𝑛 ∈ β„•0 (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45 ccncf 24391 . . . 4 class –cnβ†’
4643, 41, 45co 7408 . . 3 class ((β„‚ βˆ– {1})–cnβ†’β„‚)
4744, 11, 46crio 7363 . 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