Metamath Proof Explorer

Theorem nn0split01

Description: Split 0 and 1 from the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Assertion nn0split01 
|- NN0 = ( { 0 , 1 } u. ( ZZ>= ` 2 ) )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 2eluzge0 
 |-  2 e. ( ZZ>= ` 0 )
3 fzouzsplit 
 |-  ( 2 e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ 2 ) u. ( ZZ>= ` 2 ) ) )
4 2 3 ax-mp 
 |-  ( ZZ>= ` 0 ) = ( ( 0 ..^ 2 ) u. ( ZZ>= ` 2 ) )
5 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
6 5 uneq1i 
 |-  ( ( 0 ..^ 2 ) u. ( ZZ>= ` 2 ) ) = ( { 0 , 1 } u. ( ZZ>= ` 2 ) )
7 1 4 6 3eqtri 
 |-  NN0 = ( { 0 , 1 } u. ( ZZ>= ` 2 ) )