Metamath Proof Explorer


Theorem znnsub

Description: The positive difference of unequal integers is a positive integer. (Generalization of nnsub .) (Contributed by NM, 11-May-2004)

Ref Expression
Assertion znnsub
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )

Proof

Step Hyp Ref Expression
1 zre
 |-  ( M e. ZZ -> M e. RR )
2 zre
 |-  ( N e. ZZ -> N e. RR )
3 posdif
 |-  ( ( M e. RR /\ N e. RR ) -> ( M < N <-> 0 < ( N - M ) ) )
4 1 2 3 syl2an
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> 0 < ( N - M ) ) )
5 zsubcl
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
6 5 ancoms
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N - M ) e. ZZ )
7 6 biantrurd
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 < ( N - M ) <-> ( ( N - M ) e. ZZ /\ 0 < ( N - M ) ) ) )
8 4 7 bitrd
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( ( N - M ) e. ZZ /\ 0 < ( N - M ) ) ) )
9 elnnz
 |-  ( ( N - M ) e. NN <-> ( ( N - M ) e. ZZ /\ 0 < ( N - M ) ) )
10 8 9 bitr4di
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )