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)

	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		df-3	$$⊢3=2+1$$
2		2cn	$$⊢2\in ℂ$$
3	2	addid2i	$$⊢0+2=2$$
4	3	eqcomi	$$⊢2=0+2$$
5	4	oveq1i	$$⊢2+1=0+2+1$$
6	1 5	eqtri	$$⊢3=0+2+1$$
7		3z	$$⊢3\in \mathbb{Z}$$
8		0re	$$⊢0\in ℝ$$
9		3re	$$⊢3\in ℝ$$
10		3pos	$$⊢0<3$$
11	8 9 10	ltleii	$$⊢0\le 3$$
12		0z	$$⊢0\in \mathbb{Z}$$
13	12	eluz1i	$$⊢3\in {\mathbb{Z}}_{\ge 0}\leftrightarrow \left(3\in \mathbb{Z}\wedge 0\le 3\right)$$
14	7 11 13	mpbir2an	$$⊢3\in {\mathbb{Z}}_{\ge 0}$$
15	6 14	eqeltrri	$$⊢0+2+1\in {\mathbb{Z}}_{\ge 0}$$
16		4z	$$⊢4\in \mathbb{Z}$$
17		2re	$$⊢2\in ℝ$$
18		4re	$$⊢4\in ℝ$$
19		2lt4	$$⊢2<4$$
20	17 18 19	ltleii	$$⊢2\le 4$$
21		2z	$$⊢2\in \mathbb{Z}$$
22	21	eluz1i	$$⊢4\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(4\in \mathbb{Z}\wedge 2\le 4\right)$$
23	16 20 22	mpbir2an	$$⊢4\in {\mathbb{Z}}_{\ge 2}$$
24	4	fveq2i	$$⊢{\mathbb{Z}}_{\ge 2}={\mathbb{Z}}_{\ge \left(0+2\right)}$$
25	23 24	eleqtri	$$⊢4\in {\mathbb{Z}}_{\ge \left(0+2\right)}$$
26		fzsplit2	$$⊢\left(0+2+1\in {\mathbb{Z}}_{\ge 0}\wedge 4\in {\mathbb{Z}}_{\ge \left(0+2\right)}\right)\to \left(0\dots 4\right)=\left(0\dots 0+2\right)\cup \left(0+2+1\dots 4\right)$$
27	15 25 26	mp2an	$$⊢\left(0\dots 4\right)=\left(0\dots 0+2\right)\cup \left(0+2+1\dots 4\right)$$
28		fztp	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
29	12 28	ax-mp	$$⊢\left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
30		ax-1cn	$$⊢1\in ℂ$$
31		eqidd	$$⊢1\in ℂ\to 0=0$$
32		addid2	$$⊢1\in ℂ\to 0+1=1$$
33	3	a1i	$$⊢1\in ℂ\to 0+2=2$$
34	31 32 33	tpeq123d	$$⊢1\in ℂ\to \left\{0,0+1,0+2\right\}=\left\{0,1,2\right\}$$
35	30 34	ax-mp	$$⊢\left\{0,0+1,0+2\right\}=\left\{0,1,2\right\}$$
36	29 35	eqtri	$$⊢\left(0\dots 0+2\right)=\left\{0,1,2\right\}$$
37	3	a1i	$$⊢3\in \mathbb{Z}\to 0+2=2$$
38	37	oveq1d	$$⊢3\in \mathbb{Z}\to 0+2+1=2+1$$
39	38 1	eqtr4di	$$⊢3\in \mathbb{Z}\to 0+2+1=3$$
40	39	oveq1d	$$⊢3\in \mathbb{Z}\to \left(0+2+1\dots 4\right)=\left(3\dots 4\right)$$
41		eqid	$$⊢3=3$$
42		df-4	$$⊢4=3+1$$
43	41 42	pm3.2i	$$⊢\left(3=3\wedge 4=3+1\right)$$
44	43	a1i	$$⊢3\in \mathbb{Z}\to \left(3=3\wedge 4=3+1\right)$$
45		3lt4	$$⊢3<4$$
46	9 18 45	ltleii	$$⊢3\le 4$$
47	7	eluz1i	$$⊢4\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(4\in \mathbb{Z}\wedge 3\le 4\right)$$
48	16 46 47	mpbir2an	$$⊢4\in {\mathbb{Z}}_{\ge 3}$$
49		fzopth	$$⊢4\in {\mathbb{Z}}_{\ge 3}\to \left(\left(3\dots 4\right)=\left(3\dots 3+1\right)\leftrightarrow \left(3=3\wedge 4=3+1\right)\right)$$
50	48 49	ax-mp	$$⊢\left(3\dots 4\right)=\left(3\dots 3+1\right)\leftrightarrow \left(3=3\wedge 4=3+1\right)$$
51	44 50	sylibr	$$⊢3\in \mathbb{Z}\to \left(3\dots 4\right)=\left(3\dots 3+1\right)$$
52		fzpr	$$⊢3\in \mathbb{Z}\to \left(3\dots 3+1\right)=\left\{3,3+1\right\}$$
53	51 52	eqtrd	$$⊢3\in \mathbb{Z}\to \left(3\dots 4\right)=\left\{3,3+1\right\}$$
54	42	eqcomi	$$⊢3+1=4$$
55	54	preq2i	$$⊢\left\{3,3+1\right\}=\left\{3,4\right\}$$
56	53 55	eqtrdi	$$⊢3\in \mathbb{Z}\to \left(3\dots 4\right)=\left\{3,4\right\}$$
57	40 56	eqtrd	$$⊢3\in \mathbb{Z}\to \left(0+2+1\dots 4\right)=\left\{3,4\right\}$$
58	7 57	ax-mp	$$⊢\left(0+2+1\dots 4\right)=\left\{3,4\right\}$$
59	36 58	uneq12i	$$⊢\left(0\dots 0+2\right)\cup \left(0+2+1\dots 4\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$
60	27 59	eqtri	$$⊢\left(0\dots 4\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$