Metamath Proof Explorer

Theorem elfzom1elp1fzo

Description: Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Proof shortened by AV, 5-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 elfzofz 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> I e. ( 0 ... ( N - 1 ) ) )
2 elfzuz2 
 |-  ( I e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
3 elnn0uz 
 |-  ( ( N - 1 ) e. NN0 <-> ( N - 1 ) e. ( ZZ>= ` 0 ) )
4 zcn 
 |-  ( N e. ZZ -> N e. CC )
5 4 anim1i 
 |-  ( ( N e. ZZ /\ ( N - 1 ) e. NN0 ) -> ( N e. CC /\ ( N - 1 ) e. NN0 ) )
6 elnnnn0 
 |-  ( N e. NN <-> ( N e. CC /\ ( N - 1 ) e. NN0 ) )
7 5 6 sylibr 
 |-  ( ( N e. ZZ /\ ( N - 1 ) e. NN0 ) -> N e. NN )
8 7 expcom 
 |-  ( ( N - 1 ) e. NN0 -> ( N e. ZZ -> N e. NN ) )
9 3 8 sylbir 
 |-  ( ( N - 1 ) e. ( ZZ>= ` 0 ) -> ( N e. ZZ -> N e. NN ) )
10 1 2 9 3syl 
 |-  ( I e. ( 0 ..^ ( N - 1 ) ) -> ( N e. ZZ -> N e. NN ) )
11 10 impcom 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> N e. NN )
12 1nn0 
 |-  1 e. NN0
13 12 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
14 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
15 nnge1 
 |-  ( N e. NN -> 1 <_ N )
16 13 14 15 3jca 
 |-  ( N e. NN -> ( 1 e. NN0 /\ N e. NN0 /\ 1 <_ N ) )
17 11 16 syl 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( 1 e. NN0 /\ N e. NN0 /\ 1 <_ N ) )
18 elfz2nn0 
 |-  ( 1 e. ( 0 ... N ) <-> ( 1 e. NN0 /\ N e. NN0 /\ 1 <_ N ) )
19 17 18 sylibr 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> 1 e. ( 0 ... N ) )
20 fzossrbm1 
 |-  ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
21 20 adantr 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
22 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
23 21 22 sstrdi 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ... N ) )
24 simpr 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> I e. ( 0 ..^ ( N - 1 ) ) )
25 23 24 jca 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( ( 0 ..^ ( N - 1 ) ) C_ ( 0 ... N ) /\ I e. ( 0 ..^ ( N - 1 ) ) ) )
26 ssel2 
 |-  ( ( ( 0 ..^ ( N - 1 ) ) C_ ( 0 ... N ) /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> I e. ( 0 ... N ) )
27 elfzubelfz 
 |-  ( I e. ( 0 ... N ) -> N e. ( 0 ... N ) )
28 25 26 27 3syl 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> N e. ( 0 ... N ) )
29 19 28 jca 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( 1 e. ( 0 ... N ) /\ N e. ( 0 ... N ) ) )
30 elfzodifsumelfzo 
 |-  ( ( 1 e. ( 0 ... N ) /\ N e. ( 0 ... N ) ) -> ( I e. ( 0 ..^ ( N - 1 ) ) -> ( I + 1 ) e. ( 0 ..^ N ) ) )
31 29 24 30 sylc 
 |-  ( ( N e. ZZ /\ I e. ( 0 ..^ ( N - 1 ) ) ) -> ( I + 1 ) e. ( 0 ..^ N ) )