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

Metamath Proof Explorer

Theorem nn0disj01

Description: The pair { 0 , 1 } does not overlap the rest of the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025)

		Ref	Expression
	Assertion	nn0disj01	$⊢ \{0, 1\} \cap ℤ_{\geq 2} = \emptyset$

Step	Hyp	Ref	Expression
1		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
2	1	ineq1i	$⊢ (0 ..^2) \cap ℤ_{\geq 2} = \{0, 1\} \cap ℤ_{\geq 2}$
3		fzouzdisj	$⊢ (0 ..^2) \cap ℤ_{\geq 2} = \emptyset$
4	2 3	eqtr3i	$⊢ \{0, 1\} \cap ℤ_{\geq 2} = \emptyset$