MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zre Structured version   Unicode version

Theorem zre 10941
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre  |-  ( N  e.  ZZ  ->  N  e.  RR )

Proof of Theorem zre
StepHypRef Expression
1 elz 10939 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 461 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 981    = wceq 1437    e. wcel 1870   RRcr 9537   0cc0 9538   -ucneg 9860   NNcn 10609   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-neg 9862  df-z 10938
This theorem is referenced by:  zcn  10942  zrei  10943  zssre  10944  elnn0z  10950  elnnz1  10963  znnnlt1  10964  zletr  10981  znnsub  10983  znn0sub  10984  zltp1le  10986  zleltp1  10987  nn0ge0div  11005  zextle  11009  btwnnz  11012  suprzcl  11015  msqznn  11017  peano2uz2  11023  uzind  11027  fzind  11033  fnn0ind  11034  eluzuzle  11167  uzid  11173  uzneg  11177  uztric  11180  uz11  11181  eluzp1m1  11182  eluzp1p1  11184  eluzaddi  11185  eluzsubi  11186  uzin  11191  uz3m2nn  11201  peano2uz  11212  nn0pzuz  11216  uzwo  11222  eluz2b2  11231  uz2mulcl  11236  uzinfi  11238  eqreznegel  11249  lbzbi  11252  uzsupss  11256  nn01to3  11257  zmin  11260  zmax  11261  zbtwnre  11262  rebtwnz  11263  qre  11269  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  z2ge  11491  qbtwnre  11492  elfz1eq  11808  fzn  11813  fzen  11814  uzsubsubfz  11819  fzaddel  11831  fzsuc2  11851  fzrev  11856  elfz1b  11862  fznuz  11874  uznfz  11875  fzp1nel  11876  elfz0fzfz0  11893  fz0fzelfz0  11894  fznn0sub2  11895  fz0fzdiffz0  11897  elfzmlbmOLD  11899  elfzmlbp  11900  difelfznle  11903  nelfzo  11923  elfzouz2  11932  fzo0n  11938  fzonlt0  11939  fzossrbm1  11945  fzospliti  11948  fzo1fzo0n0  11955  elfzo0z  11956  fzofzim  11960  eluzgtdifelfzo  11973  fzossfzop1  11988  ssfzoulel  12002  ssfzo12bi  12003  elfzonelfzo  12008  elfzomelpfzo  12010  elfznelfzob  12012  fzosplitprm1  12015  fzostep1  12018  fllt  12039  flid  12041  flbi2  12049  flhalf  12059  dfceil2  12065  ceile  12073  ceilid  12075  quoremz  12079  intfracq  12083  uzsup  12087  mulmod0  12101  zmod10  12110  zmodcl  12113  zmodfz  12115  modidmul0OLD  12120  zmodid2  12122  modcyc  12129  modmul1  12140  modaddmodup  12150  modaddmodlo  12151  modaddmulmod  12153  leexp2  12324  zsqcl2  12349  iexpcyc  12376  brfi1uzind  12641  ccatsymb  12714  lswccatn0lsw  12721  swrdnd  12773  swrd0  12775  swrdswrdlem  12800  swrdswrd  12801  swrdccatin2  12828  swrdccatin12lem2  12830  swrdccatin12lem3  12831  repswswrd  12872  cshwmodn  12882  cshwsublen  12883  cshwidxmod  12890  cshwidxm1  12893  repswcshw  12896  2cshw  12897  cshweqrep  12905  cshw1  12906  swrd2lsw  13006  nn0abscl  13354  rexuzre  13394  znnenlem  14242  dvdsval3  14287  moddvds  14290  absdvdsb  14299  dvdsabsb  14300  dvdsle  14328  alzdvds  14333  mulmoddvds  14341  divalgmod  14362  bitsp1o  14381  gcdabs  14471  gcdabs1  14472  modgcd  14474  bezoutlem1  14477  algcvga  14509  lcmabs  14541  isprm3  14604  prmn2uzge3  14615  sqnprm  14617  zgcdsq  14673  hashdvds  14692  vfermltlALT  14716  powm2modprm  14717  modprm0  14719  modprmn0modprm0  14721  fldivp1  14805  zgz  14840  4sqlem4  14859  prmgaplem5  14988  prmgaplem7  14990  cshwshashlem2  15030  gexdvds  17171  zringunit  18993  prmirred  18997  znf1o  19053  chfacfscmul0  19813  chfacfscmulgsum  19815  chfacfpmmul0  19817  chfacfpmmulgsum  19819  dyadf  22426  dyadovol  22428  degltlem1  22898  coskpi  23340  cosne0  23344  relogexp  23410  cxpeq  23562  relogbzexp  23578  ppival2  23918  ppival2g  23919  ppiprm  23941  chtprm  23943  chtnprm  23944  ppip1le  23951  efexple  24072  lgsdir2lem4  24117  lgsne0  24124  lgsquadlem1  24145  lgsquadlem2  24146  2sqlem2  24155  rplogsumlem2  24186  pntrsumbnd  24267  axlowdim  24837  clwlkisclwwlklem2fv2  25356  clwlkisclwwlklem2a  25358  clwwlkext2edg  25375  wwlksubclwwlk  25377  clwwisshclwwlem1  25378  usg2cwwkdifex  25394  clwlkfclwwlk  25417  extwwlkfablem2  25651  numclwwlkovf2ex  25659  numclwlk1lem2f1  25667  frgrareg  25690  frgraregord013  25691  topnfbey  25751  gxnval  25833  gxmodid  25852  rezh  28614  zrhre  28662  hashf2  28744  ballotlemfc0  29151  ballotlemfcc  29152  elfzm12  30107  nn0prpwlem  30763  poimirlem24  31668  mblfinlem1  31681  mblfinlem2  31682  dvtanlemOLD  31695  itg2addnclem2  31698  fzmul  31773  fzadd2  31774  incsequz2  31782  ellz1  35318  lzunuz  35319  lzenom  35321  nerabdioph  35361  pell14qrgt0  35413  rmxycomplete  35471  monotuz  35495  monotoddzzfi  35496  oddcomabszz  35498  zindbi  35500  jm2.24  35519  congrep  35529  fzneg  35538  jm2.19  35554  oddfl  37096  fzdifsuc2  37139  climsuse  37259  stoweidlem26  37455  stoweidlem34  37464  fourierdlem20  37558  fourierdlem42  37580  fourierdlem51  37589  fourierdlem64  37602  fourierdlem76  37614  fourierdlem94  37632  fourierdlem97  37635  fourierdlem113  37651  zgeltp1eq  38107  smonoord  38108  fzopredsuc  38110  mod2eq1n2dvds  38115  elmod2OLD  38116  iccpartipre  38125  iccpartiltu  38126  iccpartigtl  38127  icceuelpartlem  38139  dfeven3  38177  dfodd4  38178  nn0o1gt2ALTV  38213  nnoALTV  38214  gbegt5  38252  gbogt5  38253  bgoldbwt  38268  nnsum3primesle9  38279  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  evengpop3  38283  evengpoap3  38284  nnsum4primesevenALTV  38286  bgoldbtbndlem1  38290  bgoldbtbndlem2  38291  bgoldbtbndlem3  38292  bgoldbtbndlem4  38293  pfxccatin12lem2  38355  zm1nn  38398  eluzge0nn0  38402  elfz2z  38404  2elfz2melfz  38407  elfzlble  38409  elfzelfzlble  38410  fsummmodsndifre  38417  cznnring  38716  elfzolborelfzop1  39077  zgtp1leeq  39080  mod0mul  39083  modn0mul  39084  m1modmmod  39085  difmodm1lt  39086  rege1logbzge0  39131  fllog2  39140  dignn0ldlem  39174  dignn0flhalflem1  39187  dignn0flhalflem2  39188
  Copyright terms: Public domain W3C validator