Theorem elfzlble

Description: Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018)

	Ref	Expression
Assertion	elfzlble	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ( ( 𝑁 − 𝑀 ) ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
2		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
3	1 2	sylan2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
4		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
5		nn0ge0	⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
6	5	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ 𝑀 )
7		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
9		subge02	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ 𝑀 ↔ ( 𝑁 − 𝑀 ) ≤ 𝑁 ) )
10	7 8 9	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ 𝑀 ↔ ( 𝑁 − 𝑀 ) ≤ 𝑁 ) )
11	6 10	mpbid	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 − 𝑀 ) ≤ 𝑁 )
12		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝑀 ) ) ↔ ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ≤ 𝑁 ) )
13	3 4 11 12	syl3anbrc	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝑀 ) ) )
14		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 𝑀 ) ) → 𝑁 ∈ ( ( 𝑁 − 𝑀 ) ... 𝑁 ) )
15	13 14	syl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑁 ∈ ( ( 𝑁 − 𝑀 ) ... 𝑁 ) )