Theorem ige2m2fzo

Description: Membership of an integer greater than 1 decreased by 2 in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 3-Oct-2018)

	Ref	Expression
Assertion	ige2m2fzo	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℤ )
2		1z	⊢ 1 ∈ ℤ
3	1 2	jctir	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ∈ ℤ ∧ 1 ∈ ℤ ) )
4		1lt2	⊢ 1 < 2
5	4	jctr	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 < 2 ) )
6		eluzgtdifelfzo	⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 < 2 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
7	3 5 6	sylc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )