Theorem aacn

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

	Ref	Expression
Assertion	aacn	$$⊢A\in 𝔸\to A\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		elaa	$$⊢A\in 𝔸\leftrightarrow \left(A\in ℂ\wedge \exists f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0\right)$$
2	1	simplbi	$$⊢A\in 𝔸\to A\in ℂ$$