Step | Hyp | Ref
| Expression |
1 | | citgo 41527 |
. 2
class
IntgOver |
2 | | vs |
. . 3
setvar π |
3 | | cc 11054 |
. . . 4
class
β |
4 | 3 | cpw 4561 |
. . 3
class π«
β |
5 | | vx |
. . . . . . . . 9
setvar π₯ |
6 | 5 | cv 1541 |
. . . . . . . 8
class π₯ |
7 | | vp |
. . . . . . . . 9
setvar π |
8 | 7 | cv 1541 |
. . . . . . . 8
class π |
9 | 6, 8 | cfv 6497 |
. . . . . . 7
class (πβπ₯) |
10 | | cc0 11056 |
. . . . . . 7
class
0 |
11 | 9, 10 | wceq 1542 |
. . . . . 6
wff (πβπ₯) = 0 |
12 | | cdgr 25564 |
. . . . . . . . 9
class
deg |
13 | 8, 12 | cfv 6497 |
. . . . . . . 8
class
(degβπ) |
14 | | ccoe 25563 |
. . . . . . . . 9
class
coeff |
15 | 8, 14 | cfv 6497 |
. . . . . . . 8
class
(coeffβπ) |
16 | 13, 15 | cfv 6497 |
. . . . . . 7
class
((coeffβπ)β(degβπ)) |
17 | | c1 11057 |
. . . . . . 7
class
1 |
18 | 16, 17 | wceq 1542 |
. . . . . 6
wff
((coeffβπ)β(degβπ)) = 1 |
19 | 11, 18 | wa 397 |
. . . . 5
wff ((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1) |
20 | 2 | cv 1541 |
. . . . . 6
class π |
21 | | cply 25561 |
. . . . . 6
class
Poly |
22 | 20, 21 | cfv 6497 |
. . . . 5
class
(Polyβπ ) |
23 | 19, 7, 22 | wrex 3070 |
. . . 4
wff
βπ β
(Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1) |
24 | 23, 5, 3 | crab 3406 |
. . 3
class {π₯ β β β£
βπ β
(Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)} |
25 | 2, 4, 24 | cmpt 5189 |
. 2
class (π β π« β
β¦ {π₯ β β
β£ βπ β
(Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) |
26 | 1, 25 | wceq 1542 |
1
wff IntgOver =
(π β π« β
β¦ {π₯ β β
β£ βπ β
(Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) |