Metamath Proof Explorer


Theorem nnltp1ne

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

Ref Expression
Assertion nnltp1ne ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵𝐵 ≠ ( 𝐴 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 nnz ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
2 nnz ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
3 zltp1ne ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵𝐵 ≠ ( 𝐴 + 1 ) ) ) )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵𝐵 ≠ ( 𝐴 + 1 ) ) ) )