Metamath Proof Explorer

Theorem fzossrbm1

Description: Subset of a half-open range. (Contributed by Alexander van der Vekens, 1-Nov-2017)

Ref Expression
Assertion fzossrbm1 
|- ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
2 id 
 |-  ( N e. ZZ -> N e. ZZ )
3 zre 
 |-  ( N e. ZZ -> N e. RR )
4 3 lem1d 
 |-  ( N e. ZZ -> ( N - 1 ) <_ N )
5 eluz2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) <-> ( ( N - 1 ) e. ZZ /\ N e. ZZ /\ ( N - 1 ) <_ N ) )
6 1 2 4 5 syl3anbrc 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` ( N - 1 ) ) )
7 fzoss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
8 6 7 syl 
 |-  ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )