Theorem fzo13pr

Description: A 1-based half-open integer interval up to, but not including, 3 is a pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

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

Proof

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