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 }

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 }