Theorem nn0split01

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

	Ref	Expression
Assertion	nn0split01	$$⊢{\mathbb{N}}_0=\left\{0,1\right\}\cup {\mathbb{Z}}_{\ge 2}$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		2eluzge0	$$⊢2\in {\mathbb{Z}}_{\ge 0}$$
3		fzouzsplit	$$⊢2\in {\mathbb{Z}}_{\ge 0}\to {\mathbb{Z}}_{\ge 0}=\left(0..^2\right)\cup {\mathbb{Z}}_{\ge 2}$$
4	2 3	ax-mp	$$⊢{\mathbb{Z}}_{\ge 0}=\left(0..^2\right)\cup {\mathbb{Z}}_{\ge 2}$$
5		fzo0to2pr	$$⊢\left(0..^2\right)=\left\{0,1\right\}$$
6	5	uneq1i	$$⊢\left(0..^2\right)\cup {\mathbb{Z}}_{\ge 2}=\left\{0,1\right\}\cup {\mathbb{Z}}_{\ge 2}$$
7	1 4 6	3eqtri	$$⊢{\mathbb{N}}_0=\left\{0,1\right\}\cup {\mathbb{Z}}_{\ge 2}$$