Theorem qaa

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

	Ref	Expression
Assertion	qaa	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ 𝔸 )

Proof

Step	Hyp	Ref	Expression
1		qcn	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
2		qsscn	⊢ ℚ ⊆ ℂ
3		1z	⊢ 1 ∈ ℤ
4		zq	⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
5	3 4	ax-mp	⊢ 1 ∈ ℚ
6		plyid	⊢ ( ( ℚ ⊆ ℂ ∧ 1 ∈ ℚ ) → Xp ∈ ( Poly ‘ ℚ ) )
7	2 5 6	mp2an	⊢ Xp ∈ ( Poly ‘ ℚ )
8	7	a1i	⊢ ( 𝐴 ∈ ℚ → Xp ∈ ( Poly ‘ ℚ ) )
9		plyconst	⊢ ( ( ℚ ⊆ ℂ ∧ 𝐴 ∈ ℚ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℚ ) )
10	2 9	mpan	⊢ ( 𝐴 ∈ ℚ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℚ ) )
11		qaddcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 + 𝑦 ) ∈ ℚ )
12	11	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) ∈ ℚ )
13		qmulcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
15		qnegcl	⊢ ( 1 ∈ ℚ → - 1 ∈ ℚ )
16	5 15	ax-mp	⊢ - 1 ∈ ℚ
17	16	a1i	⊢ ( 𝐴 ∈ ℚ → - 1 ∈ ℚ )
18	8 10 12 14 17	plysub	⊢ ( 𝐴 ∈ ℚ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℚ ) )
19		peano2cn	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 1 ) ∈ ℂ )
20	1 19	syl	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 + 1 ) ∈ ℂ )
21		fnresi	⊢ ( I ↾ ℂ ) Fn ℂ
22		df-idp	⊢ Xp = ( I ↾ ℂ )
23	22	fneq1i	⊢ ( Xp Fn ℂ ↔ ( I ↾ ℂ ) Fn ℂ )
24	21 23	mpbir	⊢ Xp Fn ℂ
25	24	a1i	⊢ ( 𝐴 ∈ ℚ → Xp Fn ℂ )
26		fnconstg	⊢ ( 𝐴 ∈ ℚ → ( ℂ × { 𝐴 } ) Fn ℂ )
27		cnex	⊢ ℂ ∈ V
28	27	a1i	⊢ ( 𝐴 ∈ ℚ → ℂ ∈ V )
29		inidm	⊢ ( ℂ ∩ ℂ ) = ℂ
30	22	fveq1i	⊢ ( Xp ‘ ( 𝐴 + 1 ) ) = ( ( I ↾ ℂ ) ‘ ( 𝐴 + 1 ) )
31		fvresi	⊢ ( ( 𝐴 + 1 ) ∈ ℂ → ( ( I ↾ ℂ ) ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
32	30 31	eqtrid	⊢ ( ( 𝐴 + 1 ) ∈ ℂ → ( Xp ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
33	32	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( Xp ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
34		fvconst2g	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ ( 𝐴 + 1 ) ) = 𝐴 )
35	25 26 28 28 29 33 34	ofval	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = ( ( 𝐴 + 1 ) − 𝐴 ) )
36	20 35	mpdan	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = ( ( 𝐴 + 1 ) − 𝐴 ) )
37		ax-1cn	⊢ 1 ∈ ℂ
38		pncan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
39	1 37 38	sylancl	⊢ ( 𝐴 ∈ ℚ → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
40	36 39	eqtrd	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = 1 )
41		ax-1ne0	⊢ 1 ≠ 0
42	41	a1i	⊢ ( 𝐴 ∈ ℚ → 1 ≠ 0 )
43	40 42	eqnetrd	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) ≠ 0 )
44		ne0p	⊢ ( ( ( 𝐴 + 1 ) ∈ ℂ ∧ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) ≠ 0 ) → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
45	20 43 44	syl2anc	⊢ ( 𝐴 ∈ ℚ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
46		eldifsn	⊢ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ↔ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℚ ) ∧ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) )
47	18 45 46	sylanbrc	⊢ ( 𝐴 ∈ ℚ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
48	22	fveq1i	⊢ ( Xp ‘ 𝐴 ) = ( ( I ↾ ℂ ) ‘ 𝐴 )
49		fvresi	⊢ ( 𝐴 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝐴 ) = 𝐴 )
50	48 49	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( Xp ‘ 𝐴 ) = 𝐴 )
51	50	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( Xp ‘ 𝐴 ) = 𝐴 )
52		fvconst2g	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝐴 ) = 𝐴 )
53	25 26 28 28 29 51 52	ofval	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = ( 𝐴 − 𝐴 ) )
54	1 53	mpdan	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = ( 𝐴 − 𝐴 ) )
55	1	subidd	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 − 𝐴 ) = 0 )
56	54 55	eqtrd	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 )
57		fveq1	⊢ ( 𝑓 = ( Xp ∘f − ( ℂ × { 𝐴 } ) ) → ( 𝑓 ‘ 𝐴 ) = ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) )
58	57	eqeq1d	⊢ ( 𝑓 = ( Xp ∘f − ( ℂ × { 𝐴 } ) ) → ( ( 𝑓 ‘ 𝐴 ) = 0 ↔ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 ) )
59	58	rspcev	⊢ ( ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
60	47 56 59	syl2anc	⊢ ( 𝐴 ∈ ℚ → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
61		elqaa	⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
62	1 60 61	sylanbrc	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ 𝔸 )