Theorem ige2m1fz1

Description: Membership of an integer greater than 1 decreased by 1 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018)

	Ref	Expression
Assertion	ige2m1fz1	|- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. ( 1 ... N ) )

Proof

Step	Hyp	Ref	Expression
1		1e2m1	|- 1 = ( 2 - 1 )
2	1	a1i	|- ( N e. ( ZZ>= ` 2 ) -> 1 = ( 2 - 1 ) )
3	2	oveq2d	|- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) = ( N - ( 2 - 1 ) ) )
4		2nn	|- 2 e. NN
5		uzsubsubfz1	|- ( ( 2 e. NN /\ N e. ( ZZ>= ` 2 ) ) -> ( N - ( 2 - 1 ) ) e. ( 1 ... N ) )
6	4 5	mpan	|- ( N e. ( ZZ>= ` 2 ) -> ( N - ( 2 - 1 ) ) e. ( 1 ... N ) )
7	3 6	eqeltrd	|- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. ( 1 ... N ) )