Metamath Proof Explorer


Theorem ige3m2fz

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

Proof

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