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

Theorem zre 10949
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 10947 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 461 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 981    = wceq 1437    e. wcel 1872   RRcr 9546   0cc0 9547   -ucneg 9869   NNcn 10617   ZZcz 10945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-iota 5565  df-fv 5609  df-ov 6309  df-neg 9871  df-z 10946
This theorem is referenced by:  zcn  10950  zrei  10951  zssre  10952  elnn0z  10958  elnnz1  10971  znnnlt1  10972  zletr  10989  znnsub  10991  znn0sub  10992  zltp1le  10994  zleltp1  10995  nn0ge0div  11013  zextle  11017  btwnnz  11020  suprzcl  11023  msqznn  11025  peano2uz2  11031  uzind  11035  fzind  11041  fnn0ind  11042  eluzuzle  11175  uzid  11181  uzneg  11185  uztric  11188  uz11  11189  eluzp1m1  11190  eluzp1p1  11192  eluzaddi  11193  eluzsubi  11194  uzin  11199  uz3m2nn  11209  peano2uz  11220  nn0pzuz  11224  uzwo  11230  eluz2b2  11239  uz2mulcl  11244  uzinfi  11246  eqreznegel  11257  lbzbi  11260  uzsupss  11264  nn01to3  11265  zmin  11268  zmax  11269  zbtwnre  11270  rebtwnz  11271  qre  11277  rpnnen1lem1  11298  rpnnen1lem2  11299  rpnnen1lem3  11300  rpnnen1lem5  11302  z2ge  11499  qbtwnre  11500  elfz1eq  11818  fzn  11823  fzen  11824  uzsubsubfz  11829  fzaddel  11841  fzsuc2  11861  fzrev  11866  elfz1b  11872  fznuz  11884  uznfz  11885  fzp1nel  11886  elfz0fzfz0  11903  fz0fzelfz0  11904  fznn0sub2  11905  fz0fzdiffz0  11907  elfzmlbmOLD  11909  elfzmlbp  11910  difelfznle  11913  nelfzo  11933  elfzouz2  11942  fzo0n  11948  fzonlt0  11949  fzossrbm1  11955  fzospliti  11958  fzo1fzo0n0  11965  elfzo0z  11966  fzofzim  11970  eluzgtdifelfzo  11983  fzossfzop1  11998  ssfzoulel  12012  ssfzo12bi  12013  elfzonelfzo  12018  elfzomelpfzo  12020  elfznelfzob  12022  fzosplitprm1  12025  fzostep1  12028  fllt  12049  flid  12051  flbi2  12059  flhalf  12069  dfceil2  12075  ceile  12083  ceilid  12085  quoremz  12089  intfracq  12093  uzsup  12097  mulmod0  12111  zmod10  12120  zmodcl  12123  zmodfz  12125  modidmul0OLD  12130  zmodid2  12132  modcyc  12139  modmul1  12150  modaddmodup  12160  modaddmodlo  12161  modaddmulmod  12163  leexp2  12334  zsqcl2  12359  iexpcyc  12386  fi1uzind  12655  ccatsymb  12732  lswccatn0lsw  12739  swrdnd  12791  swrd0  12793  swrdswrdlem  12818  swrdswrd  12819  swrdccatin2  12846  swrdccatin12lem2  12848  swrdccatin12lem3  12849  repswswrd  12890  cshwmodn  12900  cshwsublen  12901  cshwidxmod  12908  cshwidxm1  12911  repswcshw  12914  2cshw  12915  cshweqrep  12923  cshw1  12924  swrd2lsw  13028  nn0abscl  13376  rexuzre  13416  znnenlem  14264  dvdsval3  14309  moddvds  14312  absdvdsb  14321  dvdsabsb  14322  dvdsle  14350  alzdvds  14355  mulmoddvds  14363  divalgmod  14387  bitsp1o  14406  gcdabs  14497  gcdabs1  14498  modgcd  14500  bezoutlem1  14503  algcvga  14538  lcmabs  14570  isprm3  14633  prmn2uzge3  14644  sqnprm  14646  zgcdsq  14702  hashdvds  14723  vfermltlALT  14753  powm2modprm  14754  modprm0  14756  modprmn0modprm0  14758  fldivp1  14842  zgz  14877  4sqlem4  14896  prmgaplem5  15025  prmgaplem7  15027  cshwshashlem2  15067  gexdvds  17235  zringunit  19061  prmirred  19065  znf1o  19121  chfacfscmul0  19881  chfacfscmulgsum  19883  chfacfpmmul0  19885  chfacfpmmulgsum  19887  dyadf  22548  dyadovol  22550  degltlem1  23020  coskpi  23474  cosne0  23478  relogexp  23544  cxpeq  23696  relogbzexp  23712  ppival2  24054  ppival2g  24055  ppiprm  24077  chtprm  24079  chtnprm  24080  ppip1le  24087  efexple  24208  lgsdir2lem4  24253  lgsne0  24260  lgsquadlem1  24281  lgsquadlem2  24282  2sqlem2  24291  rplogsumlem2  24322  pntrsumbnd  24403  axlowdim  24990  clwlkisclwwlklem2fv2  25510  clwlkisclwwlklem2a  25512  clwwlkext2edg  25529  wwlksubclwwlk  25531  clwwisshclwwlem1  25532  usg2cwwkdifex  25548  clwlkfclwwlk  25571  extwwlkfablem2  25805  numclwwlkovf2ex  25813  numclwlk1lem2f1  25821  frgrareg  25844  frgraregord013  25845  topnfbey  25905  gxnval  25987  gxmodid  26006  rezh  28784  zrhre  28832  hashf2  28914  ballotlemfc0  29334  ballotlemfcc  29335  elfzm12  30328  nn0prpwlem  30984  poimirlem24  31929  mblfinlem1  31942  mblfinlem2  31943  dvtanlemOLD  31956  itg2addnclem2  31959  fzmul  32034  fzadd2  32035  incsequz2  32043  ellz1  35579  lzunuz  35580  lzenom  35582  nerabdioph  35622  pell14qrgt0  35676  rmxycomplete  35736  monotuz  35760  monotoddzzfi  35761  oddcomabszz  35763  zindbi  35765  jm2.24  35784  congrep  35794  fzneg  35803  jm2.19  35819  oddfl  37442  fzdifsuc2  37485  climsuse  37628  stoweidlem26  37827  stoweidlem34  37836  fourierdlem20  37930  fourierdlem42  37953  fourierdlem42OLD  37954  fourierdlem51  37962  fourierdlem64  37975  fourierdlem76  37987  fourierdlem94  38005  fourierdlem97  38008  fourierdlem113  38024  zgeltp1eq  38588  smonoord  38589  fzopredsuc  38591  mod2eq1n2dvds  38596  elmod2OLD  38597  iccpartipre  38606  iccpartiltu  38607  iccpartigtl  38608  icceuelpartlem  38620  dfeven3  38658  dfodd4  38659  nn0o1gt2ALTV  38694  nnoALTV  38695  gbegt5  38733  gbogt5  38734  bgoldbwt  38749  nnsum3primesle9  38760  nnsum4primesodd  38762  nnsum4primesoddALTV  38763  evengpop3  38764  evengpoap3  38765  nnsum4primesevenALTV  38767  bgoldbtbndlem1  38771  bgoldbtbndlem2  38772  bgoldbtbndlem3  38773  bgoldbtbndlem4  38774  pfxccatin12lem2  38836  zm1nn  38904  eluzge0nn0  38908  elfz2z  38910  2elfz2melfz  38913  elfzlble  38915  elfzelfzlble  38916  fsummmodsndifre  38925  cznnring  39607  elfzolborelfzop1  39967  zgtp1leeq  39970  mod0mul  39973  modn0mul  39974  m1modmmod  39975  difmodm1lt  39976  rege1logbzge0  40021  fllog2  40030  dignn0ldlem  40064  dignn0flhalflem1  40077  dignn0flhalflem2  40078
  Copyright terms: Public domain W3C validator