Theorem oddz 48454

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  1c1 11116   + caddc 11118   / cdiv 11886  2c2 12310  ℤcz 12606   Odd codd 48448

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-odd 48450

This theorem is used by:  oddm1div2z  48457  oddp1eveni  48464  oddm1eveni  48465  m1expoddALTV  48471  2dvdsoddp1  48479  2dvdsoddm1  48480  zofldiv2ALTV  48485  oddflALTV  48486  gcd2odd1  48491  oexpnegALTV  48500  oexpnegnz  48501  bits0oALTV  48504  opoeALTV  48506  opeoALTV  48507  omoeALTV  48508  omeoALTV  48509  epoo  48526  emoo  48527  stgoldbwt  48599  sbgoldbwt  48600  sbgoldbst  48601  sbgoldbm  48607  bgoldbtbndlem1  48628  bgoldbtbndlem2  48629  bgoldbtbndlem3  48630  bgoldbtbndlem4  48631  bgoldbtbnd  48632  tgoldbach  48640