Theorem zre 12597

Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
zre	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 12595	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 497	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11133  0cc0 11134  -cneg 11472  ℕcn 12245  ℤcz 12593

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-3or 1087  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-neg 11474  df-z 12594

This theorem is referenced by:  zcn  12598  zrei  12599  zssre  12600  elnn0z  12606  elnnz1  12623  znnnlt1  12624  zletr  12641  znnsub  12643  znn0sub  12644  nzadd  12645  zltp1le  12647  zleltp1  12648  nn0ge0div  12667  zextle  12671  btwnnz  12674  suprzcl  12678  msqznn  12680  peano2uz2  12686  uzind  12690  fzind  12696  fnn0ind  12697  eluzuzle  12866  uzid  12872  uzneg  12877  uztric  12881  uz11  12882  eluzp1m1  12883  eluzp1p1  12885  eluzadd  12886  eluzsub  12887  eluzaddiOLD  12889  eluzsubiOLD  12891  subeluzsub  12894  uzin  12897  uz3m2nn  12912  peano2uz  12922  nn0pzuz  12926  uzwo  12932  eluz2b2  12942  uz2mulcl  12947  uzinfi  12949  eqreznegel  12955  lbzbi  12957  uzsupss  12961  nn01to3  12962  zmin  12965  zmax  12966  zbtwnre  12967  rebtwnz  12968  qre  12974  elpq  12996  rpnnen1lem2  12998  rpnnen1lem1  12999  rpnnen1lem3  13000  rpnnen1lem5  13002  z2ge  13219  qbtwnre  13220  zltaddlt1le  13527  elfz1eq  13557  fzn  13562  fzen  13563  uzsubsubfz  13568  fzaddel  13580  fzadd2  13581  ssfzunsnext  13591  ssfzunsn  13592  fzsuc2  13604  fzrev  13609  elfz1b  13615  fznuz  13631  uznfz  13632  fzp1nel  13633  elfz0fzfz0  13655  fz0fzelfz0  13656  fznn0sub2  13657  fz0fzdiffz0  13659  elfzmlbp  13661  difelfznle  13664  nelfzo  13686  elfzouz2  13696  fzo0n  13703  fzonlt0  13704  fzossrbm1  13710  fzospliti  13713  elfzo0z  13723  fzofzim  13731  fzo1fzo0n0  13736  eluzgtdifelfzo  13748  fzossfzop1  13764  ssfzoulel  13781  ssfzo12bi  13782  elfzonelfzo  13790  elfzomelpfzo  13792  elfznelfzob  13794  fzostep1  13804  fllt  13828  flid  13830  flbi2  13839  2tnp1ge0ge0  13851  flhalf  13852  fldiv4p1lem1div2  13857  fldiv4lem1div2uz2  13858  dfceil2  13861  ceile  13871  ceilid  13873  quoremz  13877  intfracq  13881  uzsup  13885  mulmod0  13899  zmod10  13909  zmodcl  13913  zmodfz  13915  zmodid2  13921  modcyc  13928  mulp1mod1  13934  muladdmod  13935  modmuladd  13936  modmuladdim  13937  modmul1  13947  modaddmodup  13957  modaddmodlo  13958  modaddmulmod  13961  zsqcl2  14161  leexp2  14194  iexpcyc  14230  fi1uzind  14530  ccatsymb  14605  ccatval21sw  14608  lswccatn0lsw  14614  swrdnd  14677  swrdnnn0nd  14679  swrd0  14681  swrdswrdlem  14727  swrdswrd  14728  swrdccatin2  14752  pfxccatin12lem2  14754  pfxccatin12lem3  14755  repswswrd  14807  cshwmodn  14818  cshwsublen  14819  cshwidxmod  14826  cshwidxmodr  14827  cshwidxm1  14830  repswcshw  14835  2cshw  14836  cshweqrep  14844  cshw1  14845  swrd2lsw  14976  nn0abscl  15336  rexuzre  15376  dvdsval3  16281  p1modz1  16284  moddvds  16288  absdvdsb  16299  dvdsabsb  16300  dvdsle  16334  alzdvds  16344  mod2eq1n2dvds  16371  evennn02n  16374  evennn2n  16375  ltoddhalfle  16385  divalgmod  16430  fldivndvdslt  16440  flodddiv4t2lthalf  16442  bitsp1o  16457  gcdabs1  16553  modgcd  16556  bezoutlem1  16563  dfgcd2  16570  algcvga  16603  lcmabs  16629  isprm3  16707  dvdsnprmd  16714  2mulprm  16717  oddprmgt2  16723  sqnprm  16726  zgcdsq  16777  hashdvds  16799  vfermltlALT  16827  powm2modprm  16828  modprm0  16830  modprmn0modprm0  16832  fldivp1  16922  zgz  16958  4sqlem4  16977  prmgaplem5  17080  prmgaplem7  17082  cshwshashlem2  17121  setsstruct  17200  mulgmodid  19101  gexdvds  19570  zringunit  21432  prmirred  21440  znf1o  21517  chfacfscmul0  22801  chfacfscmulgsum  22803  chfacfpmmul0  22805  chfacfpmmulgsum  22807  dyadf  25549  dyadovol  25551  degltlem1  26034  coskpi  26489  cosne0  26495  relogexp  26562  cxpeq  26724  relogbzexp  26743  ppival2  27095  ppival2g  27096  ppiprm  27118  chtprm  27120  chtnprm  27121  ppip1le  27128  efexple  27249  zabsle1  27264  lgsdir2lem4  27296  lgsne0  27303  gausslemma2dlem1a  27333  gausslemma2dlem3  27336  gausslemma2dlem4  27337  lgsquadlem1  27348  lgsquadlem2  27349  2lgslem1a1  27357  2lgslem1a2  27358  2sqlem2  27386  rplogsumlem2  27453  pntrsumbnd  27534  axlowdim  28945  crctcshwlkn0lem3  29799  crctcshwlkn0lem5  29801  crctcshwlkn0  29808  crctcsh  29811  clwlkclwwlklem2fv2  29982  clwlkclwwlklem2a  29984  clwwisshclwwslemlem  29999  clwwlkinwwlk  30026  clwwlkext2edg  30042  wwlksubclwwlk  30044  numclwwlk5  30374  topnfbey  30455  uzssico  32766  1fldgenq  33321  znfermltl  33386  rezh  34005  zrhre  34055  hashf2  34120  ballotlemfc0  34530  ballotlemfcc  34531  chpvalz  34665  chtvalz  34666  zltp1ne  35137  0nn0m1nnn0  35140  elfzm12  35702  nn0prpwlem  36345  poimirlem24  37673  mblfinlem1  37686  mblfinlem2  37687  itg2addnclem2  37701  fzmul  37770  incsequz2  37778  fimgmcyc  42532  ellz1  42765  lzunuz  42766  lzenom  42768  nerabdioph  42807  pell14qrgt0  42857  rmxycomplete  42916  monotuz  42940  monotoddzzfi  42941  oddcomabszz  42943  zindbi  42945  jm2.24  42962  congrep  42972  fzneg  42981  jm2.19  42992  fzunt  43454  fzunt1d  43456  fzuntgd  43457  oddfl  45286  fzdifsuc2  45319  climsuse  45617  stoweidlem26  46035  stoweidlem34  46043  fourierdlem20  46136  fourierdlem42  46158  fourierdlem51  46166  fourierdlem64  46179  fourierdlem76  46191  fourierdlem94  46209  fourierdlem97  46212  fourierdlem113  46228  natlocalincr  46885  natglobalincr  46886  zm1nn  47311  zgeltp1eq  47318  eluzge0nn0  47321  elfz2z  47324  2elfz2melfz  47327  elfzlble  47329  elfzelfzlble  47330  fzopredsuc  47332  ceilbi  47342  smonoord  47365  fsummmodsndifre  47368  iccpartipre  47415  iccpartiltu  47416  iccpartigtl  47417  icceuelpartlem  47429  fmtno4prmfac  47566  lighneallem4b  47603  dfeven3  47652  dfodd4  47653  nn0o1gt2ALTV  47688  nnoALTV  47689  fpprel2  47735  gbegt5  47755  gbowgt5  47756  sbgoldbwt  47771  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  evengpop3  47792  evengpoap3  47793  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  gpgprismgriedgdmss  48036  gpgusgralem  48040  gpgedgvtx1  48046  gpg5nbgrvtx03starlem2  48051  gpg5nbgrvtx13starlem2  48054  gpg3nbgrvtx0  48058  cznnring  48217  elfzolborelfzop1  48475  zgtp1leeq  48477  mod0mul  48479  modn0mul  48480  m1modmmod  48481  difmodm1lt  48482  rege1logbzge0  48519  fllog2  48528  dignn0ldlem  48562  dignn0flhalflem1  48575  dignn0flhalflem2  48576