Description: A half-open integer range based at 0 is nonempty precisely if the upper bound is a positive integer. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fzo0n0 | |- ( ( 0 ..^ A ) =/= (/) <-> A e. NN ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fzon0 | |- ( ( 0 ..^ A ) =/= (/) <-> 0 e. ( 0 ..^ A ) ) |
|
| 2 | lbfzo0 | |- ( 0 e. ( 0 ..^ A ) <-> A e. NN ) |
|
| 3 | 1 2 | bitri | |- ( ( 0 ..^ A ) =/= (/) <-> A e. NN ) |