elfz5

Description: Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005)

		Ref	Expression
	Assertion	elfz5	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow K \leq N)$

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ K \in ℤ_{\geq M} \to K \in ℤ$
2		eluzel2	$⊢ K \in ℤ_{\geq M} \to M \in ℤ$
3	1 2	jca	$⊢ K \in ℤ_{\geq M} \to (K \in ℤ \land M \in ℤ)$
4		elfz	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$
5	4	3expa	$⊢ ((K \in ℤ \land M \in ℤ) \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$
6	3 5	sylan	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$
7		eluzle	$⊢ K \in ℤ_{\geq M} \to M \leq K$
8	7	biantrurd	$⊢ K \in ℤ_{\geq M} \to (K \leq N \leftrightarrow (M \leq K \land K \leq N))$
9	8	adantr	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K \leq N \leftrightarrow (M \leq K \land K \leq N))$
10	6 9	bitr4d	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow K \leq N)$

Metamath Proof Explorer