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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		3m1e2	⊢ ( 3 − 1 ) = 2
2	1	eqcomi	⊢ 2 = ( 3 − 1 )
3	2	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 = ( 3 − 1 ) )
4	3	oveq2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) = ( 𝑁 − ( 3 − 1 ) ) )
5		3nn	⊢ 3 ∈ ℕ
6		uzsubsubfz1	⊢ ( ( 3 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − ( 3 − 1 ) ) ∈ ( 1 ... 𝑁 ) )
7	5 6	mpan	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − ( 3 − 1 ) ) ∈ ( 1 ... 𝑁 ) )
8	4 7	eqeltrd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) )