This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )