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 )