Theorem aannen

Description: The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Assertion	aannen	$$⊢𝔸\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(a\in {\mathbb{N}}_0⟼\left\{b\in ℂ|\exists c\in \left\{d\in \mathrm{Poly}\left(\mathbb{Z}\right)|\left(d\ne 0_{𝑝}\wedge \mathrm{deg}\left(d\right)\le a\wedge \forall e\in {\mathbb{N}}_0\left|\mathrm{coeff}\left(d\right)\left(e\right)\right|\le a\right)\right\}c\left(b\right)=0\right\}\right)=\left(a\in {\mathbb{N}}_0⟼\left\{b\in ℂ|\exists c\in \left\{d\in \mathrm{Poly}\left(\mathbb{Z}\right)|\left(d\ne 0_{𝑝}\wedge \mathrm{deg}\left(d\right)\le a\wedge \forall e\in {\mathbb{N}}_0\left|\mathrm{coeff}\left(d\right)\left(e\right)\right|\le a\right)\right\}c\left(b\right)=0\right\}\right)$$
2	1	aannenlem3	$$⊢𝔸\approx \mathbb{N}$$