Metamath Proof Explorer

Theorem isodd

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 integer increased by 1 and then divided by 2 is still an integer. (Contributed by AV, 14-Jun-2020)

Ref Expression
Assertion isodd ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ Z + 1 2 ∈ ℤ

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ z = Z → z + 1 = Z + 1
2 1 oveq1d ⊢ z = Z → z + 1 2 = Z + 1 2
3 2 eleq1d ⊢ z = Z → z + 1 2 ∈ ℤ ↔ Z + 1 2 ∈ ℤ
4 df-odd ⊢ Odd = z ∈ ℤ | z + 1 2 ∈ ℤ
5 3 4 elrab2 ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ Z + 1 2 ∈ ℤ