Theorem fzo0to2pr

Description: A half-open integer range from 0 to 2 is an unordered pair. (Contributed by Alexander van der Vekens, 4-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		fzoval	$$⊢2\in \mathbb{Z}\to \left(0..^2\right)=\left(0\dots 2-1\right)$$
3	1 2	ax-mp	$$⊢\left(0..^2\right)=\left(0\dots 2-1\right)$$
4		2m1e1	$$⊢2-1=1$$
5		0p1e1	$$⊢0+1=1$$
6	4 5	eqtr4i	$$⊢2-1=0+1$$
7	6	oveq2i	$$⊢\left(0\dots 2-1\right)=\left(0\dots 0+1\right)$$
8		0z	$$⊢0\in \mathbb{Z}$$
9		fzpr	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+1\right)=\left\{0,0+1\right\}$$
10	5	preq2i	$$⊢\left\{0,0+1\right\}=\left\{0,1\right\}$$
11	9 10	syl6eq	$$⊢0\in \mathbb{Z}\to \left(0\dots 0+1\right)=\left\{0,1\right\}$$
12	8 11	ax-mp	$$⊢\left(0\dots 0+1\right)=\left\{0,1\right\}$$
13	3 7 12	3eqtri	$$⊢\left(0..^2\right)=\left\{0,1\right\}$$