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\in {\mathbb{Z}}_{\ge 2}\to N-1\in \left(1\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		1e2m1	$$⊢1=2-1$$
2	1	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1=2-1$$
3	2	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1=N-\left(2-1\right)$$
4		2nn	$$⊢2\in \mathbb{N}$$
5		uzsubsubfz1	$$⊢\left(2\in \mathbb{N}\wedge N\in {\mathbb{Z}}_{\ge 2}\right)\to N-\left(2-1\right)\in \left(1\dots N\right)$$
6	4 5	mpan	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-\left(2-1\right)\in \left(1\dots N\right)$$
7	3 6	eqeltrd	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in \left(1\dots N\right)$$