Theorem nnuz

Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005)

	Ref	Expression
Assertion	nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$

Proof

Step	Hyp	Ref	Expression
1		nnzrab	$$⊢\mathbb{N}=\left\{k\in \mathbb{Z}|1\le k\right\}$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		uzval	$$⊢1\in \mathbb{Z}\to {\mathbb{Z}}_{\ge 1}=\left\{k\in \mathbb{Z}|1\le k\right\}$$
4	2 3	ax-mp	$$⊢{\mathbb{Z}}_{\ge 1}=\left\{k\in \mathbb{Z}|1\le k\right\}$$
5	1 4	eqtr4i	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$