Description: Increasing an element of a half-open range of nonnegative integers by 1 results in an element of the half-open range of nonnegative integers with an upper bound increased by 1. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Proof shortened by Thierry Arnoux, 14-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elfzom1p1elfzo | |- ( ( N e. NN /\ X e. ( 0 ..^ ( N - 1 ) ) ) -> ( X + 1 ) e. ( 0 ..^ N ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnz | |- ( N e. NN -> N e. ZZ ) |
|
| 2 | elfzom1elp1fzo | |- ( ( N e. ZZ /\ X e. ( 0 ..^ ( N - 1 ) ) ) -> ( X + 1 ) e. ( 0 ..^ N ) ) |
|
| 3 | 1 2 | sylan | |- ( ( N e. NN /\ X e. ( 0 ..^ ( N - 1 ) ) ) -> ( X + 1 ) e. ( 0 ..^ N ) ) |