Theorem oddz 48214

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 7391  1c1 11068   + caddc 11070   / cdiv 11838  2c2 12266  ℤcz 12562   Odd codd 48208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-odd 48210

This theorem is referenced by:  oddm1div2z  48217  oddp1eveni  48224  oddm1eveni  48225  m1expoddALTV  48231  2dvdsoddp1  48239  2dvdsoddm1  48240  zofldiv2ALTV  48245  oddflALTV  48246  gcd2odd1  48251  oexpnegALTV  48260  oexpnegnz  48261  bits0oALTV  48264  opoeALTV  48266  opeoALTV  48267  omoeALTV  48268  omeoALTV  48269  epoo  48286  emoo  48287  stgoldbwt  48359  sbgoldbwt  48360  sbgoldbst  48361  sbgoldbm  48367  bgoldbtbndlem1  48388  bgoldbtbndlem2  48389  bgoldbtbndlem3  48390  bgoldbtbndlem4  48391  bgoldbtbnd  48392  tgoldbach  48400