Metamath Proof Explorer


Theorem aacjcl

Description: The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion aacjcl A 𝔸 A 𝔸

Proof

Step Hyp Ref Expression
1 cjcl A A
2 1 adantr A f Poly 0 𝑝 f A = 0 A
3 fveq2 f A = 0 f A = 0
4 cj0 0 = 0
5 3 4 eqtrdi f A = 0 f A = 0
6 difss Poly 0 𝑝 Poly
7 zssre
8 ax-resscn
9 plyss Poly Poly
10 7 8 9 mp2an Poly Poly
11 6 10 sstri Poly 0 𝑝 Poly
12 11 sseli f Poly 0 𝑝 f Poly
13 id A A
14 plyrecj f Poly A f A = f A
15 12 13 14 syl2anr A f Poly 0 𝑝 f A = f A
16 15 eqeq1d A f Poly 0 𝑝 f A = 0 f A = 0
17 5 16 syl5ib A f Poly 0 𝑝 f A = 0 f A = 0
18 17 reximdva A f Poly 0 𝑝 f A = 0 f Poly 0 𝑝 f A = 0
19 18 imp A f Poly 0 𝑝 f A = 0 f Poly 0 𝑝 f A = 0
20 2 19 jca A f Poly 0 𝑝 f A = 0 A f Poly 0 𝑝 f A = 0
21 elaa A 𝔸 A f Poly 0 𝑝 f A = 0
22 elaa A 𝔸 A f Poly 0 𝑝 f A = 0
23 20 21 22 3imtr4i A 𝔸 A 𝔸