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

Theorem zre 10030
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 10028 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 446 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 933    = wceq 1625    e. wcel 1686   RRcr 8738   0cc0 8739   -ucneg 9040   NNcn 9748   ZZcz 10026
This theorem is referenced by:  zcn  10031  zrei  10032  zssre  10033  elnn0z  10038  elnnz1  10051  znnnlt1  10052  znnsub  10066  znn0sub  10067  zltp1le  10069  zleltp1  10070  zextle  10087  btwnnz  10090  suprzcl  10093  msqznn  10095  peano2uz2  10101  uzind  10105  uzindOLD  10108  fzind  10112  fnn0ind  10113  uzid  10244  uztrn  10246  uzneg  10248  uzss  10250  uztric  10251  uz11  10252  eluzp1m1  10253  eluzp1p1  10255  eluzaddi  10256  eluzsubi  10257  uzin  10262  peano2uz  10274  uzwo  10283  uzwoOLD  10284  eluz2b2  10292  uz2mulcl  10297  eqreznegel  10305  lbzbi  10308  uzsupss  10312  zmin  10314  zmax  10315  zbtwnre  10316  rebtwnz  10317  qre  10323  rpnnen1lem1  10344  rpnnen1lem2  10345  rpnnen1lem3  10346  rpnnen1lem5  10348  z2ge  10527  qbtwnre  10528  elfz1eq  10809  fzn  10812  fzen  10813  fznn0sub2  10827  fzaddel  10828  fzsuc2  10844  fzrev  10848  fzm1  10864  fznuz  10866  uznfz  10867  elfzouz2  10890  fzospliti  10900  fzostep1  10924  fllt  10940  flid  10941  flbi2  10949  flhalf  10956  ceile  10960  quoremz  10961  intfracq  10965  uzsup  10969  zmod10  10989  zmodcl  10991  zmodfz  10993  modcyc  11001  modmul1  11004  leexp2  11158  zsqcl2  11183  iexpcyc  11209  nn0abscl  11799  rexuzre  11838  znnenlem  12492  dvdsval3  12537  moddvds  12540  absdvdsb  12549  dvdsabsb  12550  dvdsle  12576  alzdvds  12580  divalgmod  12607  bitsp1o  12626  gcdabs  12714  gcdabs1  12715  modgcd  12717  bezoutlem1  12719  algcvga  12751  isprm3  12769  sqnprm  12779  zgcdsq  12826  hashdvds  12845  fldivp1  12947  zgz  12982  4sqlem4  13001  gexdvds  14897  zrngunit  16440  prmirred  16450  znf1o  16507  dyadf  18948  dyadovol  18950  degltlem1  19460  coskpi  19890  cosne0  19894  relogexp  19951  cxpeq  20099  ppival2  20368  ppival2g  20369  ppiprm  20391  chtprm  20393  chtnprm  20394  ppip1le  20401  efexple  20522  lgsdir2lem4  20567  lgsne0  20574  lgsquadlem1  20595  lgsquadlem2  20596  2sqlem2  20605  rplogsumlem2  20636  pntrsumbnd  20717  gxnval  20929  gxmodid  20948  ballotlemfc0  23053  ballotlemfcc  23054  hashf2  23454  elfzm12  24010  zmodid2  24012  axlowdim  24591  itg2addnclem2  24934  nn0prpwlem  26249  fzmul  26454  fzadd2  26455  incsequz2  26470  ellz1  26857  lzunuz  26858  lzenom  26860  nerabdioph  26901  pell14qrgt0  26955  rmxycomplete  27013  monotuz  27037  monotoddzzfi  27038  oddcomabszz  27040  zindbi  27042  jm2.24  27061  congrep  27071  fzneg  27080  jm2.19  27097  fmul01  27721  fmul01lt1lem1  27725  fmul01lt1lem2  27726  climsuse  27745  stoweidlem3  27763  stoweidlem11  27771  stoweidlem20  27780  stoweidlem26  27786  stoweidlem34  27794  stoweidlem59  27819
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-neg 9042  df-z 10027
  Copyright terms: Public domain W3C validator