Metamath Proof Explorer


Theorem mpaamn

Description: Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion mpaamn A𝔸coeffminPoly𝔸Adeg𝔸A=1

Proof

Step Hyp Ref Expression
1 mpaalem A𝔸minPoly𝔸APolydegminPoly𝔸A=deg𝔸AminPoly𝔸AA=0coeffminPoly𝔸Adeg𝔸A=1
2 simpr3 minPoly𝔸APolydegminPoly𝔸A=deg𝔸AminPoly𝔸AA=0coeffminPoly𝔸Adeg𝔸A=1coeffminPoly𝔸Adeg𝔸A=1
3 1 2 syl A𝔸coeffminPoly𝔸Adeg𝔸A=1