Theorem oddz 47605

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  1c1 11045   + caddc 11047   / cdiv 11811  2c2 12217  ℤcz 12505   Odd codd 47599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-odd 47601

This theorem is referenced by:  oddm1div2z  47608  oddp1eveni  47615  oddm1eveni  47616  m1expoddALTV  47622  2dvdsoddp1  47630  2dvdsoddm1  47631  zofldiv2ALTV  47636  oddflALTV  47637  gcd2odd1  47642  oexpnegALTV  47651  oexpnegnz  47652  bits0oALTV  47655  opoeALTV  47657  opeoALTV  47658  omoeALTV  47659  omeoALTV  47660  epoo  47677  emoo  47678  stgoldbwt  47750  sbgoldbwt  47751  sbgoldbst  47752  sbgoldbm  47758  bgoldbtbndlem1  47779  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbndlem4  47782  bgoldbtbnd  47783  tgoldbach  47791