Metamath Proof Explorer

Theorem isodd2

Description: The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd number decreased by 1 and then divided by 2 is still an integer. (Contributed by AV, 15-Jun-2020)

Ref Expression
Assertion isodd2 ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ Z − 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 isodd ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ Z + 1 2 ∈ ℤ
2 zob ⊢ Z ∈ ℤ → Z + 1 2 ∈ ℤ ↔ Z − 1 2 ∈ ℤ
3 2 pm5.32i ⊢ Z ∈ ℤ ∧ Z + 1 2 ∈ ℤ ↔ Z ∈ ℤ ∧ Z − 1 2 ∈ ℤ
4 1 3 bitri ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ Z − 1 2 ∈ ℤ