Metamath Proof Explorer


Theorem zrei

Description: An integer is a real number. (Contributed by NM, 14-Jul-2005)

Ref Expression
Hypothesis zrei.1 ⊢ A ∈ ℤ
Assertion zrei ⊢ A ∈ ℝ

Proof

Step Hyp Ref Expression
1 zrei.1 ⊢ A ∈ ℤ
2 zre ⊢ A ∈ ℤ → A ∈ ℝ
3 1 2 ax-mp ⊢ A ∈ ℝ