fzo0to42pr

Description: A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017)

		Ref	Expression
	Assertion	fzo0to42pr	$⊢ (0 ..^4) = \{0, 1\} \cup \{2, 3\}$

Step	Hyp	Ref	Expression
1		2nn0	$⊢ 2 \in ℕ_{0}$
2		4nn0	$⊢ 4 \in ℕ_{0}$
3		2re	$⊢ 2 \in ℝ$
4		4re	$⊢ 4 \in ℝ$
5		2lt4	$⊢ 2 < 4$
6	3 4 5	ltleii	$⊢ 2 \leq 4$
7		elfz2nn0	$⊢ 2 \in (0 \dots 4) \leftrightarrow (2 \in ℕ_{0} \land 4 \in ℕ_{0} \land 2 \leq 4)$
8	1 2 6 7	mpbir3an	$⊢ 2 \in (0 \dots 4)$
9		fzosplit	$⊢ 2 \in (0 \dots 4) \to (0 ..^4) = (0 ..^2) \cup (2 ..^4)$
10	8 9	ax-mp	$⊢ (0 ..^4) = (0 ..^2) \cup (2 ..^4)$
11		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
12		4z	$⊢ 4 \in ℤ$
13		fzoval	$⊢ 4 \in ℤ \to (2 ..^4) = (2 \dots 4 - 1)$
14	12 13	ax-mp	$⊢ (2 ..^4) = (2 \dots 4 - 1)$
15		4m1e3	$⊢ 4 - 1 = 3$
16		df-3	$⊢ 3 = 2 + 1$
17	15 16	eqtri	$⊢ 4 - 1 = 2 + 1$
18	17	oveq2i	$⊢ (2 \dots 4 - 1) = (2 \dots 2 + 1)$
19		2z	$⊢ 2 \in ℤ$
20		fzpr	$⊢ 2 \in ℤ \to (2 \dots 2 + 1) = \{2, 2 + 1\}$
21	19 20	ax-mp	$⊢ (2 \dots 2 + 1) = \{2, 2 + 1\}$
22	18 21	eqtri	$⊢ (2 \dots 4 - 1) = \{2, 2 + 1\}$
23		2p1e3	$⊢ 2 + 1 = 3$
24	23	preq2i	$⊢ \{2, 2 + 1\} = \{2, 3\}$
25	14 22 24	3eqtri	$⊢ (2 ..^4) = \{2, 3\}$
26	11 25	uneq12i	$⊢ (0 ..^2) \cup (2 ..^4) = \{0, 1\} \cup \{2, 3\}$
27	10 26	eqtri	$⊢ (0 ..^4) = \{0, 1\} \cup \{2, 3\}$

Metamath Proof Explorer