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

Theorem zred 10962
Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
zred.1  |-  ( ph  ->  A  e.  ZZ )
Assertion
Ref Expression
zred  |-  ( ph  ->  A  e.  RR )

Proof of Theorem zred
StepHypRef Expression
1 zssre 10867 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3502 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   RRcr 9487   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-neg 9804  df-z 10861
This theorem is referenced by:  zcnd  10963  suprfinzcl  10971  eluzelre  11088  uzm1  11108  zsupss  11167  suprzcl2  11168  uzwo3  11173  rpnnen1lem3  11206  rpnnen1lem5  11208  fzsplit2  11706  fzdisj  11708  fzpreddisj  11725  fznatpl1  11730  fzp1disj  11734  uzdisj  11747  fz0fzdiffz0  11777  elfzmlbp  11779  difelfznle  11782  nn0disj  11784  elfzolt3  11802  fzonel  11805  fzospliti  11821  fzodisj  11823  fzouzdisj  11825  fzonmapblen  11832  fzoaddel  11837  reflcl  11897  flge  11906  flwordi  11912  fladdz  11922  flhalf  11926  flleceil  11944  fleqceilz  11945  quoremz  11946  uzsup  11954  modmul12d  12005  modaddmodup  12014  modaddmodlo  12015  om2uzlti  12025  om2uzf1oi  12028  seqf1olem1  12110  seqf1olem2  12111  bcval4  12349  bcp1nk  12359  bcval5  12360  fzsdom2  12447  seqcoll  12474  seqcoll2  12475  fzomaxdiflem  13134  fzomaxdif  13135  rexuzre  13144  limsupgre  13263  rlimclim1  13327  isercoll  13449  iseralt  13466  fsumm1  13525  fsum1p  13527  fsum0diaglem  13550  modfsummods  13566  isumsplit  13611  climcndslem1  13620  mertenslem1  13652  fzo0dvdseq  13894  dvdsmod  13898  oexpneg  13904  bitsp1  13936  bitsfzolem  13939  bitsfzo  13940  bitsmod  13941  bitscmp  13943  bitsinv1lem  13946  sadaddlem  13971  bitsres  13978  bitsuz  13979  smumul  13998  gcd0id  14016  gcdneg  14019  nn0seqcvgd  14054  nprm  14086  coprm  14096  isprm5  14108  prmexpb  14113  prmfac1  14114  hashdvds  14160  crt  14163  eulerthlem2  14167  fermltl  14169  prmdiv  14170  prmdiveq  14171  odzdvds  14177  modprm0  14185  modprmn0modprm0  14187  pythagtriplem13  14206  pcxcl  14239  pcaddlem  14262  pcadd  14263  pcfac  14273  qexpz  14275  prmunb  14287  1arithlem4  14299  4sqlem5  14315  4sqlem6  14316  4sqlem7  14317  4sqlem10  14320  4sqlem11  14328  4sqlem12  14329  4sqlem15  14332  4sqlem16  14333  4sqlem17  14334  vdwnnlem3  14370  cshwshashlem3  14436  subgmulg  16010  mndodconglem  16361  odnncl  16365  odmod  16366  oddvds  16367  dfod2  16382  sylow1lem3  16416  efgsp1  16551  efgredleme  16557  telgsumfzs  16809  zringlpirlem1  18276  zringlpirlem3  18278  zlpirlem1  18281  zlpirlem3  18283  znf1o  18357  zcld  21053  ovoliunlem1  21648  ovoliunlem2  21649  dyadss  21738  dyaddisjlem  21739  dyadmaxlem  21741  dvfsumle  22157  dvfsumge  22158  dvfsumabs  22159  dvfsumlem1  22162  dvfsumlem3  22164  degltlem1  22207  plyco0  22324  plyeq0lem  22342  plydivex  22427  aannenlem1  22458  efif1olem2  22663  ang180lem1  22869  ang180lem3  22871  wilthlem2  23071  basellem3  23084  basellem4  23085  ppiprm  23153  chtdif  23160  ppidif  23165  chtub  23215  mersenne  23230  bcmono  23280  bcmax  23281  bposlem1  23287  bposlem3  23289  bposlem5  23291  bposlem6  23292  lgslem4  23302  lgsval2lem  23309  lgsvalmod  23318  lgsneg  23322  lgsmod  23324  lgsdilem  23325  lgsdirprm  23332  lgsdilem2  23334  lgsne0  23336  lgssq  23338  lgssq2  23339  lgsqr  23349  lgsdchr  23351  lgseisenlem1  23352  lgseisenlem2  23353  lgseisenlem3  23354  lgseisenlem4  23355  lgsquadlem1  23357  lgsquadlem2  23358  lgsquadlem3  23359  lgsquad3  23364  2sqlem3  23369  2sqlem8  23375  2sqblem  23380  chebbnd1lem1  23382  chebbnd1lem2  23383  chebbnd1lem3  23384  dchrmusum2  23407  dchrvmasumlem1  23408  dchrvmasum2lem  23409  dchrvmasum2if  23410  dchrvmasumlem3  23412  dchrvmasumiflem2  23415  dchrisum0lem1  23429  dchrmusumlem  23435  mudivsum  23443  mulogsumlem  23444  mulogsum  23445  mulog2sumlem2  23448  mulog2sumlem3  23449  selberglem1  23458  selberglem2  23459  pntpbnd1  23499  pntlemg  23511  pntlemf  23518  qabvle  23538  padicabv  23543  padicabvcxp  23545  ostth2lem2  23547  axlowdimlem13  23933  axlowdimlem16  23936  clwwisshclwwlem1  24481  numclwwlk5  24789  nndiffz1  27264  fzsplit3  27267  bcm1n  27268  ltesubnnd  27280  pnfinf  27389  nnlogbexp  27660  logblt  27662  dya2iocress  27885  dya2iocbrsiga  27886  dya2icobrsiga  27887  dya2icoseg  27888  dya2iocucvr  27895  sxbrsigalem2  27897  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemodife  28076  ballotlemimin  28084  ballotlemsgt1  28089  ballotlemsel1i  28091  ballotlemsi  28093  ballotlemsima  28094  ballotlemrv2  28100  ballotlemfrceq  28107  ballotlemfrcn0  28108  ballotlemirc  28110  eluzmn  28131  subfacval3  28273  erdszelem8  28282  erdszelem9  28283  supfz  28582  inffz  28583  ntrivcvgmul  28613  fprodntriv  28651  fprod1p  28674  fprodeq0  28682  fallfacval4  28742  bpoly4  29398  ltflcei  29620  leceifl  29621  mblfinlem2  29629  dvtanlem  29641  itg2addnclem2  29644  mettrifi  29853  cntotbnd  29895  lzunuz  30305  lzenom  30307  diophin  30310  irrapxlem1  30362  irrapxlem2  30363  irrapxlem3  30364  irrapxlem4  30365  pellexlem5  30373  pellexlem6  30374  rmspecfund  30449  rmxypos  30489  ltrmynn0  30490  ltrmxnn0  30491  ltrmy  30494  rmyeq0  30495  rmyeq  30496  lermy  30497  rmyabs  30500  jm2.24nn  30501  jm2.17a  30502  jm2.17b  30503  jm2.17c  30504  jm2.24  30505  rmygeid  30506  acongrep  30522  fzmaxdif  30523  acongeq  30525  jm2.22  30541  jm2.23  30542  jm2.26lem3  30547  jm2.27a  30551  jm3.1lem1  30563  jm3.1lem3  30565  expdiophlem1  30567  hashgcdlem  30762  prmunb2  30794  isprm7  30795  lcmgcdlem  30812  nzprmdif  30824  hashnzfzclim  30827  zltlesub  31045  monoords  31073  fperiodmul  31081  fmul01  31130  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climsuselem1  31149  climsuse  31150  sumnnodd  31172  ltmod  31180  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  iblspltprt  31291  itgspltprt  31297  stoweidlem3  31303  stoweidlem11  31311  stoweidlem20  31320  stoweidlem26  31326  stoweidlem34  31334  stoweidlem59  31359  stirlinglem5  31378  dirkertrigeqlem3  31400  dirkeritg  31402  dirkercncflem1  31403  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem4  31411  fourierdlem6  31413  fourierdlem7  31414  fourierdlem12  31419  fourierdlem14  31421  fourierdlem19  31426  fourierdlem20  31427  fourierdlem26  31433  fourierdlem34  31441  fourierdlem35  31442  fourierdlem41  31448  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem51  31458  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem71  31478  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem114  31521  fouriersw  31532  2elfz2melfz  31803  elfzelfzlble  31806  fsummsndifre  31814
  Copyright terms: Public domain W3C validator