Theorem uzsubsubfz1

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

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

Proof

Step	Hyp	Ref	Expression
1		elnnuz	$$⊢L\in \mathbb{N}\leftrightarrow L\in {\mathbb{Z}}_{\ge 1}$$
2		uzsubsubfz	$$⊢\left(L\in {\mathbb{Z}}_{\ge 1}\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to N-\left(L-1\right)\in \left(1\dots N\right)$$
3	1 2	sylanb	$$⊢\left(L\in \mathbb{N}\wedge N\in {\mathbb{Z}}_{\ge L}\right)\to N-\left(L-1\right)\in \left(1\dots N\right)$$