Theorem fz0tp

Description: An integer range from 0 to 2 is an unordered triple. (Contributed by Alexander van der Vekens, 1-Feb-2018)

	Ref	Expression
Assertion	fz0tp	$$⊢\left(0\dots 2\right)=\left\{0,1,2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2	1	addid2i	$$⊢0+2=2$$
3	2	eqcomi	$$⊢2=0+2$$
4	3	oveq2i	$$⊢\left(0\dots 2\right)=\left(0\dots 0+2\right)$$
5		0z	$$⊢0\in \mathbb{Z}$$
6		fztp	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
7	5 6	ax-mp	$$⊢\left(0\dots 0+2\right)=\left\{0,0+1,0+2\right\}$$
8		eqid	$$⊢0=0$$
9		id	$$⊢0=0\to 0=0$$
10		0p1e1	$$⊢0+1=1$$
11	10	a1i	$$⊢0=0\to 0+1=1$$
12	2	a1i	$$⊢0=0\to 0+2=2$$
13	9 11 12	tpeq123d	$$⊢0=0\to \left\{0,0+1,0+2\right\}=\left\{0,1,2\right\}$$
14	8 13	ax-mp	$$⊢\left\{0,0+1,0+2\right\}=\left\{0,1,2\right\}$$
15	4 7 14	3eqtri	$$⊢\left(0\dots 2\right)=\left\{0,1,2\right\}$$