Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
2		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
3	1 2	sylan2	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N - M \in ℤ$
4		simpl	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in ℤ$
5		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
6	5	adantl	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 0 \leq M$
7		zre	$⊢ N \in ℤ \to N \in ℝ$
8		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
9		subge02	$⊢ (N \in ℝ \land M \in ℝ) \to (0 \leq M \leftrightarrow N - M \leq N)$
10	7 8 9	syl2an	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (0 \leq M \leftrightarrow N - M \leq N)$
11	6 10	mpbid	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N - M \leq N$
12		eluz2	$⊢ N \in ℤ_{\geq (N - M)} \leftrightarrow (N - M \in ℤ \land N \in ℤ \land N - M \leq N)$
13	3 4 11 12	syl3anbrc	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in ℤ_{\geq (N - M)}$
14		eluzfz2	$⊢ N \in ℤ_{\geq (N - M)} \to N \in (N - M \dots N)$
15	13 14	syl	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in (N - M \dots N)$