Metamath Proof Explorer

Theorem dgraacl

Description: Closure of the degree function on algebraic numbers. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion dgraacl 
|- ( A e. AA -> ( degAA ` A ) e. NN )

Proof

Step Hyp Ref Expression
1 dgraalem 
 |-  ( A e. AA -> ( ( degAA ` A ) e. NN /\ E. a e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) )
2 1 simpld 
 |-  ( A e. AA -> ( degAA ` A ) e. NN )