Description: Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deg1xrf.d | ||
deg1xrf.p | |||
deg1xrf.b | |||
Assertion | deg1cl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deg1xrf.d | ||
2 | deg1xrf.p | ||
3 | deg1xrf.b | ||
4 | 1 | deg1fval | |
5 | eqid | ||
6 | 2 3 | ply1bas | |
7 | 4 5 6 | mdegcl |