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