Theorem oddz 47632

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  1c1 11069   + caddc 11071   / cdiv 11835  2c2 12241  ℤcz 12529   Odd codd 47626

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-odd 47628

This theorem is referenced by:  oddm1div2z  47635  oddp1eveni  47642  oddm1eveni  47643  m1expoddALTV  47649  2dvdsoddp1  47657  2dvdsoddm1  47658  zofldiv2ALTV  47663  oddflALTV  47664  gcd2odd1  47669  oexpnegALTV  47678  oexpnegnz  47679  bits0oALTV  47682  opoeALTV  47684  opeoALTV  47685  omoeALTV  47686  omeoALTV  47687  epoo  47704  emoo  47705  stgoldbwt  47777  sbgoldbwt  47778  sbgoldbst  47779  sbgoldbm  47785  bgoldbtbndlem1  47806  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  tgoldbach  47818