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	⊢ ( ( 𝐿 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 1 ) ) ∈ ( 1 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elnnuz	⊢ ( 𝐿 ∈ ℕ ↔ 𝐿 ∈ ( ℤ≥ ‘ 1 ) )
2		uzsubsubfz	⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 1 ) ) ∈ ( 1 ... 𝑁 ) )
3	1 2	sylanb	⊢ ( ( 𝐿 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 1 ) ) ∈ ( 1 ... 𝑁 ) )