Metamath Proof Explorer

Theorem eluzp1l

Description: Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005)

Ref Expression
Assertion eluzp1l ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → M < N

Proof

Step Hyp Ref Expression
1 eluzle ⊢ N ∈ ℤ ≥ M + 1 → M + 1 ≤ N
2 1 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → M + 1 ≤ N
3 eluzelz ⊢ N ∈ ℤ ≥ M + 1 → N ∈ ℤ
4 zltp1le ⊢ M ∈ ℤ ∧ N ∈ ℤ → M < N ↔ M + 1 ≤ N
5 3 4 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → M < N ↔ M + 1 ≤ N
6 2 5 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → M < N