Theorem zre

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

	Ref	Expression
Assertion	zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elz	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
2	1	simplbi	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )