Theorem fzo0to3tp

Description: A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017)

	Ref	Expression
Assertion	fzo0to3tp	$$⊢\left(0..^3\right)=\left\{0,1,2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		3z	$$⊢3\in \mathbb{Z}$$
2		fzoval	$$⊢3\in \mathbb{Z}\to \left(0..^3\right)=\left(0\dots 3-1\right)$$
3	1 2	ax-mp	$$⊢\left(0..^3\right)=\left(0\dots 3-1\right)$$
4		3m1e2	$$⊢3-1=2$$
5		2cn	$$⊢2\in ℂ$$
6	5	addid2i	$$⊢0+2=2$$
7	4 6	eqtr4i	$$⊢3-1=0+2$$
8	7	oveq2i	$$⊢\left(0\dots 3-1\right)=\left(0\dots 0+2\right)$$
9		0z	$$⊢0\in \mathbb{Z}$$
10		fztp	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
11		eqidd	$$⊢0\in \mathbb{Z}\to 0=0$$
12		0p1e1	$$⊢0+1=1$$
13	12	a1i	$$⊢0\in \mathbb{Z}\to 0+1=1$$
14	6	a1i	$$⊢0\in \mathbb{Z}\to 0+2=2$$
15	11 13 14	tpeq123d	$$⊢0\in \mathbb{Z}\to \left\{0,0+1,0+2\right\}=\left\{0,1,2\right\}$$
16	10 15	eqtrd	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+2\right)=\left\{0,1,2\right\}$$
17	9 16	ax-mp	$$⊢\left(0\dots 0+2\right)=\left\{0,1,2\right\}$$
18	3 8 17	3eqtri	$$⊢\left(0..^3\right)=\left\{0,1,2\right\}$$