Theorem fznn0sub

Description: Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fznn0sub	$$⊢K\in \left(M\dots N\right)\to N-K\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		elfzuz3	$$⊢K\in \left(M\dots N\right)\to N\in {\mathbb{Z}}_{\ge K}$$
2		uznn0sub	$$⊢N\in {\mathbb{Z}}_{\ge K}\to N-K\in {\mathbb{N}}_0$$
3	1 2	syl	$$⊢K\in \left(M\dots N\right)\to N-K\in {\mathbb{N}}_0$$