Description: The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | dgrcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | dgrval | |
3 | nn0ssre | |
|
4 | ltso | |
|
5 | soss | |
|
6 | 3 4 5 | mp2 | |
7 | 6 | a1i | |
8 | 0zd | |
|
9 | cnvimass | |
|
10 | 1 | coef | |
11 | 9 10 | fssdm | |
12 | 1 | dgrlem | |
13 | 12 | simprd | |
14 | nn0uz | |
|
15 | 14 | uzsupss | |
16 | 8 11 13 15 | syl3anc | |
17 | 7 16 | supcl | |
18 | 2 17 | eqeltrd | |