Theorem oddz 45050

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7277  1c1 10870   + caddc 10872   / cdiv 11630  2c2 12026  ℤcz 12317   Odd codd 45044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5077  df-iota 6393  df-fv 6443  df-ov 7280  df-odd 45046

This theorem is referenced by:  oddm1div2z  45053  oddp1eveni  45060  oddm1eveni  45061  m1expoddALTV  45067  2dvdsoddp1  45075  2dvdsoddm1  45076  zofldiv2ALTV  45081  oddflALTV  45082  gcd2odd1  45087  oexpnegALTV  45096  oexpnegnz  45097  bits0oALTV  45100  opoeALTV  45102  opeoALTV  45103  omoeALTV  45104  omeoALTV  45105  epoo  45122  emoo  45123  stgoldbwt  45195  sbgoldbwt  45196  sbgoldbst  45197  sbgoldbm  45203  bgoldbtbndlem1  45224  bgoldbtbndlem2  45225  bgoldbtbndlem3  45226  bgoldbtbndlem4  45227  bgoldbtbnd  45228  tgoldbach  45236