Step | Hyp | Ref
| Expression |
1 | | cmnc 41487 |
. 2
class
Monic |
2 | | vs |
. . 3
setvar π |
3 | | cc 11056 |
. . . 4
class
β |
4 | 3 | cpw 4565 |
. . 3
class π«
β |
5 | | vp |
. . . . . . . 8
setvar π |
6 | 5 | cv 1541 |
. . . . . . 7
class π |
7 | | cdgr 25564 |
. . . . . . 7
class
deg |
8 | 6, 7 | cfv 6501 |
. . . . . 6
class
(degβπ) |
9 | | ccoe 25563 |
. . . . . . 7
class
coeff |
10 | 6, 9 | cfv 6501 |
. . . . . 6
class
(coeffβπ) |
11 | 8, 10 | cfv 6501 |
. . . . 5
class
((coeffβπ)β(degβπ)) |
12 | | c1 11059 |
. . . . 5
class
1 |
13 | 11, 12 | wceq 1542 |
. . . 4
wff
((coeffβπ)β(degβπ)) = 1 |
14 | 2 | cv 1541 |
. . . . 5
class π |
15 | | cply 25561 |
. . . . 5
class
Poly |
16 | 14, 15 | cfv 6501 |
. . . 4
class
(Polyβπ ) |
17 | 13, 5, 16 | crab 3410 |
. . 3
class {π β (Polyβπ ) β£ ((coeffβπ)β(degβπ)) = 1} |
18 | 2, 4, 17 | cmpt 5193 |
. 2
class (π β π« β
β¦ {π β
(Polyβπ ) β£
((coeffβπ)β(degβπ)) = 1}) |
19 | 1, 18 | wceq 1542 |
1
wff Monic =
(π β π« β
β¦ {π β
(Polyβπ ) β£
((coeffβπ)β(degβπ)) = 1}) |