Metamath Proof Explorer

Theorem oddp1d2

Description: An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo and zeo2 . (Contributed by AV, 22-Jun-2021)

Ref Expression
Assertion oddp1d2 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 oddp1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N + 1
2 2z ⊢ 2 ∈ ℤ
3 2ne0 ⊢ 2 ≠ 0
4 peano2z ⊢ N ∈ ℤ → N + 1 ∈ ℤ
5 dvdsval2 ⊢ 2 ∈ ℤ ∧ 2 ≠ 0 ∧ N + 1 ∈ ℤ → 2 ∥ N + 1 ↔ N + 1 2 ∈ ℤ
6 2 3 4 5 mp3an12i ⊢ N ∈ ℤ → 2 ∥ N + 1 ↔ N + 1 2 ∈ ℤ
7 1 6 bitrd ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ