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 imbitrid ⊢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‾∈𝔸