Theorem fzo01

Description: Expressing the singleton of 0 as a half-open integer range. (Contributed by Stefan O'Rear, 15-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		1e0p1	$$⊢1=0+1$$
2	1	oveq2i	$$⊢\left(0..^1\right)=\left(0..^0+1\right)$$
3		0z	$$⊢0\in \mathbb{Z}$$
4		fzosn	$$⊢0\in \mathbb{Z}\to \left(0..^0+1\right)=\left\{0\right\}$$
5	3 4	ax-mp	$$⊢\left(0..^0+1\right)=\left\{0\right\}$$
6	2 5	eqtri	$$⊢\left(0..^1\right)=\left\{0\right\}$$