Metamath Proof Explorer

Theorem oddm1d2

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 ∈ ℤ → ¬ 2 ∥ N ↔ N − 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 oddp1d2 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ
2 zob ⊢ N ∈ ℤ → N + 1 2 ∈ ℤ ↔ N − 1 2 ∈ ℤ
3 1 2 bitrd ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N − 1 2 ∈ ℤ