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 ) ∈ ℤ ) )