Theorem oddz 47736

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7352  1c1 11013   + caddc 11015   / cdiv 11780  2c2 12186  ℤcz 12474   Odd codd 47730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6443  df-fv 6495  df-ov 7355  df-odd 47732

This theorem is referenced by:  oddm1div2z  47739  oddp1eveni  47746  oddm1eveni  47747  m1expoddALTV  47753  2dvdsoddp1  47761  2dvdsoddm1  47762  zofldiv2ALTV  47767  oddflALTV  47768  gcd2odd1  47773  oexpnegALTV  47782  oexpnegnz  47783  bits0oALTV  47786  opoeALTV  47788  opeoALTV  47789  omoeALTV  47790  omeoALTV  47791  epoo  47808  emoo  47809  stgoldbwt  47881  sbgoldbwt  47882  sbgoldbst  47883  sbgoldbm  47889  bgoldbtbndlem1  47910  bgoldbtbndlem2  47911  bgoldbtbndlem3  47912  bgoldbtbndlem4  47913  bgoldbtbnd  47914  tgoldbach  47922