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