Description: Membership of an integer greater than 2 decreased by 2 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ige3m2fz | |- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. ( 1 ... N ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3m1e2 | |- ( 3 - 1 ) = 2 |
|
| 2 | 1 | eqcomi | |- 2 = ( 3 - 1 ) |
| 3 | 2 | a1i | |- ( N e. ( ZZ>= ` 3 ) -> 2 = ( 3 - 1 ) ) |
| 4 | 3 | oveq2d | |- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) = ( N - ( 3 - 1 ) ) ) |
| 5 | 3nn | |- 3 e. NN |
|
| 6 | uzsubsubfz1 | |- ( ( 3 e. NN /\ N e. ( ZZ>= ` 3 ) ) -> ( N - ( 3 - 1 ) ) e. ( 1 ... N ) ) |
|
| 7 | 5 6 | mpan | |- ( N e. ( ZZ>= ` 3 ) -> ( N - ( 3 - 1 ) ) e. ( 1 ... N ) ) |
| 8 | 4 7 | eqeltrd | |- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. ( 1 ... N ) ) |