Theorem oddz 45943

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7362  1c1 11061   + caddc 11063   / cdiv 11821  2c2 12217  ℤcz 12508   Odd codd 45937

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-odd 45939

This theorem is referenced by:  oddm1div2z  45946  oddp1eveni  45953  oddm1eveni  45954  m1expoddALTV  45960  2dvdsoddp1  45968  2dvdsoddm1  45969  zofldiv2ALTV  45974  oddflALTV  45975  gcd2odd1  45980  oexpnegALTV  45989  oexpnegnz  45990  bits0oALTV  45993  opoeALTV  45995  opeoALTV  45996  omoeALTV  45997  omeoALTV  45998  epoo  46015  emoo  46016  stgoldbwt  46088  sbgoldbwt  46089  sbgoldbst  46090  sbgoldbm  46096  bgoldbtbndlem1  46117  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbndlem4  46120  bgoldbtbnd  46121  tgoldbach  46129