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

Metamath Proof Explorer

Theorem fz0

Description: A finite set of sequential integers is empty if its bounds are not integers. (Contributed by AV, 13-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( M e/ ZZ <-> -. M e. ZZ )
2 df-nel 
 |-  ( N e/ ZZ <-> -. N e. ZZ )
3 1 2 orbi12i 
 |-  ( ( M e/ ZZ \/ N e/ ZZ ) <-> ( -. M e. ZZ \/ -. N e. ZZ ) )
4 ianor 
 |-  ( -. ( M e. ZZ /\ N e. ZZ ) <-> ( -. M e. ZZ \/ -. N e. ZZ ) )
5 fzf 
 |-  ... : ( ZZ X. ZZ ) --> ~P ZZ
6 5 fdmi 
 |-  dom ... = ( ZZ X. ZZ )
7 6 ndmov 
 |-  ( -. ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = (/) )
8 4 7 sylbir 
 |-  ( ( -. M e. ZZ \/ -. N e. ZZ ) -> ( M ... N ) = (/) )
9 3 8 sylbi 
 |-  ( ( M e/ ZZ \/ N e/ ZZ ) -> ( M ... N ) = (/) )