Metamath Proof Explorer


Theorem nn0ltp1ne

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

Ref Expression
Assertion nn0ltp1ne A0B0A+1<BA<BBA+1

Proof

Step Hyp Ref Expression
1 nn0z A0A
2 nn0z B0B
3 zltp1ne ABA+1<BA<BBA+1
4 1 2 3 syl2an A0B0A+1<BA<BBA+1