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

Proof

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