Metamath Proof Explorer

Theorem fzon

Description: A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
2 fzn 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( ( N - 1 ) < M <-> ( M ... ( N - 1 ) ) = (/) ) )
3 1 2 sylan2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( N - 1 ) < M <-> ( M ... ( N - 1 ) ) = (/) ) )
4 zlem1lt 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N <_ M <-> ( N - 1 ) < M ) )
5 4 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( N - 1 ) < M ) )
6 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
7 6 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
8 7 eqeq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M ..^ N ) = (/) <-> ( M ... ( N - 1 ) ) = (/) ) )
9 3 5 8 3bitr4d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N <_ M <-> ( M ..^ N ) = (/) ) )