Description: Membership of an integer greater than 1 decreased by 2 in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 3-Oct-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ige2m2fzo | |- ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eluzel2 | |- ( N e. ( ZZ>= ` 2 ) -> 2 e. ZZ ) |
|
| 2 | 1z | |- 1 e. ZZ |
|
| 3 | 1 2 | jctir | |- ( N e. ( ZZ>= ` 2 ) -> ( 2 e. ZZ /\ 1 e. ZZ ) ) |
| 4 | 1lt2 | |- 1 < 2 |
|
| 5 | 4 | jctr | |- ( N e. ( ZZ>= ` 2 ) -> ( N e. ( ZZ>= ` 2 ) /\ 1 < 2 ) ) |
| 6 | eluzgtdifelfzo | |- ( ( 2 e. ZZ /\ 1 e. ZZ ) -> ( ( N e. ( ZZ>= ` 2 ) /\ 1 < 2 ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) ) ) |
|
| 7 | 3 5 6 | sylc | |- ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. ( 0 ..^ ( N - 1 ) ) ) |