Metamath Proof Explorer


Theorem mpaadgr

Description: Minimal polynomial has degree the degree of the number. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion mpaadgr ( 𝐴 ∈ 𝔸 → ( deg ‘ ( minPolyAA ‘ 𝐴 ) ) = ( degAA𝐴 ) )

Proof

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