Description: An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021) (Proof shortened by AV, 22-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | oddm1d2 | |- ( N e. ZZ -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. ZZ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oddp1d2 | |- ( N e. ZZ -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) ) |
|
| 2 | zob | |- ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N - 1 ) / 2 ) e. ZZ ) ) |
|
| 3 | 1 2 | bitrd | |- ( N e. ZZ -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. ZZ ) ) |