Theorem oddz 47991

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  1c1 11039   + caddc 11041   / cdiv 11806  2c2 12212  ℤcz 12500   Odd codd 47985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-odd 47987

This theorem is referenced by:  oddm1div2z  47994  oddp1eveni  48001  oddm1eveni  48002  m1expoddALTV  48008  2dvdsoddp1  48016  2dvdsoddm1  48017  zofldiv2ALTV  48022  oddflALTV  48023  gcd2odd1  48028  oexpnegALTV  48037  oexpnegnz  48038  bits0oALTV  48041  opoeALTV  48043  opeoALTV  48044  omoeALTV  48045  omeoALTV  48046  epoo  48063  emoo  48064  stgoldbwt  48136  sbgoldbwt  48137  sbgoldbst  48138  sbgoldbm  48144  bgoldbtbndlem1  48165  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  tgoldbach  48177