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

Theorem zre 10893
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre

Proof of Theorem zre
StepHypRef Expression
1 elz 10891 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/w3o 972  =wceq 1395  e.wcel 1818   cr 9512  0cc0 9513  -ucneg 9829   cn 10561   cz 10889
This theorem is referenced by:  zcn  10894  zrei  10895  zssre  10896  elnn0z  10902  elnnz1  10915  znnnlt1  10916  zletr  10933  znnsub  10935  znn0sub  10936  zltp1le  10938  zleltp1  10939  nn0ge0div  10957  zextle  10961  btwnnz  10964  suprzcl  10967  msqznn  10969  peano2uz2  10975  uzind  10979  uzindOLD  10982  fzind  10987  fnn0ind  10988  eluzuzle  11118  uzid  11124  uzneg  11128  uztric  11131  uz11  11132  eluzp1m1  11133  eluzp1p1  11135  eluzaddi  11136  eluzsubi  11137  uzin  11142  uz3m2nn  11152  peano2uz  11163  nn0pzuz  11167  uzwo  11173  uzwoOLD  11174  eluz2b2  11183  uz2mulcl  11188  eqreznegel  11196  lbzbi  11199  uzsupss  11203  nn01to3  11204  zmin  11207  zmax  11208  zbtwnre  11209  rebtwnz  11210  qre  11216  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  z2ge  11426  qbtwnre  11427  elfz1eq  11726  fzn  11731  fzen  11732  uzsubsubfz  11736  fzaddel  11747  fzsuc2  11766  fzrev  11771  elfz1b  11777  fznuz  11789  uznfz  11790  fzp1nel  11791  elfz0fzfz0  11808  fz0fzelfz0  11809  fznn0sub2  11810  fz0fzdiffz0  11812  elfzmlbmOLD  11814  elfzmlbp  11815  difelfznle  11818  elfzouz2  11842  fzonlt0  11848  fzossrbm1  11854  fzospliti  11857  fzo1fzo0n0  11864  elfzo0z  11865  fzofzim  11869  eluzgtdifelfzo  11878  fzossfzop1  11893  ssfzoulel  11906  ssfzo12bi  11907  elfzonelfzo  11912  elfzomelpfzo  11914  elfznelfzob  11916  fzosplitprm1  11919  fzostep1  11922  fllt  11943  flid  11945  flbi2  11953  flhalf  11962  dfceil2  11968  ceile  11976  ceilid  11978  quoremz  11982  intfracq  11986  uzsup  11990  zmod10  12012  zmodcl  12015  zmodfz  12017  modidmul0  12022  zmodid2  12024  modcyc  12031  modmul1  12040  modaddmodup  12050  modaddmodlo  12051  modaddmulmod  12053  leexp2  12220  zsqcl2  12245  iexpcyc  12272  brfi1uzind  12532  wrdsymb0  12575  ccatsymb  12600  swrdlend  12656  swrdnd  12657  swrd0  12658  swrdvalodm2  12664  swrdswrdlem  12684  swrdswrd  12685  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12lem3  12715  repswswrd  12756  cshwmodn  12766  cshwsublen  12767  cshwidxmod  12774  cshwidxm1  12777  repswcshw  12780  2cshw  12781  cshweqrep  12789  cshw1  12790  swrd2lsw  12890  nn0abscl  13145  rexuzre  13185  znnenlem  13945  dvdsval3  13990  moddvds  13993  absdvdsb  14002  dvdsabsb  14003  dvdsle  14031  alzdvds  14036  mulmoddvds  14044  divalgmod  14064  bitsp1o  14083  gcdabs  14171  gcdabs1  14172  modgcd  14174  bezoutlem1  14176  algcvga  14208  isprm3  14226  prmn2uzge3  14237  sqnprm  14239  zgcdsq  14286  hashdvds  14305  powm2modprm  14328  modprm0  14330  modprmn0modprm0  14332  fldivp1  14416  zgz  14451  4sqlem4  14470  cshwshashlem2  14581  gexdvds  16604  zringunit  18520  zrngunit  18521  prmirred  18525  prmirredOLD  18528  znf1o  18590  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  dyadf  22000  dyadovol  22002  degltlem1  22472  coskpi  22913  cosne0  22917  relogexp  22980  cxpeq  23131  ppival2  23402  ppival2g  23403  ppiprm  23425  chtprm  23427  chtnprm  23428  ppip1le  23435  efexple  23556  lgsdir2lem4  23601  lgsne0  23608  lgsquadlem1  23629  lgsquadlem2  23630  2sqlem2  23639  rplogsumlem2  23670  pntrsumbnd  23751  axlowdim  24264  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a  24785  clwwlkext2edg  24802  wwlksubclwwlk  24804  clwwisshclwwlem1  24805  usg2cwwkdifex  24821  clwlkfclwwlk  24844  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwlk1lem2f1  25094  frgrareg  25117  frgraregord013  25118  gxnval  25262  gxmodid  25281  rezh  27952  zrhre  27997  hashf2  28090  ballotlemfc0  28431  ballotlemfcc  28432  elfzm12  29041  mblfinlem1  30051  mblfinlem2  30052  dvtanlem  30064  itg2addnclem2  30067  nn0prpwlem  30140  fzmul  30233  fzadd2  30234  incsequz2  30242  ellz1  30700  lzunuz  30701  lzenom  30703  nerabdioph  30742  pell14qrgt0  30795  rmxycomplete  30853  monotuz  30877  monotoddzzfi  30878  oddcomabszz  30880  zindbi  30882  jm2.24  30901  congrep  30911  fzneg  30920  jm2.19  30935  lcmabs  31211  oddfl  31459  fzdifsuc2  31512  climsuse  31614  stoweidlem26  31808  stoweidlem34  31816  fourierdlem20  31909  fourierdlem42  31931  fourierdlem51  31940  fourierdlem64  31953  fourierdlem76  31965  fourierdlem94  31983  fourierdlem97  31986  fourierdlem113  32002  zm1nn  32325  eluzge0nn0  32329  elfz2z  32331  2elfz2melfz  32334  elfzlble  32336  elfzelfzlble  32337  el2fzo  32339  fsummmodsndifre  32347  cznnring  32764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator