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

Metamath Proof Explorer

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