Metamath Proof Explorer

Theorem oddm1div2z

Description: The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020)

Ref Expression
Assertion oddm1div2z ⊢ Z ∈ Odd → Z − 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 oddp1div2z ⊢ Z ∈ Odd → Z + 1 2 ∈ ℤ
2 oddz ⊢ Z ∈ Odd → Z ∈ ℤ
3 zob ⊢ Z ∈ ℤ → Z + 1 2 ∈ ℤ ↔ Z − 1 2 ∈ ℤ
4 2 3 syl ⊢ Z ∈ Odd → Z + 1 2 ∈ ℤ ↔ Z − 1 2 ∈ ℤ
5 1 4 mpbid ⊢ Z ∈ Odd → Z − 1 2 ∈ ℤ