Description: 2 does not divide 1. That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018) (Proof shortened by Steven Nguyen, 3-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | n2dvds1 | |- -. 2 || 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | halfnz | |- -. ( 1 / 2 ) e. ZZ |
|
| 2 | 1z | |- 1 e. ZZ |
|
| 3 | evend2 | |- ( 1 e. ZZ -> ( 2 || 1 <-> ( 1 / 2 ) e. ZZ ) ) |
|
| 4 | 2 3 | ax-mp | |- ( 2 || 1 <-> ( 1 / 2 ) e. ZZ ) |
| 5 | 1 4 | mtbir | |- -. 2 || 1 |