Metamath Proof Explorer


Theorem fzo12sn

Description: A 1-based half-open integer interval up to, but not including, 2 is a singleton. (Contributed by Alexander van der Vekens, 31-Jan-2018)

Ref Expression
Assertion fzo12sn 1 ..^ 2 = 1

Proof

Step Hyp Ref Expression
1 df-2 2 = 1 + 1
2 1 oveq2i 1 ..^ 2 = 1 ..^ 1 + 1
3 1z 1
4 fzosn 1 1 ..^ 1 + 1 = 1
5 3 4 ax-mp 1 ..^ 1 + 1 = 1
6 2 5 eqtri 1 ..^ 2 = 1