Description: The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mpaaroot | |- ( A e. AA -> ( ( minPolyAA ` A ) ` A ) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpaalem | |- ( A e. AA -> ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) ) |
|
2 | simpr2 | |- ( ( ( minPolyAA ` A ) e. ( Poly ` QQ ) /\ ( ( deg ` ( minPolyAA ` A ) ) = ( degAA ` A ) /\ ( ( minPolyAA ` A ) ` A ) = 0 /\ ( ( coeff ` ( minPolyAA ` A ) ) ` ( degAA ` A ) ) = 1 ) ) -> ( ( minPolyAA ` A ) ` A ) = 0 ) |
|
3 | 1 2 | syl | |- ( A e. AA -> ( ( minPolyAA ` A ) ` A ) = 0 ) |