Theorem mnccoe

Description: A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014)

	Ref	Expression
Assertion	mnccoe	$$⊢P\in \mathrm{Monic}\left(S\right)\to \mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)=1$$

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	simprbi	$$⊢P\in \mathrm{Monic}\left(S\right)\to \mathrm{coeff}\left(P\right)\left(\mathrm{deg}\left(P\right)\right)=1$$