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 }

Proof

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