Theorem fz0to5un2tp

Description: An integer range from 0 to 5 is the union of two triples. (Contributed by AV, 30-Jul-2025)

	Ref	Expression
Assertion	fz0to5un2tp	$$⊢\left(0\dots 5\right)=\left\{0,1,2\right\}\cup \left\{3,4,5\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		5nn0	$$⊢5\in {\mathbb{N}}_0$$
13	12	nn0zi	$$⊢5\in \mathbb{Z}$$
14		2re	$$⊢2\in ℝ$$
15		5re	$$⊢5\in ℝ$$
16		2lt5	$$⊢2<5$$
17	14 15 16	ltleii	$$⊢2\le 5$$
18		eluz2	$$⊢5\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 5\in \mathbb{Z}\wedge 2\le 5\right)$$
19	11 13 17 18	mpbir3an	$$⊢5\in {\mathbb{Z}}_{\ge 2}$$
20		fzsplit2	$$⊢\left(2+1\in {\mathbb{Z}}_{\ge 0}\wedge 5\in {\mathbb{Z}}_{\ge 2}\right)\to \left(0\dots 5\right)=\left(0\dots 2\right)\cup \left(2+1\dots 5\right)$$
21	10 19 20	mp2an	$$⊢\left(0\dots 5\right)=\left(0\dots 2\right)\cup \left(2+1\dots 5\right)$$
22		fz0tp	$$⊢\left(0\dots 2\right)=\left\{0,1,2\right\}$$
23	1	oveq1i	$$⊢\left(2+1\dots 5\right)=\left(3\dots 5\right)$$
24		3p2e5	$$⊢3+2=5$$
25	24	eqcomi	$$⊢5=3+2$$
26	25	oveq2i	$$⊢\left(3\dots 5\right)=\left(3\dots 3+2\right)$$
27		fztp	$$⊢3\in \mathbb{Z}\to \left(3\dots 3+2\right)=\left\{3,3+1,3+2\right\}$$
28	3 27	ax-mp	$$⊢\left(3\dots 3+2\right)=\left\{3,3+1,3+2\right\}$$
29		eqid	$$⊢3=3$$
30		id	$$⊢3=3\to 3=3$$
31		3p1e4	$$⊢3+1=4$$
32	31	a1i	$$⊢3=3\to 3+1=4$$
33	24	a1i	$$⊢3=3\to 3+2=5$$
34	30 32 33	tpeq123d	$$⊢3=3\to \left\{3,3+1,3+2\right\}=\left\{3,4,5\right\}$$
35	29 34	ax-mp	$$⊢\left\{3,3+1,3+2\right\}=\left\{3,4,5\right\}$$
36	26 28 35	3eqtri	$$⊢\left(3\dots 5\right)=\left\{3,4,5\right\}$$
37	23 36	eqtri	$$⊢\left(2+1\dots 5\right)=\left\{3,4,5\right\}$$
38	22 37	uneq12i	$$⊢\left(0\dots 2\right)\cup \left(2+1\dots 5\right)=\left\{0,1,2\right\}\cup \left\{3,4,5\right\}$$
39	21 38	eqtri	$$⊢\left(0\dots 5\right)=\left\{0,1,2\right\}\cup \left\{3,4,5\right\}$$