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 \notin ℤ \lor N \notin ℤ) \to (M \dots N) = \emptyset$

Step	Hyp	Ref	Expression
1		df-nel	$⊢ M \notin ℤ \leftrightarrow \neg M \in ℤ$
2		df-nel	$⊢ N \notin ℤ \leftrightarrow \neg N \in ℤ$
3	1 2	orbi12i	$⊢ (M \notin ℤ \lor N \notin ℤ) \leftrightarrow (\neg M \in ℤ \lor \neg N \in ℤ)$
4		ianor	$⊢ \neg (M \in ℤ \land N \in ℤ) \leftrightarrow (\neg M \in ℤ \lor \neg N \in ℤ)$
5		fzf	$⊢ \dots : ℤ \times ℤ ⟶ 𝒫 ℤ$
6	5	fdmi	$⊢ dom \dots = ℤ \times ℤ$
7	6	ndmov	$⊢ \neg (M \in ℤ \land N \in ℤ) \to (M \dots N) = \emptyset$
8	4 7	sylbir	$⊢ (\neg M \in ℤ \lor \neg N \in ℤ) \to (M \dots N) = \emptyset$
9	3 8	sylbi	$⊢ (M \notin ℤ \lor N \notin ℤ) \to (M \dots N) = \emptyset$

Metamath Proof Explorer