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

Proof

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