Metamath Proof Explorer


Theorem zltp1ne

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

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

Proof

Step Hyp Ref Expression
1 zre AA
2 zre BB
3 peano2re AA+1
4 ltlen A+1BA+1<BA+1BBA+1
5 3 4 sylan ABA+1<BA+1BBA+1
6 1 2 5 syl2an ABA+1<BA+1BBA+1
7 zltp1le ABA<BA+1B
8 7 anbi1d ABA<BBA+1A+1BBA+1
9 6 8 bitr4d ABA+1<BA<BBA+1