Theorem oddz 47625

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7410  1c1 11135   + caddc 11137   / cdiv 11899  2c2 12300  ℤcz 12593   Odd codd 47619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-odd 47621

This theorem is referenced by:  oddm1div2z  47628  oddp1eveni  47635  oddm1eveni  47636  m1expoddALTV  47642  2dvdsoddp1  47650  2dvdsoddm1  47651  zofldiv2ALTV  47656  oddflALTV  47657  gcd2odd1  47662  oexpnegALTV  47671  oexpnegnz  47672  bits0oALTV  47675  opoeALTV  47677  opeoALTV  47678  omoeALTV  47679  omeoALTV  47680  epoo  47697  emoo  47698  stgoldbwt  47770  sbgoldbwt  47771  sbgoldbst  47772  sbgoldbm  47778  bgoldbtbndlem1  47799  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  tgoldbach  47811