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 26518
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 26517 . 2 class ΞΆ
2 c1 11111 . . . . . . 7 class 1
3 c2 12267 . . . . . . . 8 class 2
4 vs . . . . . . . . . 10 setvar 𝑠
54cv 1541 . . . . . . . . 9 class 𝑠
6 cmin 11444 . . . . . . . . 9 class βˆ’
72, 5, 6co 7409 . . . . . . . 8 class (1 βˆ’ 𝑠)
8 ccxp 26064 . . . . . . . 8 class ↑𝑐
93, 7, 8co 7409 . . . . . . 7 class (2↑𝑐(1 βˆ’ 𝑠))
102, 9, 6co 7409 . . . . . 6 class (1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠)))
11 vf . . . . . . . 8 setvar 𝑓
1211cv 1541 . . . . . . 7 class 𝑓
135, 12cfv 6544 . . . . . 6 class (π‘“β€˜π‘ )
14 cmul 11115 . . . . . 6 class Β·
1510, 13, 14co 7409 . . . . 5 class ((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ ))
16 cn0 12472 . . . . . 6 class β„•0
17 cc0 11110 . . . . . . . . 9 class 0
18 vn . . . . . . . . . 10 setvar 𝑛
1918cv 1541 . . . . . . . . 9 class 𝑛
20 cfz 13484 . . . . . . . . 9 class ...
2117, 19, 20co 7409 . . . . . . . 8 class (0...𝑛)
222cneg 11445 . . . . . . . . . . 11 class -1
23 vk . . . . . . . . . . . 12 setvar π‘˜
2423cv 1541 . . . . . . . . . . 11 class π‘˜
25 cexp 14027 . . . . . . . . . . 11 class ↑
2622, 24, 25co 7409 . . . . . . . . . 10 class (-1β†‘π‘˜)
27 cbc 14262 . . . . . . . . . . 11 class C
2819, 24, 27co 7409 . . . . . . . . . 10 class (𝑛Cπ‘˜)
2926, 28, 14co 7409 . . . . . . . . 9 class ((-1β†‘π‘˜) Β· (𝑛Cπ‘˜))
30 caddc 11113 . . . . . . . . . . 11 class +
3124, 2, 30co 7409 . . . . . . . . . 10 class (π‘˜ + 1)
3231, 5, 8co 7409 . . . . . . . . 9 class ((π‘˜ + 1)↑𝑐𝑠)
3329, 32, 14co 7409 . . . . . . . 8 class (((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠))
3421, 33, 23csu 15632 . . . . . . 7 class Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠))
3519, 2, 30co 7409 . . . . . . . 8 class (𝑛 + 1)
363, 35, 25co 7409 . . . . . . 7 class (2↑(𝑛 + 1))
37 cdiv 11871 . . . . . . 7 class /
3834, 36, 37co 7409 . . . . . 6 class (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
3916, 38, 18csu 15632 . . . . 5 class Σ𝑛 ∈ β„•0 (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
4015, 39wceq 1542 . . . 4 wff ((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ )) = Σ𝑛 ∈ β„•0 (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
41 cc 11108 . . . . 5 class β„‚
422csn 4629 . . . . 5 class {1}
4341, 42cdif 3946 . . . 4 class (β„‚ βˆ– {1})
4440, 4, 43wral 3062 . . 3 wff βˆ€π‘  ∈ (β„‚ βˆ– {1})((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ )) = Σ𝑛 ∈ β„•0 (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
45 ccncf 24392 . . . 4 class –cnβ†’
4643, 41, 45co 7409 . . 3 class ((β„‚ βˆ– {1})–cnβ†’β„‚)
4744, 11, 46crio 7364 . 2 class (℩𝑓 ∈ ((β„‚ βˆ– {1})–cnβ†’β„‚)βˆ€π‘  ∈ (β„‚ βˆ– {1})((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ )) = Σ𝑛 ∈ β„•0 (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
481, 47wceq 1542 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