Theorem nn0split01

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

	Ref	Expression
Assertion	nn0split01	⊢ ℕ0 = ( { 0 , 1 } ∪ ( ℤ≥ ‘ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2		2eluzge0	⊢ 2 ∈ ( ℤ≥ ‘ 0 )
3		fzouzsplit	⊢ ( 2 ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ 2 ) ∪ ( ℤ≥ ‘ 2 ) ) )
4	2 3	ax-mp	⊢ ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ 2 ) ∪ ( ℤ≥ ‘ 2 ) )
5		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
6	5	uneq1i	⊢ ( ( 0 ..^ 2 ) ∪ ( ℤ≥ ‘ 2 ) ) = ( { 0 , 1 } ∪ ( ℤ≥ ‘ 2 ) )
7	1 4 6	3eqtri	⊢ ℕ0 = ( { 0 , 1 } ∪ ( ℤ≥ ‘ 2 ) )