Theorem uznn0sub

Description: The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005)

	Ref	Expression
Assertion	uznn0sub	|- ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		eluz2	|- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2		znn0sub	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )
3	2	biimp3a	|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( N - M ) e. NN0 )
4	1 3	sylbi	|- ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )