This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℤ_{\geq 3} \to N - 2 \in (1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		3m1e2	$⊢ 3 - 1 = 2$
2	1	eqcomi	$⊢ 2 = 3 - 1$
3	2	a1i	$⊢ N \in ℤ_{\geq 3} \to 2 = 3 - 1$
4	3	oveq2d	$⊢ N \in ℤ_{\geq 3} \to N - 2 = N - (3 - 1)$
5		3nn	$⊢ 3 \in ℕ$
6		uzsubsubfz1	$⊢ (3 \in ℕ \land N \in ℤ_{\geq 3}) \to N - (3 - 1) \in (1 \dots N)$
7	5 6	mpan	$⊢ N \in ℤ_{\geq 3} \to N - (3 - 1) \in (1 \dots N)$
8	4 7	eqeltrd	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in (1 \dots N)$