This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zre

Description: An integer is a real. (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion zre ⊢ N ∈ ℤ → N ∈ ℝ

Proof

Step Hyp Ref Expression
1 elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
2 1 simplbi ⊢ N ∈ ℤ → N ∈ ℝ