Metamath Proof Explorer

Theorem nnltp1ne

Description: Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023)

Ref Expression
Assertion nnltp1ne ⊢ A ∈ ℕ ∧ B ∈ ℕ → A + 1 < B ↔ A < B ∧ B ≠ A + 1

Proof

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