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

Proof

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