Metamath Proof Explorer


Theorem zcn

Description: An integer is a complex number. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion zcn ⊢ N ∈ ℤ → N ∈ ℂ

Proof

Step Hyp Ref Expression
1 zre ⊢ N ∈ ℤ → N ∈ ℝ
2 1 recnd ⊢ N ∈ ℤ → N ∈ ℂ