Theorem oddz 47662

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7341  1c1 11002   + caddc 11004   / cdiv 11769  2c2 12175  ℤcz 12463   Odd codd 47656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-odd 47658

This theorem is referenced by:  oddm1div2z  47665  oddp1eveni  47672  oddm1eveni  47673  m1expoddALTV  47679  2dvdsoddp1  47687  2dvdsoddm1  47688  zofldiv2ALTV  47693  oddflALTV  47694  gcd2odd1  47699  oexpnegALTV  47708  oexpnegnz  47709  bits0oALTV  47712  opoeALTV  47714  opeoALTV  47715  omoeALTV  47716  omeoALTV  47717  epoo  47734  emoo  47735  stgoldbwt  47807  sbgoldbwt  47808  sbgoldbst  47809  sbgoldbm  47815  bgoldbtbndlem1  47836  bgoldbtbndlem2  47837  bgoldbtbndlem3  47838  bgoldbtbndlem4  47839  bgoldbtbnd  47840  tgoldbach  47848