Theorem fz12pr

Description: An integer range between 1 and 2 is a pair. (Contributed by AV, 11-Jan-2023)

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

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	oveq2i	$$⊢\left(1\dots 2\right)=\left(1\dots 1+1\right)$$
3		1z	$$⊢1\in \mathbb{Z}$$
4		fzpr	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+1\right)=\left\{1,1+1\right\}$$
5	3 4	ax-mp	$$⊢\left(1\dots 1+1\right)=\left\{1,1+1\right\}$$
6		1p1e2	$$⊢1+1=2$$
7	6	preq2i	$$⊢\left\{1,1+1\right\}=\left\{1,2\right\}$$
8	2 5 7	3eqtri	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$