Theorem oddz 44149

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

Assertion

Ref	Expression
oddz	⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)

Proof of Theorem oddz

Step	Hyp	Ref	Expression
1		isodd 44147	. 2 ⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))
2	1	simplbi 501	1 ⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7135  1c1 10527   + caddc 10529   / cdiv 11286  2c2 11680  ℤcz 11969   Odd codd 44143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-odd 44145

This theorem is referenced by:  oddm1div2z  44152  oddp1eveni  44159  oddm1eveni  44160  m1expoddALTV  44166  2dvdsoddp1  44174  2dvdsoddm1  44175  zofldiv2ALTV  44180  oddflALTV  44181  gcd2odd1  44186  oexpnegALTV  44195  oexpnegnz  44196  bits0oALTV  44199  opoeALTV  44201  opeoALTV  44202  omoeALTV  44203  omeoALTV  44204  epoo  44221  emoo  44222  stgoldbwt  44294  sbgoldbwt  44295  sbgoldbst  44296  sbgoldbm  44302  bgoldbtbndlem1  44323  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  bgoldbtbnd  44327  tgoldbach  44335