Theorem mnccoe

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

	Ref	Expression
Assertion	mnccoe	⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		elmnc	⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) )
2	1	simprbi	⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 )