Metamath Proof Explorer

Theorem elfzom1elp1fzo1

Description: Membership of a nonnegative integer incremented by one in a half-open range of positive integers. (Contributed by AV, 20-Mar-2021)

Ref Expression
Assertion elfzom1elp1fzo1 
|- ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ..^ N ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> I e. ZZ )
2 1 zcnd 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> I e. CC )
3 pncan1 
 |-  ( I e. CC -> ( ( I + 1 ) - 1 ) = I )
4 2 3 syl 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> ( ( I + 1 ) - 1 ) = I )
5 id 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> I e. ( 0 ..^ ( N - 1 ) ) )
6 4 5 eqeltrd 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> ( ( I + 1 ) - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
7 6 adantl 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( I + 1 ) - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
8 1 peano2zd 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> ( I + 1 ) e. ZZ )
9 8 anim1i 
 |-  ( ( I e. ( 0 ..^ ( N - 1 ) ) /\ N e. ZZ ) -> ( ( I + 1 ) e. ZZ /\ N e. ZZ ) )
10 9 ancoms 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( I + 1 ) e. ZZ /\ N e. ZZ ) )
11 elfzom1b 
 |-  ( ( ( I + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( I + 1 ) e. ( 1 ..^ N ) <-> ( ( I + 1 ) - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )
12 10 11 syl 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( I + 1 ) e. ( 1 ..^ N ) <-> ( ( I + 1 ) - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )
13 7 12 mpbird 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ..^ N ) )