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

Metamath Proof Explorer

Theorem eluzelz

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005)

Ref Expression
Assertion eluzelz ⊢ N ∈ ℤ ≥ M → N ∈ ℤ

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ N ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N
2 1 simp2bi ⊢ N ∈ ℤ ≥ M → N ∈ ℤ