Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 3z 
 |-  3 e. ZZ
3 2z 
 |-  2 e. ZZ
4 1 2 3 3pm3.2i 
 |-  ( 1 e. ZZ /\ 3 e. ZZ /\ 2 e. ZZ )
5 1le2 
 |-  1 <_ 2
6 2le3 
 |-  2 <_ 3
7 5 6 pm3.2i 
 |-  ( 1 <_ 2 /\ 2 <_ 3 )
8 elfz2 
 |-  ( 2 e. ( 1 ... 3 ) <-> ( ( 1 e. ZZ /\ 3 e. ZZ /\ 2 e. ZZ ) /\ ( 1 <_ 2 /\ 2 <_ 3 ) ) )
9 4 7 8 mpbir2an 
 |-  2 e. ( 1 ... 3 )