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	⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ 𝑁 ) ⊆ ℕ )

Proof

Step	Hyp	Ref	Expression
1		elnnuz	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
2		uzss	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 1 ) )
3	1 2	sylbi	⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 1 ) )
4		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
5	3 4	sseqtrrdi	⊢ ( 𝑁 ∈ ℕ → ( ℤ≥ ‘ 𝑁 ) ⊆ ℕ )