Theorem elaa

Description: Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		df-aa	$$⊢𝔸=\bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]$$
2	1	eleq2i	$$⊢A\in 𝔸\leftrightarrow A\in \bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]$$
3		eliun	$$⊢A\in \bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]\leftrightarrow \exists f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)A\in f^{-1}\left[\left\{0\right\}\right]$$
4		eldifi	$$⊢f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\to f\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
5		plyf	$$⊢f\in \mathrm{Poly}\left(\mathbb{Z}\right)\to f:ℂ⟶ℂ$$
6		ffn	$$⊢f:ℂ⟶ℂ\to fFnℂ$$
7		fniniseg	$$⊢fFnℂ\to \left(A\in f^{-1}\left[\left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge f\left(A\right)=0\right)\right)$$
8	4 5 6 7	4syl	$$⊢f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\to \left(A\in f^{-1}\left[\left\{0\right\}\right]\leftrightarrow \left(A\in ℂ\wedge f\left(A\right)=0\right)\right)$$
9	8	rexbiia	$$⊢\exists f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)A\in f^{-1}\left[\left\{0\right\}\right]\leftrightarrow \exists f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(A\in ℂ\wedge f\left(A\right)=0\right)$$
10		r19.42v	$$⊢\exists f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)\left(A\in ℂ\wedge f\left(A\right)=0\right)\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)$$
11	9 10	bitri	$$⊢\exists f\in \left(\mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}\right)A\in f^{-1}\left[\left\{0\right\}\right]\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)$$
12	3 11	bitri	$$⊢A\in \bigcup _{f\in \mathrm{Poly}\left(\mathbb{Z}\right)\setminus \left\{0_{𝑝}\right\}}{f}^{-1}\left[\left\{0\right\}\right]\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)$$
13	2 12	bitri	$$⊢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)$$