Metamath Proof Explorer

Theorem fzossnn

Description: Half-open integer ranges starting with 1 are subsets of NN. (Contributed by Thierry Arnoux, 28-Dec-2016)

Ref Expression
Assertion fzossnn 
|- ( 1 ..^ N ) C_ NN

Proof

Step Hyp Ref Expression
1 fzossfz 
 |-  ( 1 ..^ N ) C_ ( 1 ... N )
2 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
3 1 2 sstri 
 |-  ( 1 ..^ N ) C_ NN