This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (L \in ℕ \land N \in ℤ_{\geq L}) \to N - (L - 1) \in (1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elnnuz	$⊢ L \in ℕ \leftrightarrow L \in ℤ_{\geq 1}$
2		uzsubsubfz	$⊢ (L \in ℤ_{\geq 1} \land N \in ℤ_{\geq L}) \to N - (L - 1) \in (1 \dots N)$
3	1 2	sylanb	$⊢ (L \in ℕ \land N \in ℤ_{\geq L}) \to N - (L - 1) \in (1 \dots N)$