Description: Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | deg1z.d | |- D = ( deg1 ` R ) |
|
deg1z.p | |- P = ( Poly1 ` R ) |
||
deg1z.z | |- .0. = ( 0g ` P ) |
||
Assertion | deg1z | |- ( R e. Ring -> ( D ` .0. ) = -oo ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deg1z.d | |- D = ( deg1 ` R ) |
|
2 | deg1z.p | |- P = ( Poly1 ` R ) |
|
3 | deg1z.z | |- .0. = ( 0g ` P ) |
|
4 | 1on | |- 1o e. On |
|
5 | 1 | deg1fval | |- D = ( 1o mDeg R ) |
6 | eqid | |- ( 1o mPoly R ) = ( 1o mPoly R ) |
|
7 | 6 2 3 | ply1mpl0 | |- .0. = ( 0g ` ( 1o mPoly R ) ) |
8 | 5 6 7 | mdeg0 | |- ( ( 1o e. On /\ R e. Ring ) -> ( D ` .0. ) = -oo ) |
9 | 4 8 | mpan | |- ( R e. Ring -> ( D ` .0. ) = -oo ) |