Metamath Proof Explorer

Theorem ige2m1fz

Description: Membership in a 0-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 18-Jun-2018) (Proof shortened by Alexander van der Vekens, 15-Sep-2018)

Ref Expression
Assertion ige2m1fz 
|- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. ( 0 ... N ) )

Proof

Step Hyp Ref Expression
1 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
2 fzss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... N ) C_ ( 0 ... N ) )
3 1 2 ax-mp 
 |-  ( 1 ... N ) C_ ( 0 ... N )
4 2z 
 |-  2 e. ZZ
5 4 a1i 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> 2 e. ZZ )
6 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
7 6 adantr 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> N e. ZZ )
8 simpr 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> 2 <_ N )
9 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
10 5 7 8 9 syl3anbrc 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> N e. ( ZZ>= ` 2 ) )
11 ige2m1fz1 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. ( 1 ... N ) )
12 10 11 syl 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. ( 1 ... N ) )
13 3 12 sselid 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. ( 0 ... N ) )