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 e. ZZ
4 fzosn 
 |-  ( 0 e. ZZ -> ( 0 ..^ ( 0 + 1 ) ) = { 0 } )
5 3 4 ax-mp 
 |-  ( 0 ..^ ( 0 + 1 ) ) = { 0 }
6 2 5 eqtri 
 |-  ( 0 ..^ 1 ) = { 0 }