Theorem oddz 48122

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  1c1 11030   + caddc 11032   / cdiv 11798  2c2 12227  ℤcz 12515   Odd codd 48116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-odd 48118

This theorem is referenced by:  oddm1div2z  48125  oddp1eveni  48132  oddm1eveni  48133  m1expoddALTV  48139  2dvdsoddp1  48147  2dvdsoddm1  48148  zofldiv2ALTV  48153  oddflALTV  48154  gcd2odd1  48159  oexpnegALTV  48168  oexpnegnz  48169  bits0oALTV  48172  opoeALTV  48174  opeoALTV  48175  omoeALTV  48176  omeoALTV  48177  epoo  48194  emoo  48195  stgoldbwt  48267  sbgoldbwt  48268  sbgoldbst  48269  sbgoldbm  48275  bgoldbtbndlem1  48296  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  tgoldbach  48308