Theorem mnccoe

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

	Ref	Expression
Assertion	mnccoe	|- ( P e. ( Monic ` S ) -> ( ( coeff ` P ) ` ( deg ` P ) ) = 1 )

Proof

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