Theorem oddz 42551

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 6922  1c1 10273   + caddc 10275   / cdiv 11032  2c2 11430  ℤcz 11728   Odd codd 42545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-rex 3095  df-rab 3098  df-v 3399  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-odd 42547

This theorem is referenced by:  oddm1div2z  42554  oddp1eveni  42561  oddm1eveni  42562  m1expoddALTV  42568  2dvdsoddp1  42575  2dvdsoddm1  42576  zofldiv2ALTV  42581  oddflALTV  42582  oexpnegALTV  42595  oexpnegnz  42596  bits0oALTV  42599  opoeALTV  42601  opeoALTV  42602  omoeALTV  42603  omeoALTV  42604  epoo  42619  emoo  42620  stgoldbwt  42671  sbgoldbwt  42672  sbgoldbst  42673  sbgoldbm  42679  bgoldbtbndlem1  42700  bgoldbtbndlem2  42701  bgoldbtbndlem3  42702  bgoldbtbndlem4  42703  bgoldbtbnd  42704  tgoldbach  42712