Users' Mathboxes 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 39884
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 39882 . 2 (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))
21simplbi 474 1 (𝑍 ∈ Odd → 𝑍 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6524  1c1 9790   + caddc 9792   / cdiv 10530  2c2 10914  cz 11207   Odd codd 39878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-odd 39880
This theorem is referenced by:  oddm1div2z  39887  oddp1eveni  39894  oddm1eveni  39895  m1expoddALTV  39901  2dvdsoddp1  39908  2dvdsoddm1  39909  zofldiv2ALTV  39914  oddflALTV  39915  oexpnegALTV  39928  oexpnegnz  39929  bits0oALTV  39932  opoeALTV  39934  opeoALTV  39935  omoeALTV  39936  omeoALTV  39937  epoo  39952  emoo  39953  stgoldbwt  40000  bgoldbwt  40001  bgoldbst  40002  bgoldbtbndlem1  40023  bgoldbtbndlem2  40024  bgoldbtbndlem3  40025  bgoldbtbndlem4  40026  bgoldbtbnd  40027  tgoldbach  40034  tgoldbachOLD  40041
  Copyright terms: Public domain W3C validator