Theorem mncply

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

	Ref	Expression
Assertion	mncply	$$⊢P\in \mathrm{Monic}\left(S\right)\to P\in \mathrm{Poly}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmnc	$$⊢P\in \mathrm{Monic}\left(S\right)\leftrightarrow \left(P\in \mathrm{Poly}\left(S\right)\wedge \mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)=1\right)$$
2	1	simplbi	$$⊢P\in \mathrm{Monic}\left(S\right)\to P\in \mathrm{Poly}\left(S\right)$$