Step | Hyp | Ref
| Expression |
1 | | cplylt 41488 |
. 2
class
Poly< |
2 | | vs |
. . 3
setvar π |
3 | | vx |
. . 3
setvar π₯ |
4 | | cc 11056 |
. . . 4
class
β |
5 | 4 | cpw 4565 |
. . 3
class π«
β |
6 | | cn0 12420 |
. . 3
class
β0 |
7 | | vp |
. . . . . . 7
setvar π |
8 | 7 | cv 1541 |
. . . . . 6
class π |
9 | | c0p 25049 |
. . . . . 6
class
0π |
10 | 8, 9 | wceq 1542 |
. . . . 5
wff π =
0π |
11 | | cdgr 25564 |
. . . . . . 7
class
deg |
12 | 8, 11 | cfv 6501 |
. . . . . 6
class
(degβπ) |
13 | 3 | cv 1541 |
. . . . . 6
class π₯ |
14 | | clt 11196 |
. . . . . 6
class
< |
15 | 12, 13, 14 | wbr 5110 |
. . . . 5
wff
(degβπ) <
π₯ |
16 | 10, 15 | wo 846 |
. . . 4
wff (π = 0π β¨
(degβπ) < π₯) |
17 | 2 | cv 1541 |
. . . . 5
class π |
18 | | cply 25561 |
. . . . 5
class
Poly |
19 | 17, 18 | cfv 6501 |
. . . 4
class
(Polyβπ ) |
20 | 16, 7, 19 | crab 3410 |
. . 3
class {π β (Polyβπ ) β£ (π = 0π β¨
(degβπ) < π₯)} |
21 | 2, 3, 5, 6, 20 | cmpo 7364 |
. 2
class (π β π« β, π₯ β β0
β¦ {π β
(Polyβπ ) β£
(π = 0π
β¨ (degβπ) <
π₯)}) |
22 | 1, 21 | wceq 1542 |
1
wff
Poly< = (π
β π« β, π₯
β β0 β¦ {π β (Polyβπ ) β£ (π = 0π β¨
(degβπ) < π₯)}) |