Theorem 2elfz13

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

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

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		3nn	$$⊢3\in \mathbb{N}$$
3		2le3	$$⊢2\le 3$$
4		elfz1b	$$⊢2\in \left(1\dots 3\right)\leftrightarrow \left(2\in \mathbb{N}\wedge 3\in \mathbb{N}\wedge 2\le 3\right)$$
5	1 2 3 4	mpbir3an	$$⊢2\in \left(1\dots 3\right)$$