Theorem 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	$$⊢\left(0\dots 4\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$

Proof

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