Metamath Proof Explorer


Theorem zltp1ne

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

Ref Expression
Assertion zltp1ne A B A + 1 < B A < B B A + 1

Proof

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