Theorem fz01pr

Description: An integer range between 0 and 1 is a pair. (Contributed by AV, 11-Sep-2025)

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

Proof

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