Metamath Proof Explorer

Theorem fz01en

Description: 0-based and 1-based finite sets of sequential integers are equinumerous. (Contributed by Paul Chapman, 11-Apr-2009)

Ref Expression
Assertion fz01en 
|- ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
2 0z 
 |-  0 e. ZZ
3 1z 
 |-  1 e. ZZ
4 fzen 
 |-  ( ( 0 e. ZZ /\ ( N - 1 ) e. ZZ /\ 1 e. ZZ ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) )
5 2 3 4 mp3an13 
 |-  ( ( N - 1 ) e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) )
6 1 5 syl 
 |-  ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) )
7 0p1e1 
 |-  ( 0 + 1 ) = 1
8 7 a1i 
 |-  ( N e. ZZ -> ( 0 + 1 ) = 1 )
9 zcn 
 |-  ( N e. ZZ -> N e. CC )
10 ax-1cn 
 |-  1 e. CC
11 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
12 9 10 11 sylancl 
 |-  ( N e. ZZ -> ( ( N - 1 ) + 1 ) = N )
13 8 12 oveq12d 
 |-  ( N e. ZZ -> ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
14 6 13 breqtrd 
 |-  ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )