Theorem qaa

Description: Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014)

	Ref	Expression
Assertion	qaa	$$⊢A\in \mathbb{Q}\to A\in 𝔸$$

Proof

Step	Hyp	Ref	Expression
1		qcn	$$⊢A\in \mathbb{Q}\to A\in ℂ$$
2		fveq1	$$⊢f=X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\to f\left(A\right)=\left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)$$
3	2	eqeq1d	$$⊢f=X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\to \left(f\left(A\right)=0\leftrightarrow \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=0\right)$$
4		qsscn	$$⊢\mathbb{Q}\subseteq ℂ$$
5		1q	$$⊢1\in \mathbb{Q}$$
6		plyid	$$⊢\left(\mathbb{Q}\subseteq ℂ\wedge 1\in \mathbb{Q}\right)\to X^p\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
7	4 5 6	mp2an	$$⊢X^p\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
8	7	a1i	$$⊢A\in \mathbb{Q}\to X^p\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
9		plyconst	$$⊢\left(\mathbb{Q}\subseteq ℂ\wedge A\in \mathbb{Q}\right)\to ℂ\times \left\{A\right\}\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
10	4 9	mpan	$$⊢A\in \mathbb{Q}\to ℂ\times \left\{A\right\}\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
11		qaddcl	$$⊢\left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\to x+y\in \mathbb{Q}$$
12	11	adantl	$$⊢\left(A\in \mathbb{Q}\wedge \left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\right)\to x+y\in \mathbb{Q}$$
13		qmulcl	$$⊢\left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\to xy\in \mathbb{Q}$$
14	13	adantl	$$⊢\left(A\in \mathbb{Q}\wedge \left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\right)\to xy\in \mathbb{Q}$$
15		qnegcl	$$⊢1\in \mathbb{Q}\to -1\in \mathbb{Q}$$
16	5 15	mp1i	$$⊢A\in \mathbb{Q}\to -1\in \mathbb{Q}$$
17	8 10 12 14 16	plysub	$$⊢A\in \mathbb{Q}\to X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
18		peano2cn	$$⊢A\in ℂ\to A+1\in ℂ$$
19	1 18	syl	$$⊢A\in \mathbb{Q}\to A+1\in ℂ$$
20		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{ℂ}\right)Fnℂ$$
21		df-idp	$$⊢X^p={\mathrm{I}\upharpoonright }_{ℂ}$$
22	21	fneq1i	$$⊢X^{p}Fnℂ\leftrightarrow \left({\mathrm{I}\upharpoonright }_{ℂ}\right)Fnℂ$$
23	20 22	mpbir	$$⊢X^{p}Fnℂ$$
24	23	a1i	$$⊢A\in \mathbb{Q}\to X^{p}Fnℂ$$
25		fnconstg	$$⊢A\in \mathbb{Q}\to \left(ℂ\times \left\{A\right\}\right)Fnℂ$$
26		cnex	$$⊢ℂ\in \mathrm{V}$$
27	26	a1i	$$⊢A\in \mathbb{Q}\to ℂ\in \mathrm{V}$$
28		inidm	$$⊢ℂ\cap ℂ=ℂ$$
29		idpfv	$$⊢A+1\in ℂ\to X^p\left(A+1\right)=A+1$$
30	29	adantl	$$⊢\left(A\in \mathbb{Q}\wedge A+1\in ℂ\right)\to X^p\left(A+1\right)=A+1$$
31		fvconst2g	$$⊢\left(A\in \mathbb{Q}\wedge A+1\in ℂ\right)\to \left(ℂ\times \left\{A\right\}\right)\left(A+1\right)=A$$
32	24 25 27 27 28 30 31	ofval	$$⊢\left(A\in \mathbb{Q}\wedge A+1\in ℂ\right)\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)=A+1-A$$
33	19 32	mpdan	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)=A+1-A$$
34		ax-1cn	$$⊢1\in ℂ$$
35		pncan2	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A+1-A=1$$
36	1 34 35	sylancl	$$⊢A\in \mathbb{Q}\to A+1-A=1$$
37	33 36	eqtrd	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)=1$$
38		ax-1ne0	$$⊢1\ne 0$$
39	38	a1i	$$⊢A\in \mathbb{Q}\to 1\ne 0$$
40	37 39	eqnetrd	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)\ne 0$$
41		ne0p	$$⊢\left(A+1\in ℂ\wedge \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)\ne 0\right)\to X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\ne 0_{𝑝}$$
42	19 40 41	syl2anc	$$⊢A\in \mathbb{Q}\to X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\ne 0_{𝑝}$$
43	17 42	eldifsnd	$$⊢A\in \mathbb{Q}\to X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)$$
44		idpfv	$$⊢A\in ℂ\to X^p\left(A\right)=A$$
45	44	adantl	$$⊢\left(A\in \mathbb{Q}\wedge A\in ℂ\right)\to X^p\left(A\right)=A$$
46		fvconst2g	$$⊢\left(A\in \mathbb{Q}\wedge A\in ℂ\right)\to \left(ℂ\times \left\{A\right\}\right)\left(A\right)=A$$
47	24 25 27 27 28 45 46	ofval	$$⊢\left(A\in \mathbb{Q}\wedge A\in ℂ\right)\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=A-A$$
48	1 47	mpdan	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=A-A$$
49	1	subidd	$$⊢A\in \mathbb{Q}\to A-A=0$$
50	48 49	eqtrd	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=0$$
51	3 43 50	rspcedvdw	$$⊢A\in \mathbb{Q}\to \exists f\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0$$
52		elqaa	$$⊢A\in 𝔸\leftrightarrow \left(A\in ℂ\wedge \exists f\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0\right)$$
53	1 51 52	sylanbrc	$$⊢A\in \mathbb{Q}\to A\in 𝔸$$