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