Theorem uzsubfz0

Description: Membership of an integer greater than L decreased by L in a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 16-Sep-2018)

	Ref	Expression
Assertion	uzsubfz0	$$⊢\left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to N-L\in \left(0\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to L\in {\mathbb{N}}_0$$
2		eluznn0	$$⊢\left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to N\in {\mathbb{N}}_0$$
3		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge L}\to L\le N$$
4	3	adantl	$$⊢\left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to L\le N$$
5		elfz2nn0	$$⊢L\in \left(0\dots N\right)\leftrightarrow \left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\wedge L\le N\right)$$
6	1 2 4 5	syl3anbrc	$$⊢\left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to L\in \left(0\dots N\right)$$
7		fznn0sub2	$$⊢L\in \left(0\dots N\right)\to N-L\in \left(0\dots N\right)$$
8	6 7	syl	$$⊢\left(L\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to N-L\in \left(0\dots N\right)$$