Metamath Proof Explorer


Theorem nnltp1ne

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

Ref Expression
Assertion nnltp1ne ABA+1<BA<BBA+1

Proof

Step Hyp Ref Expression
1 nnz AA
2 nnz BB
3 zltp1ne ABA+1<BA<BBA+1
4 1 2 3 syl2an ABA+1<BA<BBA+1