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 ∈ ( 1 ... 3 )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		3z	⊢ 3 ∈ ℤ
3		1le3	⊢ 1 ≤ 3
4		eluz2	⊢ ( 3 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 1 ≤ 3 ) )
5	1 2 3 4	mpbir3an	⊢ 3 ∈ ( ℤ≥ ‘ 1 )
6		eluzfz1	⊢ ( 3 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 3 ) )
7	5 6	ax-mp	⊢ 1 ∈ ( 1 ... 3 )