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 } ∩ ( ℤ≥ ‘ 2 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
2	1	ineq1i	⊢ ( ( 0 ..^ 2 ) ∩ ( ℤ≥ ‘ 2 ) ) = ( { 0 , 1 } ∩ ( ℤ≥ ‘ 2 ) )
3		fzouzdisj	⊢ ( ( 0 ..^ 2 ) ∩ ( ℤ≥ ‘ 2 ) ) = ∅
4	2 3	eqtr3i	⊢ ( { 0 , 1 } ∩ ( ℤ≥ ‘ 2 ) ) = ∅