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	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in (0 ..^N - 1)$

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℤ$
2		1z	$⊢ 1 \in ℤ$
3	1 2	jctir	$⊢ N \in ℤ_{\geq 2} \to (2 \in ℤ \land 1 \in ℤ)$
4		1lt2	$⊢ 1 < 2$
5	4	jctr	$⊢ N \in ℤ_{\geq 2} \to (N \in ℤ_{\geq 2} \land 1 < 2)$
6		eluzgtdifelfzo	$⊢ (2 \in ℤ \land 1 \in ℤ) \to ((N \in ℤ_{\geq 2} \land 1 < 2) \to N - 2 \in (0 ..^N - 1))$
7	3 5 6	sylc	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in (0 ..^N - 1)$

Metamath Proof Explorer

Theorem ige2m2fzo

Proof