fz0to4untppr

Description: An integer range from 0 to 4 is the union of a triple and a pair. (Contributed by Alexander van der Vekens, 13-Aug-2017) (Proof shortened by AV, 7-Aug-2025)

		Ref	Expression
	Assertion	fz0to4untppr	$⊢ (0 \dots 4) = \{0, 1, 2\} \cup \{3, 4\}$

Proof

Step	Hyp	Ref	Expression
1		2p1e3	$⊢ 2 + 1 = 3$
2		0z	$⊢ 0 \in ℤ$
3		3z	$⊢ 3 \in ℤ$
4		0re	$⊢ 0 \in ℝ$
5		3re	$⊢ 3 \in ℝ$
6		3pos	$⊢ 0 < 3$
7	4 5 6	ltleii	$⊢ 0 \leq 3$
8		eluz2	$⊢ 3 \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land 3 \in ℤ \land 0 \leq 3)$
9	2 3 7 8	mpbir3an	$⊢ 3 \in ℤ_{\geq 0}$
10	1 9	eqeltri	$⊢ 2 + 1 \in ℤ_{\geq 0}$
11		2z	$⊢ 2 \in ℤ$
12		4z	$⊢ 4 \in ℤ$
13		2re	$⊢ 2 \in ℝ$
14		4re	$⊢ 4 \in ℝ$
15		2lt4	$⊢ 2 < 4$
16	13 14 15	ltleii	$⊢ 2 \leq 4$
17		eluz2	$⊢ 4 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 4 \in ℤ \land 2 \leq 4)$
18	11 12 16 17	mpbir3an	$⊢ 4 \in ℤ_{\geq 2}$
19		fzsplit2	$⊢ (2 + 1 \in ℤ_{\geq 0} \land 4 \in ℤ_{\geq 2}) \to (0 \dots 4) = (0 \dots 2) \cup (2 + 1 \dots 4)$
20	10 18 19	mp2an	$⊢ (0 \dots 4) = (0 \dots 2) \cup (2 + 1 \dots 4)$
21		fz0tp	$⊢ (0 \dots 2) = \{0, 1, 2\}$
22	1	oveq1i	$⊢ (2 + 1 \dots 4) = (3 \dots 4)$
23		df-4	$⊢ 4 = 3 + 1$
24	23	oveq2i	$⊢ (3 \dots 4) = (3 \dots 3 + 1)$
25		fzpr	$⊢ 3 \in ℤ \to (3 \dots 3 + 1) = \{3, 3 + 1\}$
26	3 25	ax-mp	$⊢ (3 \dots 3 + 1) = \{3, 3 + 1\}$
27		3p1e4	$⊢ 3 + 1 = 4$
28	27	preq2i	$⊢ \{3, 3 + 1\} = \{3, 4\}$
29	24 26 28	3eqtri	$⊢ (3 \dots 4) = \{3, 4\}$
30	22 29	eqtri	$⊢ (2 + 1 \dots 4) = \{3, 4\}$
31	21 30	uneq12i	$⊢ (0 \dots 2) \cup (2 + 1 \dots 4) = \{0, 1, 2\} \cup \{3, 4\}$
32	20 31	eqtri	$⊢ (0 \dots 4) = \{0, 1, 2\} \cup \{3, 4\}$

Metamath Proof Explorer

Theorem fz0to4untppr

Proof