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

Theorem zre 10242
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 10240 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 447 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 935    = wceq 1649    e. wcel 1721   RRcr 8945   0cc0 8946   -ucneg 9248   NNcn 9956   ZZcz 10238
This theorem is referenced by:  zcn  10243  zrei  10244  zssre  10245  elnn0z  10250  elnnz1  10263  znnnlt1  10264  znnsub  10278  znn0sub  10279  zltp1le  10281  zleltp1  10282  zextle  10299  btwnnz  10302  suprzcl  10305  msqznn  10307  peano2uz2  10313  uzind  10317  uzindOLD  10320  fzind  10324  fnn0ind  10325  uzid  10456  uztrn  10458  uzneg  10460  uzss  10462  uztric  10463  uz11  10464  eluzp1m1  10465  eluzp1p1  10467  eluzaddi  10468  eluzsubi  10469  uzin  10474  peano2uz  10486  uzwo  10495  uzwoOLD  10496  eluz2b2  10504  uz2mulcl  10509  eqreznegel  10517  lbzbi  10520  uzsupss  10524  zmin  10526  zmax  10527  zbtwnre  10528  rebtwnz  10529  qre  10535  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  z2ge  10740  qbtwnre  10741  elfz1eq  11024  fzn  11027  fzen  11028  fznn0sub2  11042  fzaddel  11043  fzsuc2  11060  fzrev  11064  fzm1  11082  fznuz  11084  uznfz  11085  elfzouz2  11108  fzospliti  11120  elfznelfzob  11148  fzostep1  11152  fllt  11170  flid  11171  flbi2  11179  flhalf  11186  ceile  11190  quoremz  11191  intfracq  11195  uzsup  11199  zmod10  11219  zmodcl  11221  zmodfz  11223  modcyc  11231  modmul1  11234  leexp2  11389  zsqcl2  11414  iexpcyc  11440  brfi1uzind  11670  nn0abscl  12072  rexuzre  12111  znnenlem  12766  dvdsval3  12811  moddvds  12814  absdvdsb  12823  dvdsabsb  12824  dvdsle  12850  alzdvds  12854  divalgmod  12881  bitsp1o  12900  gcdabs  12988  gcdabs1  12989  modgcd  12991  bezoutlem1  12993  algcvga  13025  isprm3  13043  sqnprm  13053  zgcdsq  13100  hashdvds  13119  fldivp1  13221  zgz  13256  4sqlem4  13275  gexdvds  15173  zrngunit  16720  prmirred  16730  znf1o  16787  dyadf  19436  dyadovol  19438  degltlem1  19948  coskpi  20381  cosne0  20385  relogexp  20443  cxpeq  20594  ppival2  20864  ppival2g  20865  ppiprm  20887  chtprm  20889  chtnprm  20890  ppip1le  20897  efexple  21018  lgsdir2lem4  21063  lgsne0  21070  lgsquadlem1  21091  lgsquadlem2  21092  2sqlem2  21101  rplogsumlem2  21132  pntrsumbnd  21213  gxnval  21801  gxmodid  21820  rezh  24308  zrhre  24338  hashf2  24427  ballotlemfc0  24703  ballotlemfcc  24704  elfzm12  25065  zmodid2  25067  fzp1nel  25163  axlowdim  25804  mblfinlem  26143  itg2addnclem2  26156  nn0prpwlem  26215  fzmul  26334  fzadd2  26335  incsequz2  26343  ellz1  26715  lzunuz  26716  lzenom  26718  nerabdioph  26759  pell14qrgt0  26812  rmxycomplete  26870  monotuz  26894  monotoddzzfi  26895  oddcomabszz  26897  zindbi  26899  jm2.24  26918  congrep  26928  fzneg  26937  jm2.19  26954  climsuse  27601  stoweidlem26  27642  stoweidlem34  27650  elfzmlbm  27977  elfzmlbp  27978  zletr  27980  ubmelfzo  27986  ubmelm1fzo  27987  fzo1fzo0n0  27988  elfzomelpfzo  27989  elfzonelfzo  27992  swrdltnd  28000  swrdnd  28001  swrdswrdlem  28010  swrdswrd  28011  swrdccatin2  28018  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3b  28031
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250  df-z 10239
  Copyright terms: Public domain W3C validator