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 ) ) |