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

Proof

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