Metamath Proof Explorer


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 ( 𝐴 ∈ ℚ → ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( 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 syl5eq ( ( 𝐴 + 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 ) ∈ ℂ ) → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = ( ( 𝐴 + 1 ) − 𝐴 ) )
36 20 35 mpdan ( 𝐴 ∈ ℚ → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = ( ( 𝐴 + 1 ) − 𝐴 ) )
37 ax-1cn 1 ∈ ℂ
38 pncan2 ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
39 1 37 38 sylancl ( 𝐴 ∈ ℚ → ( ( 𝐴 + 1 ) − 𝐴 ) = 1 )
40 36 39 eqtrd ( 𝐴 ∈ ℚ → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) = 1 )
41 ax-1ne0 1 ≠ 0
42 41 a1i ( 𝐴 ∈ ℚ → 1 ≠ 0 )
43 40 42 eqnetrd ( 𝐴 ∈ ℚ → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) ≠ 0 )
44 ne0p ( ( ( 𝐴 + 1 ) ∈ ℂ ∧ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ ( 𝐴 + 1 ) ) ≠ 0 ) → ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
45 20 43 44 syl2anc ( 𝐴 ∈ ℚ → ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
46 eldifsn ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ↔ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℚ ) ∧ ( Xpf − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) )
47 18 45 46 sylanbrc ( 𝐴 ∈ ℚ → ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
48 22 fveq1i ( Xp𝐴 ) = ( ( I ↾ ℂ ) ‘ 𝐴 )
49 fvresi ( 𝐴 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝐴 ) = 𝐴 )
50 48 49 syl5eq ( 𝐴 ∈ ℂ → ( Xp𝐴 ) = 𝐴 )
51 50 adantl ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( Xp𝐴 ) = 𝐴 )
52 fvconst2g ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝐴 ) = 𝐴 )
53 25 26 28 28 29 51 52 ofval ( ( 𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ ) → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = ( 𝐴𝐴 ) )
54 1 53 mpdan ( 𝐴 ∈ ℚ → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = ( 𝐴𝐴 ) )
55 1 subidd ( 𝐴 ∈ ℚ → ( 𝐴𝐴 ) = 0 )
56 54 55 eqtrd ( 𝐴 ∈ ℚ → ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 )
57 fveq1 ( 𝑓 = ( Xpf − ( ℂ × { 𝐴 } ) ) → ( 𝑓𝐴 ) = ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) )
58 57 eqeq1d ( 𝑓 = ( Xpf − ( ℂ × { 𝐴 } ) ) → ( ( 𝑓𝐴 ) = 0 ↔ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 ) )
59 58 rspcev ( ( ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( ( Xpf − ( ℂ × { 𝐴 } ) ) ‘ 𝐴 ) = 0 ) → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 )
60 47 56 59 syl2anc ( 𝐴 ∈ ℚ → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 )
61 elqaa ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑓𝐴 ) = 0 ) )
62 1 60 61 sylanbrc ( 𝐴 ∈ ℚ → 𝐴 ∈ 𝔸 )