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	$$⊢\left\{0,1\right\}\cap {\mathbb{Z}}_{\ge 2}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fzo0to2pr	$$⊢\left(0..^2\right)=\left\{0,1\right\}$$
2	1	ineq1i	$$⊢\left(0..^2\right)\cap {\mathbb{Z}}_{\ge 2}=\left\{0,1\right\}\cap {\mathbb{Z}}_{\ge 2}$$
3		fzouzdisj	$$⊢\left(0..^2\right)\cap {\mathbb{Z}}_{\ge 2}=\varnothing$$
4	2 3	eqtr3i	$$⊢\left\{0,1\right\}\cap {\mathbb{Z}}_{\ge 2}=\varnothing$$