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		fveq1	⊢ ( 𝑓 = ( Xp ∘f − ( ℂ × { 𝐴 } ) ) → ( 𝑓 ‘ 𝐴 ) = ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) )
3	2	eqeq1d	⊢ ( 𝑓 = ( Xp ∘f − ( ℂ × { 𝐴 } ) ) → ( ( 𝑓 ‘ 𝐴 ) = 0 ↔ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 ) )
4		qsscn	⊢ ℚ ⊆ ℂ
5		1q	⊢ 1 ∈ ℚ
6		plyid	⊢ ( ( ℚ ⊆ ℂ ∧ 1 ∈ ℚ ) → Xp ∈ ( Poly ‘ ℚ ) )
7	4 5 6	mp2an	⊢ Xp ∈ ( Poly ‘ ℚ )
8	7	a1i	⊢ ( 𝐴 ∈ ℚ → Xp ∈ ( Poly ‘ ℚ ) )
9		plyconst	⊢ ( ( ℚ ⊆ ℂ ∧ 𝐴 ∈ ℚ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℚ ) )
10	4 9	mpan	⊢ ( 𝐴 ∈ ℚ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℚ ) )
11		qaddcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 + 𝑦 ) ∈ ℚ )
12	11	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 + 𝑦 ) ∈ ℚ )
13		qmulcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
14	13	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
15		qnegcl	⊢ ( 1 ∈ ℚ → - 1 ∈ ℚ )
16	5 15	mp1i	⊢ ( 𝐴 ∈ ℚ → - 1 ∈ ℚ )
17	8 10 12 14 16	plysub	⊢ ( 𝐴 ∈ ℚ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℚ ) )
18		peano2cn	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 1 ) ∈ ℂ )
19	1 18	syl	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 + 1 ) ∈ ℂ )
20		fnresi	⊢ ( I ↾ ℂ ) Fn ℂ
21		df-idp	⊢ Xp = ( I ↾ ℂ )
22	21	fneq1i	⊢ ( Xp Fn ℂ ↔ ( I ↾ ℂ ) Fn ℂ )
23	20 22	mpbir	⊢ Xp Fn ℂ
24	23	a1i	⊢ ( 𝐴 ∈ ℚ → Xp Fn ℂ )
25		fnconstg	⊢ ( 𝐴 ∈ ℚ → ( ℂ × { 𝐴 } ) Fn ℂ )
26		cnex	⊢ ℂ ∈ V
27	26	a1i	⊢ ( 𝐴 ∈ ℚ → ℂ ∈ V )
28		inidm	⊢ ( ℂ ∩ ℂ ) = ℂ
29		idpfv	⊢ ( ( 𝐴 + 1 ) ∈ ℂ → ( Xp ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
30	29	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( Xp ‘ ( 𝐴 + 1 ) ) = ( 𝐴 + 1 ) )
31		fvconst2g	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ ( 𝐴 + 1 ) ) = 𝐴 )
32	24 25 27 27 28 30 31	ofval	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = ( ( 𝐴 + 1 ) − 𝐴 ) )
33	19 32	mpdan	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = ( ( 𝐴 + 1 ) − 𝐴 ) )
34		ax-1cn	⊢ 1 ∈ ℂ
35		pncan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
36	1 34 35	sylancl	⊢ ( 𝐴 ∈ ℚ → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
37	33 36	eqtrd	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = 1 )
38		ax-1ne0	⊢ 1 ≠ 0
39	38	a1i	⊢ ( 𝐴 ∈ ℚ → 1 ≠ 0 )
40	37 39	eqnetrd	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) ≠ 0 )
41		ne0p	⊢ ( ( ( 𝐴 + 1 ) ∈ ℂ ∧ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) ≠ 0 ) → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
42	19 40 41	syl2anc	⊢ ( 𝐴 ∈ ℚ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
43	17 42	eldifsnd	⊢ ( 𝐴 ∈ ℚ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
44		idpfv	⊢ ( 𝐴 ∈ ℂ → ( Xp ‘ 𝐴 ) = 𝐴 )
45	44	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( Xp ‘ 𝐴 ) = 𝐴 )
46		fvconst2g	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝐴 ) = 𝐴 )
47	24 25 27 27 28 45 46	ofval	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = ( 𝐴 − 𝐴 ) )
48	1 47	mpdan	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = ( 𝐴 − 𝐴 ) )
49	1	subidd	⊢ ( 𝐴 ∈ ℚ → ( 𝐴 − 𝐴 ) = 0 )
50	48 49	eqtrd	⊢ ( 𝐴 ∈ ℚ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 )
51	3 43 50	rspcedvdw	⊢ ( 𝐴 ∈ ℚ → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
52		elqaa	⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
53	1 51 52	sylanbrc	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ 𝔸 )