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

Theorem zre 10875
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 10873 . 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 973    = wceq 1383    e. wcel 1804   RRcr 9494   0cc0 9495   -ucneg 9811   NNcn 10543   ZZcz 10871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-neg 9813  df-z 10872
This theorem is referenced by:  zcn  10876  zrei  10877  zssre  10878  elnn0z  10884  elnnz1  10897  znnnlt1  10898  zletr  10915  znnsub  10917  znn0sub  10918  zltp1le  10920  zleltp1  10921  nn0ge0div  10939  zextle  10943  btwnnz  10946  suprzcl  10949  msqznn  10951  peano2uz2  10957  uzind  10961  uzindOLD  10964  fzind  10969  fnn0ind  10970  eluzuzle  11100  uzid  11106  uzneg  11110  uztric  11113  uz11  11114  eluzp1m1  11115  eluzp1p1  11117  eluzaddi  11118  eluzsubi  11119  uzin  11124  uz3m2nn  11134  peano2uz  11145  nn0pzuz  11149  uzwo  11155  uzwoOLD  11156  eluz2b2  11165  uz2mulcl  11170  eqreznegel  11178  lbzbi  11181  uzsupss  11185  nn01to3  11186  zmin  11189  zmax  11190  zbtwnre  11191  rebtwnz  11192  qre  11198  rpnnen1lem1  11219  rpnnen1lem2  11220  rpnnen1lem3  11221  rpnnen1lem5  11223  z2ge  11408  qbtwnre  11409  elfz1eq  11708  fzn  11713  fzen  11714  uzsubsubfz  11718  fzaddel  11729  fzsuc2  11748  fzrev  11753  elfz1b  11759  fzm1  11769  fznuz  11771  uznfz  11772  fzp1nel  11773  elfz0fzfz0  11790  fz0fzelfz0  11791  fznn0sub2  11792  fz0fzdiffz0  11794  elfzmlbmOLD  11796  elfzmlbp  11797  difelfznle  11800  elfzouz2  11824  fzonlt0  11830  fzossrbm1  11836  fzospliti  11839  fzo1fzo0n0  11846  elfzo0z  11847  fzofzim  11851  eluzgtdifelfzo  11860  fzossfzop1  11875  ssfzoulel  11888  ssfzo12bi  11889  elfzonelfzo  11894  elfzomelpfzo  11896  elfznelfzob  11898  fzosplitprm1  11901  fzostep1  11904  fllt  11925  flid  11927  flbi2  11935  flhalf  11944  dfceil2  11950  ceile  11958  ceilid  11960  quoremz  11964  intfracq  11968  uzsup  11972  zmod10  11994  zmodcl  11997  zmodfz  11999  modidmul0  12004  zmodid2  12006  modcyc  12013  modmul1  12022  modaddmodup  12032  modaddmodlo  12033  modaddmulmod  12035  leexp2  12202  zsqcl2  12227  iexpcyc  12254  brfi1uzind  12514  wrdsymb0  12557  ccatsymb  12582  swrdlend  12638  swrdnd  12639  swrd0  12640  swrdvalodm2  12646  swrdswrdlem  12666  swrdswrd  12667  swrdccatin2  12694  swrdccatin12lem2  12696  swrdccatin12lem3  12697  repswswrd  12738  cshwmodn  12748  cshwsublen  12749  cshwidxmod  12756  cshwidxm1  12759  repswcshw  12762  2cshw  12763  cshweqrep  12771  cshw1  12772  swrd2lsw  12872  nn0abscl  13127  rexuzre  13167  znnenlem  13927  dvdsval3  13972  moddvds  13975  absdvdsb  13984  dvdsabsb  13985  dvdsle  14013  alzdvds  14018  mulmoddvds  14026  divalgmod  14046  bitsp1o  14065  gcdabs  14153  gcdabs1  14154  modgcd  14156  bezoutlem1  14158  algcvga  14190  isprm3  14208  prmn2uzge3  14219  sqnprm  14221  zgcdsq  14268  hashdvds  14287  powm2modprm  14310  modprm0  14312  modprmn0modprm0  14314  fldivp1  14398  zgz  14433  4sqlem4  14452  cshwshashlem2  14563  gexdvds  16583  zringunit  18498  zrngunit  18499  prmirred  18503  prmirredOLD  18506  znf1o  18568  chfacfscmul0  19337  chfacfscmulgsum  19339  chfacfpmmul0  19341  chfacfpmmulgsum  19343  dyadf  21978  dyadovol  21980  degltlem1  22450  coskpi  22891  cosne0  22895  relogexp  22958  cxpeq  23109  ppival2  23380  ppival2g  23381  ppiprm  23403  chtprm  23405  chtnprm  23406  ppip1le  23413  efexple  23534  lgsdir2lem4  23579  lgsne0  23586  lgsquadlem1  23607  lgsquadlem2  23608  2sqlem2  23617  rplogsumlem2  23648  pntrsumbnd  23729  axlowdim  24242  clwlkisclwwlklem2fv2  24761  clwlkisclwwlklem2a  24763  clwwlkext2edg  24780  wwlksubclwwlk  24782  clwwisshclwwlem1  24783  usg2cwwkdifex  24799  clwlkfclwwlk  24822  extwwlkfablem2  25056  numclwwlkovf2ex  25064  numclwlk1lem2f1  25072  frgrareg  25095  frgraregord013  25096  gxnval  25240  gxmodid  25259  rezh  27930  zrhre  27975  hashf2  28068  ballotlemfc0  28409  ballotlemfcc  28410  elfzm12  29019  mblfinlem1  30027  mblfinlem2  30028  dvtanlem  30040  itg2addnclem2  30043  nn0prpwlem  30116  fzmul  30209  fzadd2  30210  incsequz2  30218  ellz1  30676  lzunuz  30677  lzenom  30679  nerabdioph  30718  pell14qrgt0  30771  rmxycomplete  30829  monotuz  30853  monotoddzzfi  30854  oddcomabszz  30856  zindbi  30858  jm2.24  30877  congrep  30887  fzneg  30896  jm2.19  30911  lcmabs  31187  oddfl  31413  fzdifsuc2  31466  climsuse  31568  stoweidlem26  31762  stoweidlem34  31770  fourierdlem20  31863  fourierdlem42  31885  fourierdlem51  31894  fourierdlem64  31907  fourierdlem76  31919  fourierdlem94  31937  fourierdlem97  31940  fourierdlem113  31956  zm1nn  32279  eluzge0nn0  32283  elfz2z  32285  2elfz2melfz  32288  elfzlble  32290  elfzelfzlble  32291  el2fzo  32293  fsummmodsndifre  32301  cznnring  32591
  Copyright terms: Public domain W3C validator