Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 3z 
 |-  3 e. ZZ
3 1le3 
 |-  1 <_ 3
4 eluz2 
 |-  ( 3 e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ 3 e. ZZ /\ 1 <_ 3 ) )
5 1 2 3 4 mpbir3an 
 |-  3 e. ( ZZ>= ` 1 )
6 eluzfz1 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... 3 ) )
7 5 6 ax-mp 
 |-  1 e. ( 1 ... 3 )