Theorem oddz 48396

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  1c1 11096   + caddc 11098   / cdiv 11866  2c2 12290  ℤcz 12586   Odd codd 48390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-odd 48392

This theorem is referenced by:  oddm1div2z  48399  oddp1eveni  48406  oddm1eveni  48407  m1expoddALTV  48413  2dvdsoddp1  48421  2dvdsoddm1  48422  zofldiv2ALTV  48427  oddflALTV  48428  gcd2odd1  48433  oexpnegALTV  48442  oexpnegnz  48443  bits0oALTV  48446  opoeALTV  48448  opeoALTV  48449  omoeALTV  48450  omeoALTV  48451  epoo  48468  emoo  48469  stgoldbwt  48541  sbgoldbwt  48542  sbgoldbst  48543  sbgoldbm  48549  bgoldbtbndlem1  48570  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbndlem4  48573  bgoldbtbnd  48574  tgoldbach  48582