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

Metamath Proof Explorer

Theorem nnleltp1

Description: Positive integer ordering relation. (Contributed by NM, 13-Aug-2001) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnleltp1 ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ≤ B ↔ A < B + 1

Proof

Step Hyp Ref Expression
1 nnz ⊢ A ∈ ℕ → A ∈ ℤ
2 nnz ⊢ B ∈ ℕ → B ∈ ℤ
3 zleltp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ≤ B ↔ A < B + 1
4 1 2 3 syl2an ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ≤ B ↔ A < B + 1