Theorem oddz 47635

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7353  1c1 11029   + caddc 11031   / cdiv 11796  2c2 12202  ℤcz 12490   Odd codd 47629

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-odd 47631

This theorem is referenced by:  oddm1div2z  47638  oddp1eveni  47645  oddm1eveni  47646  m1expoddALTV  47652  2dvdsoddp1  47660  2dvdsoddm1  47661  zofldiv2ALTV  47666  oddflALTV  47667  gcd2odd1  47672  oexpnegALTV  47681  oexpnegnz  47682  bits0oALTV  47685  opoeALTV  47687  opeoALTV  47688  omoeALTV  47689  omeoALTV  47690  epoo  47707  emoo  47708  stgoldbwt  47780  sbgoldbwt  47781  sbgoldbst  47782  sbgoldbm  47788  bgoldbtbndlem1  47809  bgoldbtbndlem2  47810  bgoldbtbndlem3  47811  bgoldbtbndlem4  47812  bgoldbtbnd  47813  tgoldbach  47821