Theorem oddz 40082

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 40080	. 2 ⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))
2	1	simplbi 475	1 ⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  1c1 9816   + caddc 9818   / cdiv 10563  2c2 10947  ℤcz 11254   Odd codd 40076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-odd 40078

This theorem is referenced by:  oddm1div2z  40085  oddp1eveni  40092  oddm1eveni  40093  m1expoddALTV  40099  2dvdsoddp1  40106  2dvdsoddm1  40107  zofldiv2ALTV  40112  oddflALTV  40113  oexpnegALTV  40126  oexpnegnz  40127  bits0oALTV  40130  opoeALTV  40132  opeoALTV  40133  omoeALTV  40134  omeoALTV  40135  epoo  40150  emoo  40151  stgoldbwt  40198  bgoldbwt  40199  bgoldbst  40200  bgoldbtbndlem1  40221  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239