elfzm11

Description: Membership in a finite set of sequential integers. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	elfzm11	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (K \in ℤ \land M \leq K \land K < N))$

Step	Hyp	Ref	Expression
1		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
2		elfz1	$⊢ (M \in ℤ \land N - 1 \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N - 1))$
3	1 2	sylan2	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N - 1))$
4		zltlem1	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow K \leq N - 1)$
5	4	anbi2d	$⊢ (K \in ℤ \land N \in ℤ) \to ((M \leq K \land K < N) \leftrightarrow (M \leq K \land K \leq N - 1))$
6	5	expcom	$⊢ N \in ℤ \to (K \in ℤ \to ((M \leq K \land K < N) \leftrightarrow (M \leq K \land K \leq N - 1)))$
7	6	pm5.32d	$⊢ N \in ℤ \to ((K \in ℤ \land (M \leq K \land K < N)) \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N - 1)))$
8		3anass	$⊢ (K \in ℤ \land M \leq K \land K < N) \leftrightarrow (K \in ℤ \land (M \leq K \land K < N))$
9		3anass	$⊢ (K \in ℤ \land M \leq K \land K \leq N - 1) \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N - 1))$
10	7 8 9	3bitr4g	$⊢ N \in ℤ \to ((K \in ℤ \land M \leq K \land K < N) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N - 1))$
11	10	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to ((K \in ℤ \land M \leq K \land K < N) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N - 1))$
12	3 11	bitr4d	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N - 1) \leftrightarrow (K \in ℤ \land M \leq K \land K < N))$

Metamath Proof Explorer