Theorem mpaamn

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

	Ref	Expression
Assertion	mpaamn	⊢ ( 𝐴 ∈ 𝔸 → ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		mpaalem	⊢ ( 𝐴 ∈ 𝔸 → ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) )
2		simpr3	⊢ ( ( ( minPolyAA ‘ 𝐴 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA ‘ 𝐴 ) ∧ ( ( minPolyAA ‘ 𝐴 ) ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) ) → ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 )
3	1 2	syl	⊢ ( 𝐴 ∈ 𝔸 → ( ( coeff ‘ ( minPolyAA ‘ 𝐴 ) ) ‘ ( degAA ‘ 𝐴 ) ) = 1 )