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

Metamath Proof Explorer

Theorem znn0sub

Description: The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub .) (Contributed by NM, 14-Jul-2005)

Ref Expression
Assertion znn0sub 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 zre 
 |-  ( M e. ZZ -> M e. RR )
3 subge0 
 |-  ( ( N e. RR /\ M e. RR ) -> ( 0 <_ ( N - M ) <-> M <_ N ) )
4 1 2 3 syl2an 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( 0 <_ ( N - M ) <-> M <_ N ) )
5 zsubcl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
6 5 biantrurd 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( 0 <_ ( N - M ) <-> ( ( N - M ) e. ZZ /\ 0 <_ ( N - M ) ) ) )
7 4 6 bitr3d 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( M <_ N <-> ( ( N - M ) e. ZZ /\ 0 <_ ( N - M ) ) ) )
8 7 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( ( N - M ) e. ZZ /\ 0 <_ ( N - M ) ) ) )
9 elnn0z 
 |-  ( ( N - M ) e. NN0 <-> ( ( N - M ) e. ZZ /\ 0 <_ ( N - M ) ) )
10 8 9 bitr4di 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )