Theorem 1elfz13

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

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

Proof

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