Metamath Proof Explorer

Theorem oddz

Description: An odd number is an integer. (Contributed by AV, 14-Jun-2020)

Ref Expression
Assertion oddz ⊢ Z ∈ Odd → Z ∈ ℤ

Proof

Step Hyp Ref Expression
1 isodd ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ Z + 1 2 ∈ ℤ
2 1 simplbi ⊢ Z ∈ Odd → Z ∈ ℤ