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	⊢ ( ( 𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ ) → ( 𝑀 ... 𝑁 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝑀 ∉ ℤ ↔ ¬ 𝑀 ∈ ℤ )
2		df-nel	⊢ ( 𝑁 ∉ ℤ ↔ ¬ 𝑁 ∈ ℤ )
3	1 2	orbi12i	⊢ ( ( 𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ ) ↔ ( ¬ 𝑀 ∈ ℤ ∨ ¬ 𝑁 ∈ ℤ ) )
4		ianor	⊢ ( ¬ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( ¬ 𝑀 ∈ ℤ ∨ ¬ 𝑁 ∈ ℤ ) )
5		fzf	⊢ ... : ( ℤ × ℤ ) ⟶ 𝒫 ℤ
6	5	fdmi	⊢ dom ... = ( ℤ × ℤ )
7	6	ndmov	⊢ ( ¬ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ∅ )
8	4 7	sylbir	⊢ ( ( ¬ 𝑀 ∈ ℤ ∨ ¬ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ∅ )
9	3 8	sylbi	⊢ ( ( 𝑀 ∉ ℤ ∨ 𝑁 ∉ ℤ ) → ( 𝑀 ... 𝑁 ) = ∅ )