Description: Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0ltp1ne | |- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A + 1 ) < B <-> ( A < B /\ B =/= ( A + 1 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0z | |- ( A e. NN0 -> A e. ZZ ) |
|
2 | nn0z | |- ( B e. NN0 -> B e. ZZ ) |
|
3 | zltp1ne | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A + 1 ) < B <-> ( A < B /\ B =/= ( A + 1 ) ) ) ) |
|
4 | 1 2 3 | syl2an | |- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A + 1 ) < B <-> ( A < B /\ B =/= ( A + 1 ) ) ) ) |