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

Theorem zre 10278
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 10276 . 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 1652    e. wcel 1725   RRcr 8981   0cc0 8982   -ucneg 9284   NNcn 9992   ZZcz 10274
This theorem is referenced by:  zcn  10279  zrei  10280  zssre  10281  elnn0z  10286  elnnz1  10299  znnnlt1  10300  znnsub  10314  znn0sub  10315  zltp1le  10317  zleltp1  10318  zextle  10335  btwnnz  10338  suprzcl  10341  msqznn  10343  peano2uz2  10349  uzind  10353  uzindOLD  10356  fzind  10360  fnn0ind  10361  uzid  10492  uztrn  10494  uzneg  10496  uzss  10498  uztric  10499  uz11  10500  eluzp1m1  10501  eluzp1p1  10503  eluzaddi  10504  eluzsubi  10505  uzin  10510  peano2uz  10522  uzwo  10531  uzwoOLD  10532  eluz2b2  10540  uz2mulcl  10545  eqreznegel  10553  lbzbi  10556  uzsupss  10560  zmin  10562  zmax  10563  zbtwnre  10564  rebtwnz  10565  qre  10571  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem5  10596  z2ge  10776  qbtwnre  10777  elfz1eq  11060  fzn  11063  fzen  11064  fznn0sub2  11078  fzaddel  11079  fzsuc2  11096  fzrev  11100  fzm1  11119  fznuz  11121  uznfz  11122  elfzouz2  11145  fzospliti  11157  elfznelfzob  11185  fzostep1  11189  fllt  11207  flid  11208  flbi2  11216  flhalf  11223  ceile  11227  quoremz  11228  intfracq  11232  uzsup  11236  zmod10  11256  zmodcl  11258  zmodfz  11260  modcyc  11268  modmul1  11271  leexp2  11426  zsqcl2  11451  iexpcyc  11477  brfi1uzind  11707  nn0abscl  12109  rexuzre  12148  znnenlem  12803  dvdsval3  12848  moddvds  12851  absdvdsb  12860  dvdsabsb  12861  dvdsle  12887  alzdvds  12891  divalgmod  12918  bitsp1o  12937  gcdabs  13025  gcdabs1  13026  modgcd  13028  bezoutlem1  13030  algcvga  13062  isprm3  13080  sqnprm  13090  zgcdsq  13137  hashdvds  13156  fldivp1  13258  zgz  13293  4sqlem4  13312  gexdvds  15210  zrngunit  16757  prmirred  16767  znf1o  16824  dyadf  19475  dyadovol  19477  degltlem1  19987  coskpi  20420  cosne0  20424  relogexp  20482  cxpeq  20633  ppival2  20903  ppival2g  20904  ppiprm  20926  chtprm  20928  chtnprm  20929  ppip1le  20936  efexple  21057  lgsdir2lem4  21102  lgsne0  21109  lgsquadlem1  21130  lgsquadlem2  21131  2sqlem2  21140  rplogsumlem2  21171  pntrsumbnd  21252  gxnval  21840  gxmodid  21859  rezh  24347  zrhre  24377  hashf2  24466  ballotlemfc0  24742  ballotlemfcc  24743  elfzm12  25104  zmodid2  25106  fzp1nel  25202  axlowdim  25892  mblfinlem  26234  itg2addnclem2  26247  nn0prpwlem  26316  fzmul  26435  fzadd2  26436  incsequz2  26444  ellz1  26816  lzunuz  26817  lzenom  26819  nerabdioph  26860  pell14qrgt0  26913  rmxycomplete  26971  monotuz  26995  monotoddzzfi  26996  oddcomabszz  26998  zindbi  27000  jm2.24  27019  congrep  27029  fzneg  27038  jm2.19  27055  climsuse  27701  stoweidlem26  27742  stoweidlem34  27750  elfz2z  28089  elfzmlbm  28090  elfzmlbp  28091  zletr  28092  elfz0fzfz0  28098  2elfz2melfz  28101  fz0fzelfz0  28102  fz0fzdiffz0  28103  ubmelfzo  28109  ubmelm1fzo  28110  fzo1fzo0n0  28111  elfzomelpfzo  28112  elfzonelfzo  28115  nn0ge0div  28120  modaddmulmod  28136  modidmul0  28138  wrdsymb0  28147  ccatsymb  28152  swrdltnd  28153  swrdnd  28154  swrdvalodmlem1  28159  swrdvalodm2  28160  swrdswrdlem  28164  swrdswrd  28165  swrdccatin2  28176  swrdccatin12lem3  28178  swrdccatin12lem4  28179  modprm0  28194  cshwidx  28208  2cshw1lem1  28214  2cshw1lem2  28215  2cshw2lem1  28218  2cshwmod  28223  cshweqdif2  28233  cshweqdif2s  28234  cshweqrep  28237  cshwssizelem4a  28246
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-neg 9286  df-z 10275
  Copyright terms: Public domain W3C validator