Theorem oddz 47877

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  1c1 11027   + caddc 11029   / cdiv 11794  2c2 12200  ℤcz 12488   Odd codd 47871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-odd 47873

This theorem is referenced by:  oddm1div2z  47880  oddp1eveni  47887  oddm1eveni  47888  m1expoddALTV  47894  2dvdsoddp1  47902  2dvdsoddm1  47903  zofldiv2ALTV  47908  oddflALTV  47909  gcd2odd1  47914  oexpnegALTV  47923  oexpnegnz  47924  bits0oALTV  47927  opoeALTV  47929  opeoALTV  47930  omoeALTV  47931  omeoALTV  47932  epoo  47949  emoo  47950  stgoldbwt  48022  sbgoldbwt  48023  sbgoldbst  48024  sbgoldbm  48030  bgoldbtbndlem1  48051  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgoldbach  48063