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

Theorem zre 10803
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 10801 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 458 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 970    = wceq 1399    e. wcel 1836   RRcr 9420   0cc0 9421   -ucneg 9737   NNcn 10470   ZZcz 10799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rex 2748  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-iota 5473  df-fv 5517  df-ov 6217  df-neg 9739  df-z 10800
This theorem is referenced by:  zcn  10804  zrei  10805  zssre  10806  elnn0z  10812  elnnz1  10825  znnnlt1  10826  zletr  10843  znnsub  10845  znn0sub  10846  zltp1le  10848  zleltp1  10849  nn0ge0div  10867  zextle  10871  btwnnz  10874  suprzcl  10877  msqznn  10879  peano2uz2  10885  uzind  10889  fzind  10895  fnn0ind  10896  eluzuzle  11027  uzid  11033  uzneg  11037  uztric  11040  uz11  11041  eluzp1m1  11042  eluzp1p1  11044  eluzaddi  11045  eluzsubi  11046  uzin  11051  uz3m2nn  11061  peano2uz  11072  nn0pzuz  11076  uzwo  11082  eluz2b2  11091  uz2mulcl  11096  eqreznegel  11104  lbzbi  11107  uzsupss  11111  nn01to3  11112  zmin  11115  zmax  11116  zbtwnre  11117  rebtwnz  11118  qre  11124  rpnnen1lem1  11145  rpnnen1lem2  11146  rpnnen1lem3  11147  rpnnen1lem5  11149  z2ge  11336  qbtwnre  11337  elfz1eq  11636  fzn  11641  fzen  11642  uzsubsubfz  11646  fzaddel  11658  fzsuc2  11677  fzrev  11682  elfz1b  11688  fznuz  11700  uznfz  11701  fzp1nel  11702  elfz0fzfz0  11719  fz0fzelfz0  11720  fznn0sub2  11721  fz0fzdiffz0  11723  elfzmlbmOLD  11725  elfzmlbp  11726  difelfznle  11729  nelfzo  11745  elfzouz2  11754  fzo0n  11760  fzonlt0  11761  fzossrbm1  11767  fzospliti  11770  fzo1fzo0n0  11777  elfzo0z  11778  fzofzim  11782  eluzgtdifelfzo  11795  fzossfzop1  11810  ssfzoulel  11824  ssfzo12bi  11825  elfzonelfzo  11830  elfzomelpfzo  11832  elfznelfzob  11834  fzosplitprm1  11837  fzostep1  11840  fllt  11861  flid  11863  flbi2  11871  flhalf  11881  dfceil2  11887  ceile  11895  ceilid  11897  quoremz  11901  intfracq  11905  uzsup  11909  mulmod0  11923  zmod10  11932  zmodcl  11935  zmodfz  11937  modidmul0OLD  11942  zmodid2  11944  modcyc  11951  modmul1  11962  modaddmodup  11972  modaddmodlo  11973  modaddmulmod  11975  leexp2  12142  zsqcl2  12167  iexpcyc  12194  brfi1uzind  12455  ccatsymb  12528  lswccatn0lsw  12535  swrdnd  12587  swrd0  12589  swrdswrdlem  12614  swrdswrd  12615  swrdccatin2  12642  swrdccatin12lem2  12644  swrdccatin12lem3  12645  repswswrd  12686  cshwmodn  12696  cshwsublen  12697  cshwidxmod  12704  cshwidxm1  12707  repswcshw  12710  2cshw  12711  cshweqrep  12719  cshw1  12720  swrd2lsw  12820  nn0abscl  13166  rexuzre  13206  znnenlem  13966  dvdsval3  14011  moddvds  14014  absdvdsb  14023  dvdsabsb  14024  dvdsle  14052  alzdvds  14057  mulmoddvds  14065  divalgmod  14085  bitsp1o  14104  gcdabs  14192  gcdabs1  14193  modgcd  14195  bezoutlem1  14197  algcvga  14229  isprm3  14247  prmn2uzge3  14258  sqnprm  14260  zgcdsq  14307  hashdvds  14326  powm2modprm  14349  modprm0  14351  modprmn0modprm0  14353  fldivp1  14437  zgz  14472  4sqlem4  14491  cshwshashlem2  14602  gexdvds  16740  zringunit  18640  prmirred  18644  znf1o  18700  chfacfscmul0  19463  chfacfscmulgsum  19465  chfacfpmmul0  19467  chfacfpmmulgsum  19469  dyadf  22104  dyadovol  22106  degltlem1  22576  coskpi  23017  cosne0  23021  relogexp  23087  cxpeq  23237  relogbzexp  23253  ppival2  23538  ppival2g  23539  ppiprm  23561  chtprm  23563  chtnprm  23564  ppip1le  23571  efexple  23692  lgsdir2lem4  23737  lgsne0  23744  lgsquadlem1  23765  lgsquadlem2  23766  2sqlem2  23775  rplogsumlem2  23806  pntrsumbnd  23887  axlowdim  24406  clwlkisclwwlklem2fv2  24925  clwlkisclwwlklem2a  24927  clwwlkext2edg  24944  wwlksubclwwlk  24946  clwwisshclwwlem1  24947  usg2cwwkdifex  24963  clwlkfclwwlk  24986  extwwlkfablem2  25220  numclwwlkovf2ex  25228  numclwlk1lem2f1  25236  frgrareg  25259  frgraregord013  25260  gxnval  25400  gxmodid  25419  rezh  28136  zrhre  28181  hashf2  28263  ballotlemfc0  28650  ballotlemfcc  28651  elfzm12  29266  mblfinlem1  30252  mblfinlem2  30253  dvtanlemOLD  30266  itg2addnclem2  30269  nn0prpwlem  30342  fzmul  30435  fzadd2  30436  incsequz2  30444  ellz1  30901  lzunuz  30902  lzenom  30904  nerabdioph  30944  pell14qrgt0  30996  rmxycomplete  31054  monotuz  31078  monotoddzzfi  31079  oddcomabszz  31081  zindbi  31083  jm2.24  31102  congrep  31112  fzneg  31121  jm2.19  31137  lcmabs  31415  oddfl  31661  fzdifsuc2  31713  climsuse  31815  stoweidlem26  32009  stoweidlem34  32017  fourierdlem20  32110  fourierdlem42  32132  fourierdlem51  32141  fourierdlem64  32154  fourierdlem76  32166  fourierdlem94  32184  fourierdlem97  32187  fourierdlem113  32203  mod2eq1n2dvds  32497  elmod2OLD  32498  dfeven3  32535  dfodd4  32536  nn0o1gt2ALTV  32571  nnoALTV  32572  pfxccatin12lem2  32634  zm1nn  32681  eluzge0nn0  32685  elfz2z  32687  2elfz2melfz  32690  elfzlble  32692  elfzelfzlble  32693  fsummmodsndifre  32700  cznnring  32999  elfzolborelfzop1  33360  zgeltp1eq  33363  zgtp1leeq  33364  mod0mul  33367  modn0mul  33368  m1modmmod  33369  difmodm1lt  33370  rege1logbzge0  33415  fllog2  33424  dignn0ldlem  33458  dignn0flhalflem1  33471  dignn0flhalflem2  33472
  Copyright terms: Public domain W3C validator