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 } i^i ( ZZ>= ` 2 ) ) = (/)

Proof

Step Hyp Ref Expression
1 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
2 1 ineq1i 
 |-  ( ( 0 ..^ 2 ) i^i ( ZZ>= ` 2 ) ) = ( { 0 , 1 } i^i ( ZZ>= ` 2 ) )
3 fzouzdisj 
 |-  ( ( 0 ..^ 2 ) i^i ( ZZ>= ` 2 ) ) = (/)
4 2 3 eqtr3i 
 |-  ( { 0 , 1 } i^i ( ZZ>= ` 2 ) ) = (/)