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

Metamath Proof Explorer

Theorem eluz

Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005)

Ref Expression
Assertion eluz ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ M ↔ M ≤ N

Proof

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