Theorem uznn0sub

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

	Ref	Expression
Assertion	uznn0sub	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N-M\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\le N\right)$$
2		znn0sub	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M\le N\leftrightarrow N-M\in {\mathbb{N}}_0\right)$$
3	2	biimp3a	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\le N\right)\to N-M\in {\mathbb{N}}_0$$
4	1 3	sylbi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N-M\in {\mathbb{N}}_0$$