Metamath Proof Explorer

Theorem aacn

Description: An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion aacn 
|- ( A e. AA -> A e. CC )

Proof

Step Hyp Ref Expression
1 elaa 
 |-  ( A e. AA <-> ( A e. CC /\ E. f e. ( ( Poly ` ZZ ) \ { 0p } ) ( f ` A ) = 0 ) )
2 1 simplbi 
 |-  ( A e. AA -> A e. CC )