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 ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )

Proof

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