Metamath Proof Explorer


Theorem fzo0n0

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..^AA

Proof

Step Hyp Ref Expression
1 fzon0 0..^A00..^A
2 lbfzo0 00..^AA
3 1 2 bitri 0..^AA