Metamath Proof Explorer

Theorem fz1ssfz0

Description: Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion fz1ssfz0 
|- ( 1 ... N ) C_ ( 0 ... N )

Proof

Step Hyp Ref Expression
1 1e0p1 
 |-  1 = ( 0 + 1 )
2 1 oveq1i 
 |-  ( 1 ... N ) = ( ( 0 + 1 ) ... N )
3 0z 
 |-  0 e. ZZ
4 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... N ) C_ ( 0 ... N ) )
5 3 4 ax-mp 
 |-  ( ( 0 + 1 ) ... N ) C_ ( 0 ... N )
6 2 5 eqsstri 
 |-  ( 1 ... N ) C_ ( 0 ... N )