This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfz4

Description: Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005) (Revised by Mario Carneiro, 28-Apr-2015)

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

Step	Hyp	Ref	Expression
1		elfz2	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N))$
2	1	biimpri	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \to K \in (M \dots N)$