Metamath Proof Explorer

Theorem nnltlem1

Description: Positive integer ordering relation. (Contributed by NM, 21-Jun-2005)

Ref Expression
Assertion nnltlem1 ⊢M∈ℕ∧N∈ℕ→M<N↔M≤N−1

Proof

Step Hyp Ref Expression
1 nnz ⊢M∈ℕ→M∈ℤ
2 nnz ⊢N∈ℕ→N∈ℤ
3 zltlem1 ⊢M∈ℤ∧N∈ℤ→M<N↔M≤N−1
4 1 2 3 syl2an ⊢M∈ℕ∧N∈ℕ→M<N↔M≤N−1