Metamath Proof Explorer


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 NN

Proof

Step Hyp Ref Expression
1 elnnuz NN1
2 uzss N1N1
3 1 2 sylbi NN1
4 nnuz =1
5 3 4 sseqtrrdi NN