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	$$⊢\left(M\notin \mathbb{Z}\vee N\notin \mathbb{Z}\right)\to \left(M\dots N\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢M\notin \mathbb{Z}\leftrightarrow \neg M\in \mathbb{Z}$$
2		df-nel	$$⊢N\notin \mathbb{Z}\leftrightarrow \neg N\in \mathbb{Z}$$
3	1 2	orbi12i	$$⊢\left(M\notin \mathbb{Z}\vee N\notin \mathbb{Z}\right)\leftrightarrow \left(\neg M\in \mathbb{Z}\vee \neg N\in \mathbb{Z}\right)$$
4		ianor	$$⊢\neg \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\leftrightarrow \left(\neg M\in \mathbb{Z}\vee \neg N\in \mathbb{Z}\right)$$
5		fzf	$$⊢\dots :\mathbb{Z}\times \mathbb{Z}⟶𝒫\mathbb{Z}$$
6	5	fdmi	$$⊢\mathrm{dom}\dots =\mathbb{Z}\times \mathbb{Z}$$
7	6	ndmov	$$⊢\neg \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M\dots N\right)=\varnothing$$
8	4 7	sylbir	$$⊢\left(\neg M\in \mathbb{Z}\vee \neg N\in \mathbb{Z}\right)\to \left(M\dots N\right)=\varnothing$$
9	3 8	sylbi	$$⊢\left(M\notin \mathbb{Z}\vee N\notin \mathbb{Z}\right)\to \left(M\dots N\right)=\varnothing$$