Step | Hyp | Ref
| Expression |
1 | | czeta 26514 |
. 2
class
ΞΆ |
2 | | c1 11110 |
. . . . . . 7
class
1 |
3 | | c2 12266 |
. . . . . . . 8
class
2 |
4 | | vs |
. . . . . . . . . 10
setvar π |
5 | 4 | cv 1540 |
. . . . . . . . 9
class π |
6 | | cmin 11443 |
. . . . . . . . 9
class
β |
7 | 2, 5, 6 | co 7408 |
. . . . . . . 8
class (1
β π ) |
8 | | ccxp 26063 |
. . . . . . . 8
class
βπ |
9 | 3, 7, 8 | co 7408 |
. . . . . . 7
class
(2βπ(1 β π )) |
10 | 2, 9, 6 | co 7408 |
. . . . . 6
class (1
β (2βπ(1 β π ))) |
11 | | vf |
. . . . . . . 8
setvar π |
12 | 11 | cv 1540 |
. . . . . . 7
class π |
13 | 5, 12 | cfv 6543 |
. . . . . 6
class (πβπ ) |
14 | | cmul 11114 |
. . . . . 6
class
Β· |
15 | 10, 13, 14 | co 7408 |
. . . . 5
class ((1
β (2βπ(1 β π ))) Β· (πβπ )) |
16 | | cn0 12471 |
. . . . . 6
class
β0 |
17 | | cc0 11109 |
. . . . . . . . 9
class
0 |
18 | | vn |
. . . . . . . . . 10
setvar π |
19 | 18 | cv 1540 |
. . . . . . . . 9
class π |
20 | | cfz 13483 |
. . . . . . . . 9
class
... |
21 | 17, 19, 20 | co 7408 |
. . . . . . . 8
class
(0...π) |
22 | 2 | cneg 11444 |
. . . . . . . . . . 11
class
-1 |
23 | | vk |
. . . . . . . . . . . 12
setvar π |
24 | 23 | cv 1540 |
. . . . . . . . . . 11
class π |
25 | | cexp 14026 |
. . . . . . . . . . 11
class
β |
26 | 22, 24, 25 | co 7408 |
. . . . . . . . . 10
class
(-1βπ) |
27 | | cbc 14261 |
. . . . . . . . . . 11
class
C |
28 | 19, 24, 27 | co 7408 |
. . . . . . . . . 10
class (πCπ) |
29 | 26, 28, 14 | co 7408 |
. . . . . . . . 9
class
((-1βπ)
Β· (πCπ)) |
30 | | caddc 11112 |
. . . . . . . . . . 11
class
+ |
31 | 24, 2, 30 | co 7408 |
. . . . . . . . . 10
class (π + 1) |
32 | 31, 5, 8 | co 7408 |
. . . . . . . . 9
class ((π +
1)βππ ) |
33 | 29, 32, 14 | co 7408 |
. . . . . . . 8
class
(((-1βπ)
Β· (πCπ)) Β· ((π + 1)βππ )) |
34 | 21, 33, 23 | csu 15631 |
. . . . . . 7
class
Ξ£π β
(0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) |
35 | 19, 2, 30 | co 7408 |
. . . . . . . 8
class (π + 1) |
36 | 3, 35, 25 | co 7408 |
. . . . . . 7
class
(2β(π +
1)) |
37 | | cdiv 11870 |
. . . . . . 7
class
/ |
38 | 34, 36, 37 | co 7408 |
. . . . . 6
class
(Ξ£π β
(0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) / (2β(π + 1))) |
39 | 16, 38, 18 | csu 15631 |
. . . . 5
class
Ξ£π β
β0 (Ξ£π β (0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) / (2β(π + 1))) |
40 | 15, 39 | wceq 1541 |
. . . 4
wff ((1 β
(2βπ(1 β π ))) Β· (πβπ )) = Ξ£π β β0 (Ξ£π β (0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) / (2β(π + 1))) |
41 | | cc 11107 |
. . . . 5
class
β |
42 | 2 | csn 4628 |
. . . . 5
class
{1} |
43 | 41, 42 | cdif 3945 |
. . . 4
class (β
β {1}) |
44 | 40, 4, 43 | wral 3061 |
. . 3
wff
βπ β
(β β {1})((1 β (2βπ(1 β π ))) Β· (πβπ )) = Ξ£π β β0 (Ξ£π β (0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) / (2β(π + 1))) |
45 | | ccncf 24391 |
. . . 4
class
βcnβ |
46 | 43, 41, 45 | co 7408 |
. . 3
class ((β
β {1})βcnββ) |
47 | 44, 11, 46 | crio 7363 |
. 2
class
(β©π
β ((β β {1})βcnββ)βπ β (β β {1})((1 β
(2βπ(1 β π ))) Β· (πβπ )) = Ξ£π β β0 (Ξ£π β (0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) / (2β(π + 1)))) |
48 | 1, 47 | wceq 1541 |
1
wff ΞΆ =
(β©π β
((β β {1})βcnββ)βπ β (β β {1})((1 β
(2βπ(1 β π ))) Β· (πβπ )) = Ξ£π β β0 (Ξ£π β (0...π)(((-1βπ) Β· (πCπ)) Β· ((π + 1)βππ )) / (2β(π + 1)))) |