This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzo0n

Description: A half-open range of nonnegative integers is empty iff the upper bound is not positive. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion fzo0n 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( 0 ..^ ( N - M ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 zre 
 |-  ( M e. ZZ -> M e. RR )
3 suble0 
 |-  ( ( N e. RR /\ M e. RR ) -> ( ( N - M ) <_ 0 <-> N <_ M ) )
4 1 2 3 syl2an 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N - M ) <_ 0 <-> N <_ M ) )
5 0z 
 |-  0 e. ZZ
6 zsubcl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
7 fzon 
 |-  ( ( 0 e. ZZ /\ ( N - M ) e. ZZ ) -> ( ( N - M ) <_ 0 <-> ( 0 ..^ ( N - M ) ) = (/) ) )
8 5 6 7 sylancr 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N - M ) <_ 0 <-> ( 0 ..^ ( N - M ) ) = (/) ) )
9 4 8 bitr3d 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N <_ M <-> ( 0 ..^ ( N - M ) ) = (/) ) )
10 9 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( 0 ..^ ( N - M ) ) = (/) ) )