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