Theorem nnsplit

Description: Express the set of positive integers as the disjoint (see nnuzdisj ) union of the first N values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

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