Theorem fzonlt0

Description: A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018)

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

Proof

Step	Hyp	Ref	Expression
1		zre	|- ( N e. ZZ -> N e. RR )
2		zre	|- ( M e. ZZ -> M e. RR )
3		lenlt	|- ( ( N e. RR /\ M e. RR ) -> ( N <_ M <-> -. M < N ) )
4	1 2 3	syl2anr	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> -. M < N ) )
5		fzon	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )
6	4 5	bitr3d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -. M < N <-> ( M ..^ N ) = (/) ) )