Description: An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | aacn | ⊢ ( 𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elaa | ⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) ) | |
2 | 1 | simplbi | ⊢ ( 𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ ) |