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

Metamath Proof Explorer

Theorem eluz1i

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

Ref Expression
Hypothesis eluz.1 ⊢ M ∈ ℤ
Assertion eluz1i ⊢ N ∈ ℤ ≥ M ↔ N ∈ ℤ ∧ M ≤ N

Proof

Step Hyp Ref Expression
1 eluz.1 ⊢ M ∈ ℤ
2 eluz1 ⊢ M ∈ ℤ → N ∈ ℤ ≥ M ↔ N ∈ ℤ ∧ M ≤ N
3 1 2 ax-mp ⊢ N ∈ ℤ ≥ M ↔ N ∈ ℤ ∧ M ≤ N