Theorem uznnssnn

Description: The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013)

	Ref	Expression
Assertion	uznnssnn	$$⊢N\in \mathbb{N}\to {\mathbb{Z}}_{\ge N}\subseteq \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		elnnuz	$$⊢N\in \mathbb{N}\leftrightarrow N\in {\mathbb{Z}}_{\ge 1}$$
2		uzss	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge 1}$$
3	1 2	sylbi	$$⊢N\in \mathbb{N}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge 1}$$
4		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
5	3 4	sseqtrrdi	$$⊢N\in \mathbb{N}\to {\mathbb{Z}}_{\ge N}\subseteq \mathbb{N}$$