Metamath Proof Explorer

Theorem mncply

Description: A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion mncply 
|- ( P e. ( Monic ` S ) -> P e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 elmnc 
 |-  ( P e. ( Monic ` S ) <-> ( P e. ( Poly ` S ) /\ ( ( coeff ` P ) ` ( deg ` P ) ) = 1 ) )
2 1 simplbi 
 |-  ( P e. ( Monic ` S ) -> P e. ( Poly ` S ) )