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 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 | |- 2 = ( 1 + 1 ) |
|
2 | 1 | oveq2i | |- ( 1 ..^ 2 ) = ( 1 ..^ ( 1 + 1 ) ) |
3 | 1z | |- 1 e. ZZ |
|
4 | fzosn | |- ( 1 e. ZZ -> ( 1 ..^ ( 1 + 1 ) ) = { 1 } ) |
|
5 | 3 4 | ax-mp | |- ( 1 ..^ ( 1 + 1 ) ) = { 1 } |
6 | 2 5 | eqtri | |- ( 1 ..^ 2 ) = { 1 } |