Metamath Proof Explorer

Theorem fzo0ss1

Description: Subset relationship for half-open integer ranges with lower bounds 0 and 1. (Contributed by Alexander van der Vekens, 18-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
2 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ N ) C_ ( 0 ..^ N ) )
3 1 2 ax-mp 
 |-  ( 1 ..^ N ) C_ ( 0 ..^ N )