Theorem 1elfz13

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

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

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		3z	$$⊢3\in \mathbb{Z}$$
3		1le3	$$⊢1\le 3$$
4		eluz2	$$⊢3\in {\mathbb{Z}}_{\ge 1}\leftrightarrow \left(1\in \mathbb{Z}\wedge 3\in \mathbb{Z}\wedge 1\le 3\right)$$
5	1 2 3 4	mpbir3an	$$⊢3\in {\mathbb{Z}}_{\ge 1}$$
6		eluzfz1	$$⊢3\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots 3\right)$$
7	5 6	ax-mp	$$⊢1\in \left(1\dots 3\right)$$