Metamath Proof Explorer

Theorem nnlem1lt

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

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

Proof

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