Theorem 2elfz13

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

	Ref	Expression
Assertion	2elfz13	⊢ 2 ∈ ( 1 ... 3 )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		3z	⊢ 3 ∈ ℤ
3		2z	⊢ 2 ∈ ℤ
4	1 2 3	3pm3.2i	⊢ ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ∈ ℤ )
5		1le2	⊢ 1 ≤ 2
6		2le3	⊢ 2 ≤ 3
7	5 6	pm3.2i	⊢ ( 1 ≤ 2 ∧ 2 ≤ 3 )
8		elfz2	⊢ ( 2 ∈ ( 1 ... 3 ) ↔ ( ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 1 ≤ 2 ∧ 2 ≤ 3 ) ) )
9	4 7 8	mpbir2an	⊢ 2 ∈ ( 1 ... 3 )