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 26525
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 26524 . 2 class ΞΆ
2 c1 11113 . . . . . . 7 class 1
3 c2 12269 . . . . . . . 8 class 2
4 vs . . . . . . . . . 10 setvar 𝑠
54cv 1540 . . . . . . . . 9 class 𝑠
6 cmin 11446 . . . . . . . . 9 class βˆ’
72, 5, 6co 7411 . . . . . . . 8 class (1 βˆ’ 𝑠)
8 ccxp 26071 . . . . . . . 8 class ↑𝑐
93, 7, 8co 7411 . . . . . . 7 class (2↑𝑐(1 βˆ’ 𝑠))
102, 9, 6co 7411 . . . . . 6 class (1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠)))
11 vf . . . . . . . 8 setvar 𝑓
1211cv 1540 . . . . . . 7 class 𝑓
135, 12cfv 6543 . . . . . 6 class (π‘“β€˜π‘ )
14 cmul 11117 . . . . . 6 class Β·
1510, 13, 14co 7411 . . . . 5 class ((1 βˆ’ (2↑𝑐(1 βˆ’ 𝑠))) Β· (π‘“β€˜π‘ ))
16 cn0 12474 . . . . . 6 class β„•0
17 cc0 11112 . . . . . . . . 9 class 0
18 vn . . . . . . . . . 10 setvar 𝑛
1918cv 1540 . . . . . . . . 9 class 𝑛
20 cfz 13486 . . . . . . . . 9 class ...
2117, 19, 20co 7411 . . . . . . . 8 class (0...𝑛)
222cneg 11447 . . . . . . . . . . 11 class -1
23 vk . . . . . . . . . . . 12 setvar π‘˜
2423cv 1540 . . . . . . . . . . 11 class π‘˜
25 cexp 14029 . . . . . . . . . . 11 class ↑
2622, 24, 25co 7411 . . . . . . . . . 10 class (-1β†‘π‘˜)
27 cbc 14264 . . . . . . . . . . 11 class C
2819, 24, 27co 7411 . . . . . . . . . 10 class (𝑛Cπ‘˜)
2926, 28, 14co 7411 . . . . . . . . 9 class ((-1β†‘π‘˜) Β· (𝑛Cπ‘˜))
30 caddc 11115 . . . . . . . . . . 11 class +
3124, 2, 30co 7411 . . . . . . . . . 10 class (π‘˜ + 1)
3231, 5, 8co 7411 . . . . . . . . 9 class ((π‘˜ + 1)↑𝑐𝑠)
3329, 32, 14co 7411 . . . . . . . 8 class (((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠))
3421, 33, 23csu 15634 . . . . . . 7 class Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠))
3519, 2, 30co 7411 . . . . . . . 8 class (𝑛 + 1)
363, 35, 25co 7411 . . . . . . 7 class (2↑(𝑛 + 1))
37 cdiv 11873 . . . . . . 7 class /
3834, 36, 37co 7411 . . . . . 6 class (Ξ£π‘˜ ∈ (0...𝑛)(((-1β†‘π‘˜) Β· (𝑛Cπ‘˜)) Β· ((π‘˜ + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1)))
3916, 38, 18csu 15634 . . . . 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 11110 . . . . 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 24399 . . . 4 class –cnβ†’
4643, 41, 45co 7411 . . 3 class ((β„‚ βˆ– {1})–cnβ†’β„‚)
4744, 11, 46crio 7366 . 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