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

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		3nn	⊢ 3 ∈ ℕ
3		1le3	⊢ 1 ≤ 3
4		elfz1b	⊢ ( 1 ∈ ( 1 ... 3 ) ↔ ( 1 ∈ ℕ ∧ 3 ∈ ℕ ∧ 1 ≤ 3 ) )
5	1 2 3 4	mpbir3an	⊢ 1 ∈ ( 1 ... 3 )