elfz

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

		Ref	Expression
	Assertion	elfz	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$

Step	Hyp	Ref	Expression
1		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N))$
2		3anass	$⊢ (K \in ℤ \land M \leq K \land K \leq N) \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N))$
3	2	baib	$⊢ K \in ℤ \to ((K \in ℤ \land M \leq K \land K \leq N) \leftrightarrow (M \leq K \land K \leq N))$
4	1 3	sylan9bb	$⊢ ((M \in ℤ \land N \in ℤ) \land K \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$
5	4	3impa	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$
6	5	3comr	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (M \leq K \land K \leq N))$

Metamath Proof Explorer