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

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → 𝐿 ∈ ℕ0 )
2		eluznn0	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → 𝑁 ∈ ℕ0 )
3		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → 𝐿 ≤ 𝑁 )
4	3	adantl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → 𝐿 ≤ 𝑁 )
5		elfz2nn0	⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ≤ 𝑁 ) )
6	1 2 4 5	syl3anbrc	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → 𝐿 ∈ ( 0 ... 𝑁 ) )
7		fznn0sub2	⊢ ( 𝐿 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... 𝑁 ) )
8	6 7	syl	⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... 𝑁 ) )