This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (0 ..^1) = \{0\}$

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