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

Theorem zre 10864
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 10862 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 460 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 972    = wceq 1379    e. wcel 1767   RRcr 9487   0cc0 9488   -ucneg 9802   NNcn 10532   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-neg 9804  df-z 10861
This theorem is referenced by:  zcn  10865  zrei  10866  zssre  10867  elnn0z  10873  elnnz1  10886  znnnlt1  10887  zletr  10903  znnsub  10905  znn0sub  10906  zltp1le  10908  zleltp1  10909  nn0ge0div  10926  zextle  10930  btwnnz  10933  suprzcl  10936  msqznn  10938  peano2uz2  10944  uzind  10948  uzindOLD  10951  fzind  10955  fnn0ind  10956  eluzuzle  11086  uzid  11092  uztrn  11094  uzneg  11096  uzss  11098  uztric  11099  uz11  11100  eluzp1m1  11101  eluzp1p1  11103  eluzaddi  11104  eluzsubi  11105  uzin  11110  uz3m2nn  11120  peano2uz  11130  nn0pzuz  11134  uzwo  11140  uzwoOLD  11141  eluz2b2  11150  uz2mulcl  11155  eqreznegel  11163  lbzbi  11166  uzsupss  11170  nn01to3  11171  zmin  11174  zmax  11175  zbtwnre  11176  rebtwnz  11177  qre  11183  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  z2ge  11393  qbtwnre  11394  elfz1eq  11693  fzn  11698  fzen  11699  uzsubsubfz  11703  fzaddel  11714  fzsuc2  11733  fzrev  11738  elfz1b  11744  fzm1  11754  fznuz  11756  uznfz  11757  elfz0fzfz0  11773  fz0fzelfz0  11774  fznn0sub2  11775  fz0fzdiffz0  11777  elfzmlbm  11778  elfzmlbp  11779  difelfznle  11782  elfzouz2  11806  fzonlt0  11812  fzossrbm1  11818  fzospliti  11821  fzo1fzo0n0  11828  elfzo0z  11829  fzofzim  11833  eluzgtdifelfzo  11842  fzossfzop1  11857  ssfzoulel  11870  ssfzo12bi  11871  elfzonelfzo  11876  elfzomelpfzo  11878  elfznelfzob  11880  fzosplitprm1  11883  fzostep1  11886  fllt  11907  flid  11908  flbi2  11916  flhalf  11925  dfceil2  11931  ceile  11939  ceilid  11941  quoremz  11945  intfracq  11949  uzsup  11953  zmod10  11975  zmodcl  11978  zmodfz  11980  modidmul0  11985  zmodid2  11987  modcyc  11994  modmul1  12003  modaddmodup  12013  modaddmodlo  12014  modaddmulmod  12016  leexp2  12182  zsqcl2  12207  iexpcyc  12234  brfi1uzind  12492  wrdsymb0  12534  ccatsymb  12559  swrdlend  12613  swrdnd  12614  swrd0  12615  swrdvalodm2  12621  swrdswrdlem  12641  swrdswrd  12642  swrdccatin2  12669  swrdccatin12lem2  12671  swrdccatin12lem3  12672  repswswrd  12713  cshwmodn  12723  cshwsublen  12724  cshwidxmod  12731  cshwidxm1  12734  repswcshw  12737  2cshw  12738  cshweqrep  12746  cshw1  12747  swrd2lsw  12847  nn0abscl  13102  rexuzre  13141  znnenlem  13799  dvdsval3  13844  moddvds  13847  absdvdsb  13856  dvdsabsb  13857  dvdsle  13883  alzdvds  13888  mulmoddvds  13896  divalgmod  13916  bitsp1o  13935  gcdabs  14023  gcdabs1  14024  modgcd  14026  bezoutlem1  14028  algcvga  14060  isprm3  14078  prmn2uzge3  14089  sqnprm  14091  zgcdsq  14138  hashdvds  14157  powm2modprm  14180  modprm0  14182  modprmn0modprm0  14184  fldivp1  14268  zgz  14303  4sqlem4  14322  cshwshashlem2  14432  gexdvds  16397  zringunit  18284  zrngunit  18285  prmirred  18289  prmirredOLD  18292  znf1o  18354  chfacfscmul0  19123  chfacfscmulgsum  19125  chfacfpmmul0  19127  chfacfpmmulgsum  19129  dyadf  21732  dyadovol  21734  degltlem1  22204  coskpi  22643  cosne0  22647  relogexp  22705  cxpeq  22856  ppival2  23127  ppival2g  23128  ppiprm  23150  chtprm  23152  chtnprm  23153  ppip1le  23160  efexple  23281  lgsdir2lem4  23326  lgsne0  23333  lgsquadlem1  23354  lgsquadlem2  23355  2sqlem2  23364  rplogsumlem2  23395  pntrsumbnd  23476  axlowdim  23937  clwlkisclwwlklem2fv2  24456  clwlkisclwwlklem2a  24458  clwwlkext2edg  24475  wwlksubclwwlk  24477  clwwisshclwwlem1  24478  usg2cwwkdifex  24494  clwlkfclwwlk  24517  extwwlkfablem2  24752  numclwwlkovf2ex  24760  numclwlk1lem2f1  24768  frgrareg  24791  frgraregord013  24792  gxnval  24935  gxmodid  24954  rezh  27585  zrhre  27630  hashf2  27727  ballotlemfc0  28068  ballotlemfcc  28069  elfzm12  28513  fzp1nel  28590  mblfinlem1  29626  mblfinlem2  29627  dvtanlem  29639  itg2addnclem2  29642  nn0prpwlem  29715  fzmul  29834  fzadd2  29835  incsequz2  29843  ellz1  30302  lzunuz  30303  lzenom  30305  nerabdioph  30344  pell14qrgt0  30397  rmxycomplete  30455  monotuz  30479  monotoddzzfi  30480  oddcomabszz  30482  zindbi  30484  jm2.24  30503  congrep  30513  fzneg  30522  jm2.19  30539  lcmabs  30811  oddfl  31036  climsuse  31150  stoweidlem26  31326  stoweidlem34  31334  fourierdlem11  31418  fourierdlem15  31422  fourierdlem20  31427  fourierdlem42  31449  fourierdlem51  31458  fourierdlem54  31461  fourierdlem64  31471  fourierdlem65  31472  fourierdlem76  31483  fourierdlem79  31486  fourierdlem94  31501  fourierdlem97  31504  fourierdlem103  31510  fourierdlem104  31511  fourierdlem113  31520  zm1nn  31794  eluzge0nn0  31798  elfz2z  31800  2elfz2melfz  31803  elfzlble  31805  elfzelfzlble  31806  el2fzo  31808  fsummmodsndifre  31816
  Copyright terms: Public domain W3C validator