Theorem nn0diffz0

Description: Upper set of the nonnegative integers. (Contributed by Thierry Arnoux, 25-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
3	2 1	eleqtrdi	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{Z}}_{\ge 0}$$
4		fzouzsplit	$$⊢N+1\in {\mathbb{Z}}_{\ge 0}\to {\mathbb{Z}}_{\ge 0}=\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
5	3 4	syl	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge 0}=\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
6	1 5	eqtrid	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{N}}_0=\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
7	6	difeq1d	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{N}}_0\setminus \left(0\dots N\right)=\left(\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}\right)\setminus \left(0\dots N\right)$$
8		uncom	$$⊢{\mathbb{Z}}_{\ge \left(N+1\right)}\cup \left(0\dots N\right)=\left(0\dots N\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
9		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
10		fzval3	$$⊢N\in \mathbb{Z}\to \left(0\dots N\right)=\left(0..^N+1\right)$$
11	9 10	syl	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N\right)=\left(0..^N+1\right)$$
12	11	uneq1d	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}=\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
13	8 12	eqtrid	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge \left(N+1\right)}\cup \left(0\dots N\right)=\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}$$
14	13	difeq1d	$$⊢N\in {\mathbb{N}}_0\to \left({\mathbb{Z}}_{\ge \left(N+1\right)}\cup \left(0\dots N\right)\right)\setminus \left(0\dots N\right)=\left(\left(0..^N+1\right)\cup {\mathbb{Z}}_{\ge \left(N+1\right)}\right)\setminus \left(0\dots N\right)$$
15	11	ineq2d	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge \left(N+1\right)}\cap \left(0\dots N\right)={\mathbb{Z}}_{\ge \left(N+1\right)}\cap \left(0..^N+1\right)$$
16		fzouzdisj	$$⊢\left(0..^N+1\right)\cap {\mathbb{Z}}_{\ge \left(N+1\right)}=\varnothing$$
17	16	ineqcomi	$$⊢{\mathbb{Z}}_{\ge \left(N+1\right)}\cap \left(0..^N+1\right)=\varnothing$$
18	15 17	eqtrdi	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge \left(N+1\right)}\cap \left(0\dots N\right)=\varnothing$$
19		undif5	$$⊢{\mathbb{Z}}_{\ge \left(N+1\right)}\cap \left(0\dots N\right)=\varnothing \to \left({\mathbb{Z}}_{\ge \left(N+1\right)}\cup \left(0\dots N\right)\right)\setminus \left(0\dots N\right)={\mathbb{Z}}_{\ge \left(N+1\right)}$$
20	18 19	syl	$$⊢N\in {\mathbb{N}}_0\to \left({\mathbb{Z}}_{\ge \left(N+1\right)}\cup \left(0\dots N\right)\right)\setminus \left(0\dots N\right)={\mathbb{Z}}_{\ge \left(N+1\right)}$$
21	7 14 20	3eqtr2d	$$⊢N\in {\mathbb{N}}_0\to {\mathbb{N}}_0\setminus \left(0\dots N\right)={\mathbb{Z}}_{\ge \left(N+1\right)}$$