Metamath Proof Explorer

Theorem elfzp1b

Description: An integer is a member of a 0-based finite set of sequential integers iff its successor is a member of the corresponding 1-based set. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion elfzp1b 
|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 0 ... ( N - 1 ) ) <-> ( K + 1 ) e. ( 1 ... N ) ) )

Proof

Step Hyp Ref Expression
1 peano2z 
 |-  ( K e. ZZ -> ( K + 1 ) e. ZZ )
2 1z 
 |-  1 e. ZZ
3 fzsubel 
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ ( ( K + 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
4 2 3 mpanl1 
 |-  ( ( N e. ZZ /\ ( ( K + 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
5 2 4 mpanr2 
 |-  ( ( N e. ZZ /\ ( K + 1 ) e. ZZ ) -> ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
6 1 5 sylan2 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
7 6 ancoms 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) )
8 zcn 
 |-  ( K e. ZZ -> K e. CC )
9 ax-1cn 
 |-  1 e. CC
10 pncan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K + 1 ) - 1 ) = K )
11 8 9 10 sylancl 
 |-  ( K e. ZZ -> ( ( K + 1 ) - 1 ) = K )
12 1m1e0 
 |-  ( 1 - 1 ) = 0
13 12 oveq1i 
 |-  ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) )
14 13 a1i 
 |-  ( K e. ZZ -> ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) ) )
15 11 14 eleq12d 
 |-  ( K e. ZZ -> ( ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) <-> K e. ( 0 ... ( N - 1 ) ) ) )
16 15 adantr 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( ( ( K + 1 ) - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) <-> K e. ( 0 ... ( N - 1 ) ) ) )
17 7 16 bitr2d 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K e. ( 0 ... ( N - 1 ) ) <-> ( K + 1 ) e. ( 1 ... N ) ) )