Theorem nn0split

Description: Express the set of nonnegative integers as the disjoint (see nn0disj ) union of the first N + 1 values and the rest. (Contributed by AV, 8-Nov-2019)

	Ref	Expression
Assertion	nn0split	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{N}}_0=\left(0\dots N\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2	1	a1i	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
4	3 1	eleqtrdi	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{Z}}_{\ge 0}$$
5		uzsplit	$$⊢N+1\in {\mathbb{Z}}_{\ge 0}\to {\mathbb{Z}}_{\ge 0}=\left(0\dots N+1-1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
6	4 5	syl	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge 0}=\left(0\dots N+1-1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
7		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
8		pncan1	$$⊢N\in ℂ\to N+1-1=N$$
9	7 8	syl	$$⊢N\in {\mathbb{N}}_0\to N+1-1=N$$
10	9	oveq2d	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N+1-1\right)=\left(0\dots N\right)$$
11	10	uneq1d	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N+1-1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}=\left(0\dots N\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
12	2 6 11	3eqtrd	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{N}}_0=\left(0\dots N\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$