Theorem zre 12601

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 12599	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 497	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107  ℝcr 11137  0cc0 11138  -cneg 11476  ℕcn 12249  ℤcz 12597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-iota 6495  df-fv 6550  df-ov 7417  df-neg 11478  df-z 12598

This theorem is referenced by:  zcn  12602  zrei  12603  zssre  12604  elnn0z  12610  elnnz1  12627  znnnlt1  12628  zletr  12645  znnsub  12647  znn0sub  12648  nzadd  12649  zltp1le  12651  zleltp1  12652  nn0ge0div  12671  zextle  12675  btwnnz  12678  suprzcl  12682  msqznn  12684  peano2uz2  12690  uzind  12694  fzind  12700  fnn0ind  12701  eluzuzle  12870  uzid  12876  uzneg  12881  uztric  12885  uz11  12886  eluzp1m1  12887  eluzp1p1  12889  eluzadd  12890  eluzsub  12891  eluzaddiOLD  12893  eluzsubiOLD  12895  subeluzsub  12898  uzin  12901  uz3m2nn  12916  peano2uz  12926  nn0pzuz  12930  uzwo  12936  eluz2b2  12946  uz2mulcl  12951  uzinfi  12953  eqreznegel  12959  lbzbi  12961  uzsupss  12965  nn01to3  12966  zmin  12969  zmax  12970  zbtwnre  12971  rebtwnz  12972  qre  12978  elpq  13000  rpnnen1lem2  13002  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  z2ge  13223  qbtwnre  13224  zltaddlt1le  13528  elfz1eq  13558  fzn  13563  fzen  13564  uzsubsubfz  13569  fzaddel  13581  fzadd2  13582  ssfzunsnext  13592  ssfzunsn  13593  fzsuc2  13605  fzrev  13610  elfz1b  13616  fznuz  13632  uznfz  13633  fzp1nel  13634  elfz0fzfz0  13656  fz0fzelfz0  13657  fznn0sub2  13658  fz0fzdiffz0  13660  elfzmlbp  13662  difelfznle  13665  nelfzo  13687  elfzouz2  13697  fzo0n  13704  fzonlt0  13705  fzossrbm1  13711  fzospliti  13714  elfzo0z  13724  fzofzim  13732  fzo1fzo0n0  13737  eluzgtdifelfzo  13749  fzossfzop1  13765  ssfzoulel  13782  ssfzo12bi  13783  elfzonelfzo  13791  elfzomelpfzo  13793  elfznelfzob  13795  fzostep1  13805  fllt  13829  flid  13831  flbi2  13840  2tnp1ge0ge0  13852  flhalf  13853  fldiv4p1lem1div2  13858  fldiv4lem1div2uz2  13859  dfceil2  13862  ceile  13872  ceilid  13874  quoremz  13878  intfracq  13882  uzsup  13886  mulmod0  13900  zmod10  13910  zmodcl  13914  zmodfz  13916  zmodid2  13922  modcyc  13929  mulp1mod1  13935  muladdmod  13936  modmuladd  13937  modmuladdim  13938  modmul1  13948  modaddmodup  13958  modaddmodlo  13959  modaddmulmod  13962  zsqcl2  14161  leexp2  14194  iexpcyc  14229  fi1uzind  14529  ccatsymb  14603  ccatval21sw  14606  lswccatn0lsw  14612  swrdnd  14675  swrdnnn0nd  14677  swrd0  14679  swrdswrdlem  14725  swrdswrd  14726  swrdccatin2  14750  pfxccatin12lem2  14752  pfxccatin12lem3  14753  repswswrd  14805  cshwmodn  14816  cshwsublen  14817  cshwidxmod  14824  cshwidxmodr  14825  cshwidxm1  14828  repswcshw  14833  2cshw  14834  cshweqrep  14842  cshw1  14843  swrd2lsw  14974  nn0abscl  15334  rexuzre  15374  dvdsval3  16277  p1modz1  16280  moddvds  16284  absdvdsb  16295  dvdsabsb  16296  dvdsle  16330  alzdvds  16340  mod2eq1n2dvds  16367  evennn02n  16370  evennn2n  16371  ltoddhalfle  16381  divalgmod  16426  fldivndvdslt  16436  flodddiv4t2lthalf  16438  bitsp1o  16453  gcdabs1  16549  modgcd  16552  bezoutlem1  16559  dfgcd2  16566  algcvga  16599  lcmabs  16625  isprm3  16703  dvdsnprmd  16710  2mulprm  16713  oddprmgt2  16719  sqnprm  16722  zgcdsq  16773  hashdvds  16795  vfermltlALT  16823  powm2modprm  16824  modprm0  16826  modprmn0modprm0  16828  fldivp1  16918  zgz  16954  4sqlem4  16973  prmgaplem5  17076  prmgaplem7  17078  cshwshashlem2  17117  setsstruct  17196  mulgmodid  19105  gexdvds  19575  zringunit  21444  prmirred  21452  znf1o  21537  chfacfscmul0  22831  chfacfscmulgsum  22833  chfacfpmmul0  22835  chfacfpmmulgsum  22837  dyadf  25581  dyadovol  25583  degltlem1  26066  coskpi  26520  cosne0  26526  relogexp  26593  cxpeq  26755  relogbzexp  26774  ppival2  27126  ppival2g  27127  ppiprm  27149  chtprm  27151  chtnprm  27152  ppip1le  27159  efexple  27280  zabsle1  27295  lgsdir2lem4  27327  lgsne0  27334  gausslemma2dlem1a  27364  gausslemma2dlem3  27367  gausslemma2dlem4  27368  lgsquadlem1  27379  lgsquadlem2  27380  2lgslem1a1  27388  2lgslem1a2  27389  2sqlem2  27417  rplogsumlem2  27484  pntrsumbnd  27565  axlowdim  28925  crctcshwlkn0lem3  29779  crctcshwlkn0lem5  29781  crctcshwlkn0  29788  crctcsh  29791  clwlkclwwlklem2fv2  29962  clwlkclwwlklem2a  29964  clwwisshclwwslemlem  29979  clwwlkinwwlk  30006  clwwlkext2edg  30022  wwlksubclwwlk  30024  numclwwlk5  30354  topnfbey  30435  uzssico  32733  1fldgenq  33270  znfermltl  33335  rezh  33911  zrhre  33961  hashf2  34026  ballotlemfc0  34436  ballotlemfcc  34437  chpvalz  34584  chtvalz  34585  zltp1ne  35056  0nn0m1nnn0  35059  elfzm12  35621  nn0prpwlem  36264  poimirlem24  37592  mblfinlem1  37605  mblfinlem2  37606  itg2addnclem2  37620  fzmul  37689  incsequz2  37697  fimgmcyc  42489  ellz1  42723  lzunuz  42724  lzenom  42726  nerabdioph  42765  pell14qrgt0  42815  rmxycomplete  42874  monotuz  42898  monotoddzzfi  42899  oddcomabszz  42901  zindbi  42903  jm2.24  42920  congrep  42930  fzneg  42939  jm2.19  42950  fzunt  43413  fzunt1d  43415  fzuntgd  43416  oddfl  45234  fzdifsuc2  45267  climsuse  45568  stoweidlem26  45986  stoweidlem34  45994  fourierdlem20  46087  fourierdlem42  46109  fourierdlem51  46117  fourierdlem64  46130  fourierdlem76  46142  fourierdlem94  46160  fourierdlem97  46163  fourierdlem113  46179  natlocalincr  46836  natglobalincr  46837  zm1nn  47260  zgeltp1eq  47267  eluzge0nn0  47270  elfz2z  47273  2elfz2melfz  47276  elfzlble  47278  elfzelfzlble  47279  fzopredsuc  47281  smonoord  47304  fsummmodsndifre  47307  iccpartipre  47354  iccpartiltu  47355  iccpartigtl  47356  icceuelpartlem  47368  fmtno4prmfac  47505  lighneallem4b  47542  dfeven3  47591  dfodd4  47592  nn0o1gt2ALTV  47627  nnoALTV  47628  fpprel2  47674  gbegt5  47694  gbowgt5  47695  sbgoldbwt  47710  nnsum3primesle9  47727  nnsum4primesodd  47729  nnsum4primesoddALTV  47730  evengpop3  47731  evengpoap3  47732  nnsum4primesevenALTV  47734  bgoldbtbndlem1  47738  bgoldbtbndlem2  47739  bgoldbtbndlem3  47740  bgoldbtbndlem4  47741  gpgusgralem  47957  gpgedgvtx1  47966  gpg5nbgrvtx03starlem2  47971  gpg5nbgrvtx13starlem2  47974  gpg3nbgrvtx0  47978  cznnring  48124  elfzolborelfzop1  48382  zgtp1leeq  48384  mod0mul  48386  modn0mul  48387  m1modmmod  48388  difmodm1lt  48389  rege1logbzge0  48426  fllog2  48435  dignn0ldlem  48469  dignn0flhalflem1  48482  dignn0flhalflem2  48483