Theorem zre 12558

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

Syntax hints:   → wi 4   ∨ w3o 1094   = wceq 1550   ∈ wcel 2132  ℝcr 11058  0cc0 11059  -cneg 11401  ℕcn 12196  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384  df-neg 11403  df-z 12555

This theorem is referenced by:  zcn  12559  zrei  12560  zssre  12561  elnn0z  12567  elnnz1  12583  znnnlt1  12584  zletr  12601  znnsub  12603  znn0sub  12604  nzadd  12605  zltp1le  12607  zleltp1  12608  nn0ge0div  12628  zextle  12632  btwnnz  12635  suprzcl  12639  msqznn  12641  peano2uz2  12647  uzind  12651  fzind  12657  fnn0ind  12658  eluzuzle  12834  uzid  12840  uzneg  12845  uztric  12849  uz11  12850  eluzp1m1  12851  eluzp1p1  12853  eluzadd  12854  eluzsub  12855  subeluzsub  12858  uzin  12861  uz3m2nn  12881  peano2uz  12888  nn0pzuz  12892  uzwo  12898  eluz2b2  12908  uz2mulcl  12913  uzinfi  12915  eqreznegel  12921  lbzbi  12923  uzsupss  12927  nn01to3  12928  zmin  12931  zmax  12932  zbtwnre  12933  rebtwnz  12934  qre  12940  elpq  12962  rpnnen1lem2  12964  rpnnen1lem1  12965  rpnnen1lem3  12966  rpnnen1lem5  12968  z2ge  13187  qbtwnre  13188  zltaddlt1le  13495  elfz1eq  13526  fzn  13531  fzen  13532  uzsubsubfz  13537  fzaddel  13549  fzadd2  13550  ssfzunsnext  13560  ssfzunsn  13561  fzsuc2  13573  fzrev  13578  elfz1b  13584  fznuz  13600  uznfz  13601  fzp1nel  13602  elfz0fzfz0  13624  fz0fzelfz0  13625  fznn0sub2  13626  fz0fzdiffz0  13628  elfzmlbp  13630  difelfznle  13633  nelfzo  13656  elfzouz2  13666  fzo0n  13673  fzonlt0  13674  fzossrbm1  13680  fzospliti  13683  elfzo0z  13693  fzofzim  13701  fzo1fzo0n0  13707  eluzgtdifelfzo  13719  fzossfzop1  13735  ssfzoulel  13752  ssfzo12bi  13753  elfzonelfzo  13761  elfzomelpfzo  13764  elfznelfzob  13766  fzostep1  13778  fllt  13802  flid  13804  flbi2  13813  2tnp1ge0ge0  13825  flhalf  13826  fldiv4p1lem1div2  13831  fldiv4lem1div2uz2  13832  dfceil2  13835  ceile  13845  ceilid  13847  quoremz  13851  intfracq  13855  uzsup  13859  mulmod0  13873  zmod10  13883  zmodcl  13887  zmodfz  13889  zmodid2  13895  modcyc  13902  modaddid  13906  mulp1mod1  13910  muladdmod  13911  modmuladd  13912  modmuladdim  13913  modmul1  13923  modaddmodup  13933  modaddmodlo  13934  modaddmulmod  13937  zsqcl2  14137  leexp2  14170  iexpcyc  14206  fi1uzind  14506  ccatsymb  14582  ccatval21sw  14585  lswccatn0lsw  14591  swrdnd  14654  swrdnnn0nd  14656  swrd0  14658  swrdswrdlem  14703  swrdswrd  14704  swrdccatin2  14728  pfxccatin12lem2  14730  pfxccatin12lem3  14731  repswswrd  14783  cshwmodn  14794  cshwsublen  14795  cshwidxmod  14802  cshwidxmodr  14803  cshwidxm1  14806  repswcshw  14811  2cshw  14812  cshweqrep  14820  cshw1  14821  swrd2lsw  14951  nn0abscl  15311  rexuzre  15352  dvdsval3  16262  p1modz1  16265  moddvds  16269  absdvdsb  16280  dvdsabsb  16281  dvdsle  16316  alzdvds  16326  mod2eq1n2dvds  16353  evennn02n  16356  evennn2n  16357  ltoddhalfle  16367  divalgmod  16412  fldivndvdslt  16422  flodddiv4t2lthalf  16424  bitsp1o  16439  gcdabs1  16535  modgcd  16538  bezoutlem1  16545  dfgcd2  16552  algcvga  16585  lcmabs  16611  isprm3  16689  dvdsnprmd  16696  2mulprm  16699  oddprmgt2  16706  sqnprm  16709  zgcdsq  16760  hashdvds  16782  vfermltlALT  16810  powm2modprm  16811  modprm0  16813  modprmn0modprm0  16815  fldivp1  16905  zgz  16941  4sqlem4  16960  prmgaplem5  17063  prmgaplem7  17065  cshwshashlem2  17104  setsstruct  17184  mulgmodid  19127  gexdvds  19596  zringunit  21487  prmirred  21495  znf1o  21572  chfacfscmul0  22887  chfacfscmulgsum  22889  chfacfpmmul0  22891  chfacfpmmulgsum  22893  dyadf  25622  dyadovol  25624  degltlem1  26101  coskpi  26554  cosne0  26560  relogexp  26627  cxpeq  26788  relogbzexp  26807  ppival2  27158  ppival2g  27159  ppiprm  27181  chtprm  27183  chtnprm  27184  ppip1le  27191  efexple  27311  zabsle1  27326  lgsdir2lem4  27358  lgsne0  27365  gausslemma2dlem1a  27395  gausslemma2dlem3  27398  gausslemma2dlem4  27399  lgsquadlem1  27410  lgsquadlem2  27411  2lgslem1a1  27419  2lgslem1a2  27420  2sqlem2  27448  rplogsumlem2  27515  pntrsumbnd  27596  axlowdim  29097  crctcshwlkn0lem3  29947  crctcshwlkn0lem5  29949  crctcshwlkn0  29956  crctcsh  29959  clwlkclwwlklem2fv2  30133  clwlkclwwlklem2a  30135  clwwisshclwwslemlem  30150  clwwlkinwwlk  30177  clwwlkext2edg  30193  wwlksubclwwlk  30195  numclwwlk5  30525  topnfbey  30606  uzssico  32925  1fldgenq  33455  znfermltl  33498  ply1coedeg  33729  rezh  34210  zrhre  34260  hashf2  34325  ballotlemfc0  34734  ballotlemfcc  34735  chpvalz  34869  chtvalz  34870  zltp1ne  35398  0nn0m1nnn0  35401  elfzm12  35963  nn0prpwlem  36620  poimirlem24  38081  mblfinlem1  38094  mblfinlem2  38095  itg2addnclem2  38109  fzmul  38178  incsequz2  38186  fimgmcyc  43090  ellz1  43286  lzunuz  43287  lzenom  43289  nerabdioph  43324  pell14qrgt0  43374  rmxycomplete  43432  monotuz  43456  monotoddzzfi  43457  oddcomabszz  43459  zindbi  43461  jm2.24  43478  congrep  43488  fzneg  43497  jm2.19  43508  fzunt  43969  fzunt1d  43971  fzuntgd  43972  oddfl  45795  fzdifsuc2  45827  climsuse  46122  stoweidlem26  46538  stoweidlem34  46546  fourierdlem20  46639  fourierdlem42  46661  fourierdlem51  46669  fourierdlem64  46682  fourierdlem76  46694  fourierdlem94  46712  fourierdlem97  46715  fourierdlem113  46731  natlocalincr  47390  natglobalincr  47391  zm1nn  47834  zgeltp1eq  47841  eluzge0nn0  47844  elfz2z  47847  2elfz2melfz  47850  elfzlble  47852  elfzelfzlble  47853  fzopredsuc  47856  ceilbi  47869  mod0mul  47894  modn0mul  47895  m1modmmod  47896  difmodm1lt  47897  mod2addne  47902  modm2nep1  47904  modp2nep1  47905  modm1nep2  47906  modm1nem2  47907  modm1p1ne  47908  smonoord  47909  2timesltsqm1  47911  fsummmodsndifre  47914  muldvdsfacgt  47918  muldvdsfacm1  47919  iccpartipre  47965  iccpartiltu  47966  iccpartigtl  47967  icceuelpartlem  47979  fmtno4prmfac  48119  lighneallem4b  48156  nprmdvdsfacm1lem2  48168  nprmdvdsfacm1lem4  48170  dfeven3  48218  dfodd4  48219  nn0o1gt2ALTV  48254  nnoALTV  48255  fpprel2  48301  gbegt5  48321  gbowgt5  48322  sbgoldbwt  48337  nnsum3primesle9  48354  nnsum4primesodd  48356  nnsum4primesoddALTV  48357  evengpop3  48358  evengpoap3  48359  nnsum4primesevenALTV  48361  bgoldbtbndlem1  48365  bgoldbtbndlem2  48366  bgoldbtbndlem3  48367  bgoldbtbndlem4  48368  gpgprismgriedgdmss  48612  gpgusgralem  48616  gpgedgvtx1  48622  gpg5nbgrvtx03starlem2  48629  gpg5nbgrvtx13starlem2  48632  gpg3nbgrvtx0  48636  cznnring  48822  elfzolborelfzop1  49079  zgtp1leeq  49081  rege1logbzge0  49119  fllog2  49128  dignn0ldlem  49162  dignn0flhalflem1  49175  dignn0flhalflem2  49176