Theorem oddz 45035

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7268  1c1 10856   + caddc 10858   / cdiv 11615  2c2 12011  ℤcz 12302   Odd codd 45029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-odd 45031

This theorem is referenced by:  oddm1div2z  45038  oddp1eveni  45045  oddm1eveni  45046  m1expoddALTV  45052  2dvdsoddp1  45060  2dvdsoddm1  45061  zofldiv2ALTV  45066  oddflALTV  45067  gcd2odd1  45072  oexpnegALTV  45081  oexpnegnz  45082  bits0oALTV  45085  opoeALTV  45087  opeoALTV  45088  omoeALTV  45089  omeoALTV  45090  epoo  45107  emoo  45108  stgoldbwt  45180  sbgoldbwt  45181  sbgoldbst  45182  sbgoldbm  45188  bgoldbtbndlem1  45209  bgoldbtbndlem2  45210  bgoldbtbndlem3  45211  bgoldbtbndlem4  45212  bgoldbtbnd  45213  tgoldbach  45221