fzpr

Description: A finite interval of integers with two elements. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	fzpr	$⊢ M \in ℤ \to (M \dots M + 1) = \{M, M + 1\}$

Step	Hyp	Ref	Expression
1		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
2		elfzp1	$⊢ M \in ℤ_{\geq M} \to (m \in (M \dots M + 1) \leftrightarrow (m \in (M \dots M) \lor m = M + 1))$
3	1 2	syl	$⊢ M \in ℤ \to (m \in (M \dots M + 1) \leftrightarrow (m \in (M \dots M) \lor m = M + 1))$
4		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
5	4	eleq2d	$⊢ M \in ℤ \to (m \in (M \dots M) \leftrightarrow m \in \{M\})$
6		velsn	$⊢ m \in \{M\} \leftrightarrow m = M$
7	5 6	bitrdi	$⊢ M \in ℤ \to (m \in (M \dots M) \leftrightarrow m = M)$
8	7	orbi1d	$⊢ M \in ℤ \to ((m \in (M \dots M) \lor m = M + 1) \leftrightarrow (m = M \lor m = M + 1))$
9	3 8	bitrd	$⊢ M \in ℤ \to (m \in (M \dots M + 1) \leftrightarrow (m = M \lor m = M + 1))$
10		vex	$⊢ m \in V$
11	10	elpr	$⊢ m \in \{M, M + 1\} \leftrightarrow (m = M \lor m = M + 1)$
12	9 11	bitr4di	$⊢ M \in ℤ \to (m \in (M \dots M + 1) \leftrightarrow m \in \{M, M + 1\})$
13	12	eqrdv	$⊢ M \in ℤ \to (M \dots M + 1) = \{M, M + 1\}$

Metamath Proof Explorer