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 e. ( 1 ... 3 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn | |- 1 e. NN |
|
| 2 | 3nn | |- 3 e. NN |
|
| 3 | 1le3 | |- 1 <_ 3 |
|
| 4 | elfz1b | |- ( 1 e. ( 1 ... 3 ) <-> ( 1 e. NN /\ 3 e. NN /\ 1 <_ 3 ) ) |
|
| 5 | 1 2 3 4 | mpbir3an | |- 1 e. ( 1 ... 3 ) |