Theorem oddz 47556

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7431  1c1 11154   + caddc 11156   / cdiv 11918  2c2 12319  ℤcz 12611   Odd codd 47550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-odd 47552

This theorem is referenced by:  oddm1div2z  47559  oddp1eveni  47566  oddm1eveni  47567  m1expoddALTV  47573  2dvdsoddp1  47581  2dvdsoddm1  47582  zofldiv2ALTV  47587  oddflALTV  47588  gcd2odd1  47593  oexpnegALTV  47602  oexpnegnz  47603  bits0oALTV  47606  opoeALTV  47608  opeoALTV  47609  omoeALTV  47610  omeoALTV  47611  epoo  47628  emoo  47629  stgoldbwt  47701  sbgoldbwt  47702  sbgoldbst  47703  sbgoldbm  47709  bgoldbtbndlem1  47730  bgoldbtbndlem2  47731  bgoldbtbndlem3  47732  bgoldbtbndlem4  47733  bgoldbtbnd  47734  tgoldbach  47742