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