Description: Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | nnltp1ne | |- ( ( A e. NN /\ B e. NN ) -> ( ( A + 1 ) < B <-> ( A < B /\ B =/= ( A + 1 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnz | |- ( A e. NN -> A e. ZZ ) |
|
2 | nnz | |- ( B e. NN -> 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. NN /\ B e. NN ) -> ( ( A + 1 ) < B <-> ( A < B /\ B =/= ( A + 1 ) ) ) ) |