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 
|- ( N e. NN -> ( ZZ>= ` N ) C_ NN )

Proof

Step Hyp Ref Expression
1 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
2 uzss 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` 1 ) )
3 1 2 sylbi 
 |-  ( N e. NN -> ( ZZ>= ` N ) C_ ( ZZ>= ` 1 ) )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 3 4 sseqtrrdi 
 |-  ( N e. NN -> ( ZZ>= ` N ) C_ NN )