Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  oddz Structured version   Visualization version   GIF version

Theorem oddz 42054
 Description: An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
oddz (𝑍 ∈ Odd → 𝑍 ∈ ℤ)

Proof of Theorem oddz
StepHypRef Expression
1 isodd 42052 . 2 (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))
21simplbi 478 1 (𝑍 ∈ Odd → 𝑍 ∈ ℤ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2139  (class class class)co 6813  1c1 10129   + caddc 10131   / cdiv 10876  2c2 11262  ℤcz 11569   Odd codd 42048 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-odd 42050 This theorem is referenced by:  oddm1div2z  42057  oddp1eveni  42064  oddm1eveni  42065  m1expoddALTV  42071  2dvdsoddp1  42078  2dvdsoddm1  42079  zofldiv2ALTV  42084  oddflALTV  42085  oexpnegALTV  42098  oexpnegnz  42099  bits0oALTV  42102  opoeALTV  42104  opeoALTV  42105  omoeALTV  42106  omeoALTV  42107  epoo  42122  emoo  42123  stgoldbwt  42174  sbgoldbwt  42175  sbgoldbst  42176  sbgoldbm  42182  bgoldbtbndlem1  42203  bgoldbtbndlem2  42204  bgoldbtbndlem3  42205  bgoldbtbndlem4  42206  bgoldbtbnd  42207  tgoldbach  42215  tgoldbachOLD  42222
 Copyright terms: Public domain W3C validator