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

Proof

Step	Hyp	Ref	Expression
1		oddp1d2	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
2		zob	⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )
3	1 2	bitrd	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℤ ) )