fzval2

Description: An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Assertion	fzval2	$⊢ (M \in ℤ \land N \in ℤ) \to (M \dots N) = [M, N] \cap ℤ$

Step	Hyp	Ref	Expression
1		fzval	$⊢ (M \in ℤ \land N \in ℤ) \to (M \dots N) = \{k \in ℤ \| (M \leq k \land k \leq N)\}$
2		zssre	$⊢ ℤ \subseteq ℝ$
3		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
4	2 3	sstri	$⊢ ℤ \subseteq ℝ^{*}$
5	4	sseli	$⊢ M \in ℤ \to M \in ℝ^{*}$
6	4	sseli	$⊢ N \in ℤ \to N \in ℝ^{*}$
7		iccval	$⊢ (M \in ℝ^{} \land N \in ℝ^{}) \to [M, N] = \{k \in ℝ^{*} \| (M \leq k \land k \leq N)\}$
8	5 6 7	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to [M, N] = \{k \in ℝ^{*} \| (M \leq k \land k \leq N)\}$
9	8	ineq1d	$⊢ (M \in ℤ \land N \in ℤ) \to [M, N] \cap ℤ = \{k \in ℝ^{*} \| (M \leq k \land k \leq N)\} \cap ℤ$
10		inrab2	$⊢ \{k \in ℝ^{} \| (M \leq k \land k \leq N)\} \cap ℤ = \{k \in (ℝ^{} \cap ℤ) \| (M \leq k \land k \leq N)\}$
11		sseqin2	$⊢ ℤ \subseteq ℝ^{} \leftrightarrow ℝ^{} \cap ℤ = ℤ$
12	4 11	mpbi	$⊢ ℝ^{*} \cap ℤ = ℤ$
13	12	rabeqi	$⊢ \{k \in (ℝ^{*} \cap ℤ) \| (M \leq k \land k \leq N)\} = \{k \in ℤ \| (M \leq k \land k \leq N)\}$
14	10 13	eqtri	$⊢ \{k \in ℝ^{*} \| (M \leq k \land k \leq N)\} \cap ℤ = \{k \in ℤ \| (M \leq k \land k \leq N)\}$
15	9 14	eqtr2di	$⊢ (M \in ℤ \land N \in ℤ) \to \{k \in ℤ \| (M \leq k \land k \leq N)\} = [M, N] \cap ℤ$
16	1 15	eqtrd	$⊢ (M \in ℤ \land N \in ℤ) \to (M \dots N) = [M, N] \cap ℤ$

Metamath Proof Explorer