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