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 00..^0+1=0
5 3 4 ax-mp 0..^0+1=0
6 2 5 eqtri 0..^1=0