Theorem fzn

Description: A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005)

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

Proof

Step	Hyp	Ref	Expression
1		fzn0	|- ( ( M ... N ) =/= (/) <-> N e. ( ZZ>= ` M ) )
2		eluz	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )
3	1 2	bitrid	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M ... N ) =/= (/) <-> M <_ N ) )
4		zre	|- ( M e. ZZ -> M e. RR )
5		zre	|- ( N e. ZZ -> N e. RR )
6		lenlt	|- ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> -. N < M ) )
7	4 5 6	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> -. N < M ) )
8	3 7	bitr2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -. N < M <-> ( M ... N ) =/= (/) ) )
9	8	necon4bbid	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( N < M <-> ( M ... N ) = (/) ) )