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		qsscn	$$⊢\mathbb{Q}\subseteq ℂ$$
3		1z	$$⊢1\in \mathbb{Z}$$
4		zq	$$⊢1\in \mathbb{Z}\to 1\in \mathbb{Q}$$
5	3 4	ax-mp	$$⊢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	2 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	2 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	ax-mp	$$⊢-1\in \mathbb{Q}$$
17	16	a1i	$$⊢A\in \mathbb{Q}\to -1\in \mathbb{Q}$$
18	8 10 12 14 17	plysub	$$⊢A\in \mathbb{Q}\to X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\in \mathrm{Poly}\left(\mathbb{Q}\right)$$
19		peano2cn	$$⊢A\in ℂ\to A+1\in ℂ$$
20	1 19	syl	$$⊢A\in \mathbb{Q}\to A+1\in ℂ$$
21		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{ℂ}\right)Fnℂ$$
22		df-idp	$$⊢X^p={\mathrm{I}\upharpoonright }_{ℂ}$$
23	22	fneq1i	$$⊢X^{p}Fnℂ\leftrightarrow \left({\mathrm{I}\upharpoonright }_{ℂ}\right)Fnℂ$$
24	21 23	mpbir	$$⊢X^{p}Fnℂ$$
25	24	a1i	$$⊢A\in \mathbb{Q}\to X^{p}Fnℂ$$
26		fnconstg	$$⊢A\in \mathbb{Q}\to \left(ℂ\times \left\{A\right\}\right)Fnℂ$$
27		cnex	$$⊢ℂ\in \mathrm{V}$$
28	27	a1i	$$⊢A\in \mathbb{Q}\to ℂ\in \mathrm{V}$$
29		inidm	$$⊢ℂ\cap ℂ=ℂ$$
30	22	fveq1i	$$⊢X^p\left(A+1\right)=\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A+1\right)$$
31		fvresi	$$⊢A+1\in ℂ\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A+1\right)=A+1$$
32	30 31	syl5eq	$$⊢A+1\in ℂ\to X^p\left(A+1\right)=A+1$$
33	32	adantl	$$⊢\left(A\in \mathbb{Q}\wedge A+1\in ℂ\right)\to X^p\left(A+1\right)=A+1$$
34		fvconst2g	$$⊢\left(A\in \mathbb{Q}\wedge A+1\in ℂ\right)\to \left(ℂ\times \left\{A\right\}\right)\left(A+1\right)=A$$
35	25 26 28 28 29 33 34	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$$
36	20 35	mpdan	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)=A+1-A$$
37		ax-1cn	$$⊢1\in ℂ$$
38		pncan2	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A+1-A=1$$
39	1 37 38	sylancl	$$⊢A\in \mathbb{Q}\to A+1-A=1$$
40	36 39	eqtrd	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)=1$$
41		ax-1ne0	$$⊢1\ne 0$$
42	41	a1i	$$⊢A\in \mathbb{Q}\to 1\ne 0$$
43	40 42	eqnetrd	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A+1\right)\ne 0$$
44		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_{𝑝}$$
45	20 43 44	syl2anc	$$⊢A\in \mathbb{Q}\to X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\ne 0_{𝑝}$$
46		eldifsn	$$⊢X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\leftrightarrow \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\in \mathrm{Poly}\left(\mathbb{Q}\right)\wedge X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\ne 0_{𝑝}\right)$$
47	18 45 46	sylanbrc	$$⊢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)$$
48	22	fveq1i	$$⊢X^p\left(A\right)=\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)$$
49		fvresi	$$⊢A\in ℂ\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)=A$$
50	48 49	syl5eq	$$⊢A\in ℂ\to X^p\left(A\right)=A$$
51	50	adantl	$$⊢\left(A\in \mathbb{Q}\wedge A\in ℂ\right)\to X^p\left(A\right)=A$$
52		fvconst2g	$$⊢\left(A\in \mathbb{Q}\wedge A\in ℂ\right)\to \left(ℂ\times \left\{A\right\}\right)\left(A\right)=A$$
53	25 26 28 28 29 51 52	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$$
54	1 53	mpdan	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=A-A$$
55	1	subidd	$$⊢A\in \mathbb{Q}\to A-A=0$$
56	54 55	eqtrd	$$⊢A\in \mathbb{Q}\to \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=0$$
57		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)$$
58	57	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)$$
59	58	rspcev	$$⊢\left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)\wedge \left(X^p{-}_f\left(ℂ\times \left\{A\right\}\right)\right)\left(A\right)=0\right)\to \exists f\in \left(\mathrm{Poly}\left(\mathbb{Q}\right)\setminus \left\{0_{𝑝}\right\}\right)f\left(A\right)=0$$
60	47 56 59	syl2anc	$$⊢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$$
61		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)$$
62	1 60 61	sylanbrc	$$⊢A\in \mathbb{Q}\to A\in 𝔸$$