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

Theorem zre 10638
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 10636 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 457 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 957    = wceq 1362    e. wcel 1755   RRcr 9269   0cc0 9270   -ucneg 9584   NNcn 10310   ZZcz 10634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9586  df-z 10635
This theorem is referenced by:  zcn  10639  zrei  10640  zssre  10641  elnn0z  10647  elnnz1  10660  znnnlt1  10661  zletr  10677  znnsub  10679  znn0sub  10680  zltp1le  10682  zleltp1  10683  nn0ge0div  10699  zextle  10703  btwnnz  10706  suprzcl  10709  msqznn  10711  peano2uz2  10717  uzind  10721  uzindOLD  10724  fzind  10728  fnn0ind  10729  uzletr  10857  uzid  10863  uztrn  10865  uzneg  10867  uzss  10869  uztric  10870  uz11  10871  eluzp1m1  10872  eluzp1p1  10874  eluzaddi  10875  eluzsubi  10876  uzin  10881  peano2uz  10896  uzwo  10905  uzwoOLD  10906  eluz2b2  10915  uz2mulcl  10920  eqreznegel  10928  lbzbi  10931  uzsupss  10935  zmin  10937  zmax  10938  zbtwnre  10939  rebtwnz  10940  qre  10946  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem5  10971  z2ge  11156  qbtwnre  11157  elfz1eq  11449  fzn  11453  fzen  11454  uzsubsubfz  11458  elfz0fzfz0  11472  fz0fzelfz0  11473  fznn0sub2  11475  fz0fzdiffz0  11476  elfzmlbm  11477  elfzmlbp  11478  fzaddel  11480  fzsuc2  11499  fzrev  11503  elfz1b  11511  fzm1  11524  fznuz  11526  uznfz  11527  elfzouz2  11550  fzonlt0  11556  fzospliti  11565  fzo1fzo0n0  11572  elfzo0z  11573  fzofzim  11577  fzossfzop1  11594  ssfzoulel  11605  ssfzo12bi  11606  elfzonelfzo  11611  elfzomelpfzo  11613  elfznelfzob  11615  fzostep1  11619  fllt  11640  flid  11641  flbi2  11649  flhalf  11658  dfceil2  11664  ceile  11672  ceilid  11674  quoremz  11678  intfracq  11682  uzsup  11686  zmod10  11708  zmodcl  11711  zmodfz  11713  modidmul0  11718  zmodid2  11720  modcyc  11727  modmul1  11736  modaddmodup  11746  modaddmodlo  11747  modaddmulmod  11749  leexp2  11902  zsqcl2  11927  iexpcyc  11954  brfi1uzind  12203  wrdsymb0  12243  ccatsymb  12265  swrdlend  12309  swrdnd  12310  swrd0  12311  swrdvalodm2  12317  swrdswrdlem  12337  swrdswrd  12338  swrdccatin2  12362  swrdccatin12lem2  12364  swrdccatin12lem3  12365  repswswrd  12406  cshwmodn  12416  cshwsublen  12417  cshwidxmod  12424  cshwidxm1  12427  repswcshw  12430  2cshw  12431  cshweqrep  12439  cshw1  12440  swrd2lsw  12536  nn0abscl  12785  rexuzre  12824  znnenlem  13477  dvdsval3  13522  moddvds  13525  absdvdsb  13534  dvdsabsb  13535  dvdsle  13561  alzdvds  13566  divalgmod  13593  bitsp1o  13612  gcdabs  13700  gcdabs1  13701  modgcd  13703  bezoutlem1  13705  algcvga  13737  isprm3  13755  sqnprm  13767  zgcdsq  13814  hashdvds  13833  modprm0  13856  modprmn0modprm0  13858  fldivp1  13942  zgz  13977  4sqlem4  13996  cshwshashlem2  14106  gexdvds  16063  zringunit  17756  zrngunit  17757  prmirred  17761  prmirredOLD  17764  znf1o  17826  dyadf  20913  dyadovol  20915  degltlem1  21428  coskpi  21867  cosne0  21871  relogexp  21929  cxpeq  22080  ppival2  22351  ppival2g  22352  ppiprm  22374  chtprm  22376  chtnprm  22377  ppip1le  22384  efexple  22505  lgsdir2lem4  22550  lgsne0  22557  lgsquadlem1  22578  lgsquadlem2  22579  2sqlem2  22588  rplogsumlem2  22619  pntrsumbnd  22700  axlowdim  23030  gxnval  23570  gxmodid  23589  rezh  26254  zrhre  26299  hashf2  26387  ballotlemfc0  26723  ballotlemfcc  26724  elfzm12  27167  fzp1nel  27244  mblfinlem1  28272  mblfinlem2  28273  dvtanlem  28285  itg2addnclem2  28288  nn0prpwlem  28361  fzmul  28480  fzadd2  28481  incsequz2  28489  ellz1  28950  lzunuz  28951  lzenom  28953  nerabdioph  28992  pell14qrgt0  29045  rmxycomplete  29103  monotuz  29127  monotoddzzfi  29128  oddcomabszz  29130  zindbi  29132  jm2.24  29151  congrep  29161  fzneg  29170  jm2.19  29187  climsuse  29627  stoweidlem26  29667  stoweidlem34  29675  nn01to3  30033  eluzge0nn0  30035  uzuzle  30036  uz3m2nn  30041  nn0pzuz  30042  elfz2z  30044  2elfz2melfz  30048  elfzlble  30054  elfzelfzlble  30055  el2fzo  30058  elfzom1elp1fzo  30064  eluzgtdifelfzo  30065  fzosplitprm1  30070  fsummmodsndifre  30085  mulmoddvds  30092  powm2modprm  30094  prmn2uzge3  30095  clwlkisclwwlklem2fv2  30291  clwlkisclwwlklem2a  30293  clwwlkext2edg  30310  wwlksubclwwlk  30312  zm1nn  30314  clwwisshclwwlem1  30315  difelfznle  30334  usg2cwwkdifex  30341  clwlkfclwwlk  30363  extwwlkfablem2  30517  numclwwlkovf2ex  30525  numclwlk1lem2f1  30533  frgrareg  30556  frgraregord013  30557
  Copyright terms: Public domain W3C validator