2elfz13

Description: Membership of 2 in the integer interval ( 1 ... 3 ). (Suggested by tirix.) (Contributed by Jiamin Zhao, 1-Aug-2026)

		Ref	Expression
	Assertion	2elfz13	$⊢ 2 \in (1 \dots 3)$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		3z	$⊢ 3 \in ℤ$
3		2z	$⊢ 2 \in ℤ$
4	1 2 3	3pm3.2i	$⊢ (1 \in ℤ \land 3 \in ℤ \land 2 \in ℤ)$
5		1le2	$⊢ 1 \leq 2$
6		2le3	$⊢ 2 \leq 3$
7	5 6	pm3.2i	$⊢ (1 \leq 2 \land 2 \leq 3)$
8		elfz2	$⊢ 2 \in (1 \dots 3) \leftrightarrow ((1 \in ℤ \land 3 \in ℤ \land 2 \in ℤ) \land (1 \leq 2 \land 2 \leq 3))$
9	4 7 8	mpbir2an	$⊢ 2 \in (1 \dots 3)$

Metamath Proof Explorer