Metamath Proof Explorer

Theorem elaa

Description: Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion elaa ⊢ A ∈ 𝔸 ↔ A ∈ ℂ ∧ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f ⁡ A = 0

Proof

Step Hyp Ref Expression
1 df-aa ⊢ 𝔸 = ⋃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f -1 0
2 1 eleq2i ⊢ A ∈ 𝔸 ↔ A ∈ ⋃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f -1 0
3 eliun ⊢ A ∈ ⋃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f -1 0 ↔ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 A ∈ f -1 0
4 eldifi ⊢ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 → f ∈ Poly ⁡ ℤ
5 plyf ⊢ f ∈ Poly ⁡ ℤ → f : ℂ ⟶ ℂ
6 ffn ⊢ f : ℂ ⟶ ℂ → f Fn ℂ
7 fniniseg ⊢ f Fn ℂ → A ∈ f -1 0 ↔ A ∈ ℂ ∧ f ⁡ A = 0
8 4 5 6 7 4syl ⊢ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 → A ∈ f -1 0 ↔ A ∈ ℂ ∧ f ⁡ A = 0
9 8 rexbiia ⊢ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 A ∈ f -1 0 ↔ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 A ∈ ℂ ∧ f ⁡ A = 0
10 r19.42v ⊢ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 A ∈ ℂ ∧ f ⁡ A = 0 ↔ A ∈ ℂ ∧ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f ⁡ A = 0
11 9 10 bitri ⊢ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 A ∈ f -1 0 ↔ A ∈ ℂ ∧ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f ⁡ A = 0
12 3 11 bitri ⊢ A ∈ ⋃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f -1 0 ↔ A ∈ ℂ ∧ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f ⁡ A = 0
13 2 12 bitri ⊢ A ∈ 𝔸 ↔ A ∈ ℂ ∧ ∃ f ∈ Poly ⁡ ℤ ∖ 0 𝑝 f ⁡ A = 0