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 ) ) = (/) ) )