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

Theorem zre 10642
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 10640 . 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 964    = wceq 1369    e. wcel 1756   RRcr 9273   0cc0 9274   -ucneg 9588   NNcn 10314   ZZcz 10638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639
This theorem is referenced by:  zcn  10643  zrei  10644  zssre  10645  elnn0z  10651  elnnz1  10664  znnnlt1  10665  zletr  10681  znnsub  10683  znn0sub  10684  zltp1le  10686  zleltp1  10687  nn0ge0div  10703  zextle  10707  btwnnz  10710  suprzcl  10713  msqznn  10715  peano2uz2  10721  uzind  10725  uzindOLD  10728  fzind  10732  fnn0ind  10733  uzletr  10861  uzid  10867  uztrn  10869  uzneg  10871  uzss  10873  uztric  10874  uz11  10875  eluzp1m1  10876  eluzp1p1  10878  eluzaddi  10879  eluzsubi  10880  uzin  10885  peano2uz  10900  uzwo  10909  uzwoOLD  10910  eluz2b2  10919  uz2mulcl  10924  eqreznegel  10932  lbzbi  10935  uzsupss  10939  zmin  10941  zmax  10942  zbtwnre  10943  rebtwnz  10944  qre  10950  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  z2ge  11160  qbtwnre  11161  elfz1eq  11454  fzn  11458  fzen  11459  uzsubsubfz  11463  elfz0fzfz0  11477  fz0fzelfz0  11478  fznn0sub2  11480  fz0fzdiffz0  11481  elfzmlbm  11482  elfzmlbp  11483  fzaddel  11485  fzsuc2  11506  fzrev  11511  elfz1b  11519  fzm1  11532  fznuz  11534  uznfz  11535  elfzouz2  11558  fzonlt0  11564  fzospliti  11573  fzo1fzo0n0  11580  elfzo0z  11581  fzofzim  11585  fzossfzop1  11602  ssfzoulel  11613  ssfzo12bi  11614  elfzonelfzo  11619  elfzomelpfzo  11621  elfznelfzob  11623  fzostep1  11627  fllt  11648  flid  11649  flbi2  11657  flhalf  11666  dfceil2  11672  ceile  11680  ceilid  11682  quoremz  11686  intfracq  11690  uzsup  11694  zmod10  11716  zmodcl  11719  zmodfz  11721  modidmul0  11726  zmodid2  11728  modcyc  11735  modmul1  11744  modaddmodup  11754  modaddmodlo  11755  modaddmulmod  11757  leexp2  11910  zsqcl2  11935  iexpcyc  11962  brfi1uzind  12211  wrdsymb0  12251  ccatsymb  12273  swrdlend  12317  swrdnd  12318  swrd0  12319  swrdvalodm2  12325  swrdswrdlem  12345  swrdswrd  12346  swrdccatin2  12370  swrdccatin12lem2  12372  swrdccatin12lem3  12373  repswswrd  12414  cshwmodn  12424  cshwsublen  12425  cshwidxmod  12432  cshwidxm1  12435  repswcshw  12438  2cshw  12439  cshweqrep  12447  cshw1  12448  swrd2lsw  12544  nn0abscl  12793  rexuzre  12832  znnenlem  13486  dvdsval3  13531  moddvds  13534  absdvdsb  13543  dvdsabsb  13544  dvdsle  13570  alzdvds  13575  divalgmod  13602  bitsp1o  13621  gcdabs  13709  gcdabs1  13710  modgcd  13712  bezoutlem1  13714  algcvga  13746  isprm3  13764  sqnprm  13776  zgcdsq  13823  hashdvds  13842  modprm0  13865  modprmn0modprm0  13867  fldivp1  13951  zgz  13986  4sqlem4  14005  cshwshashlem2  14115  gexdvds  16074  zringunit  17889  zrngunit  17890  prmirred  17894  prmirredOLD  17897  znf1o  17959  dyadf  21046  dyadovol  21048  degltlem1  21518  coskpi  21957  cosne0  21961  relogexp  22019  cxpeq  22170  ppival2  22441  ppival2g  22442  ppiprm  22464  chtprm  22466  chtnprm  22467  ppip1le  22474  efexple  22595  lgsdir2lem4  22640  lgsne0  22647  lgsquadlem1  22668  lgsquadlem2  22669  2sqlem2  22678  rplogsumlem2  22709  pntrsumbnd  22790  axlowdim  23158  gxnval  23698  gxmodid  23717  rezh  26352  zrhre  26397  hashf2  26485  ballotlemfc0  26827  ballotlemfcc  26828  elfzm12  27271  fzp1nel  27348  mblfinlem1  28381  mblfinlem2  28382  dvtanlem  28394  itg2addnclem2  28397  nn0prpwlem  28470  fzmul  28589  fzadd2  28590  incsequz2  28598  ellz1  29058  lzunuz  29059  lzenom  29061  nerabdioph  29100  pell14qrgt0  29153  rmxycomplete  29211  monotuz  29235  monotoddzzfi  29236  oddcomabszz  29238  zindbi  29240  jm2.24  29259  congrep  29269  fzneg  29278  jm2.19  29295  climsuse  29734  stoweidlem26  29774  stoweidlem34  29782  nn01to3  30140  eluzge0nn0  30142  uzuzle  30143  uz3m2nn  30148  nn0pzuz  30149  elfz2z  30151  2elfz2melfz  30155  elfzlble  30161  elfzelfzlble  30162  el2fzo  30165  elfzom1elp1fzo  30171  eluzgtdifelfzo  30172  fzosplitprm1  30177  fsummmodsndifre  30192  mulmoddvds  30199  powm2modprm  30201  prmn2uzge3  30202  clwlkisclwwlklem2fv2  30398  clwlkisclwwlklem2a  30400  clwwlkext2edg  30417  wwlksubclwwlk  30419  zm1nn  30421  clwwisshclwwlem1  30422  difelfznle  30441  usg2cwwkdifex  30448  clwlkfclwwlk  30470  extwwlkfablem2  30624  numclwwlkovf2ex  30632  numclwlk1lem2f1  30640  frgrareg  30663  frgraregord013  30664
  Copyright terms: Public domain W3C validator