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

Theorem zred 10331
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 10245 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3306 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   RRcr 8945   ZZcz 10238
This theorem is referenced by:  zcnd  10332  eluzelre  10453  uzm1  10472  zsupss  10521  suprzcl2  10522  uzwo3  10525  rpnnen1lem3  10558  rpnnen1lem5  10560  fzsplit2  11032  fzdisj  11034  fzp1disj  11061  uzdisj  11074  elfzolt3  11104  fzonel  11107  fzospliti  11120  fzodisj  11122  fzouzdisj  11124  fzoaddel  11130  reflcl  11160  flge  11169  flwordi  11174  fladdz  11182  flhalf  11186  quoremz  11191  uzsup  11199  modmul12d  11235  om2uzlti  11245  om2uzf1oi  11248  seqf1olem1  11317  seqf1olem2  11318  bcval4  11553  bcp1nk  11563  bcval5  11564  fzsdom2  11648  seqcoll  11667  seqcoll2  11668  fzomaxdiflem  12101  fzomaxdif  12102  rexuzre  12111  limsupgre  12230  rlimclim1  12294  isercoll  12416  iseralt  12433  fsumm1  12492  fsum1p  12494  fsum0diaglem  12515  isumsplit  12575  climcndslem1  12584  mertenslem1  12616  fzo0dvdseq  12857  dvdsmod  12861  oexpneg  12866  bitsp1  12898  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  bitscmp  12905  bitsinv1lem  12908  sadaddlem  12933  bitsres  12940  bitsuz  12941  smumul  12960  gcd0id  12978  gcdneg  12981  nn0seqcvgd  13016  nprm  13048  coprm  13055  isprm5  13067  prmexpb  13072  prmfac1  13073  hashdvds  13119  crt  13122  eulerthlem2  13126  fermltl  13128  prmdiv  13129  prmdiveq  13130  odzdvds  13136  pythagtriplem13  13156  pcxcl  13189  pcaddlem  13212  pcadd  13213  pcfac  13223  qexpz  13225  prmunb  13237  1arithlem4  13249  4sqlem5  13265  4sqlem6  13266  4sqlem7  13267  4sqlem10  13270  4sqlem11  13278  4sqlem12  13279  4sqlem15  13282  4sqlem16  13283  4sqlem17  13284  vdwnnlem3  13320  subgmulg  14913  mndodconglem  15134  odnncl  15138  odmod  15139  oddvds  15140  dfod2  15155  sylow1lem3  15189  efgsp1  15324  efgredleme  15330  zlpirlem1  16723  zlpirlem3  16725  znf1o  16787  zcld  18797  ovoliunlem1  19351  ovoliunlem2  19352  dyadss  19439  dyaddisjlem  19440  dyadmaxlem  19442  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem3  19865  degltlem1  19948  plyco0  20064  plyeq0lem  20082  plydivex  20167  aannenlem1  20198  efif1olem2  20398  ang180lem1  20604  ang180lem3  20606  wilthlem2  20805  basellem3  20818  basellem4  20819  ppiprm  20887  chtdif  20894  ppidif  20899  chtub  20949  mersenne  20964  bcmono  21014  bcmax  21015  bposlem1  21021  bposlem3  21023  bposlem5  21025  bposlem6  21026  lgslem4  21036  lgsval2lem  21043  lgsvalmod  21052  lgsneg  21056  lgsmod  21058  lgsdilem  21059  lgsdirprm  21066  lgsdilem2  21068  lgsne0  21070  lgssq  21072  lgssq2  21073  lgsqr  21083  lgsdchr  21085  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad3  21098  2sqlem3  21103  2sqlem8  21109  2sqblem  21114  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasum2if  21144  dchrvmasumlem3  21146  dchrvmasumiflem2  21149  dchrisum0lem1  21163  dchrmusumlem  21169  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  mulog2sumlem2  21182  mulog2sumlem3  21183  selberglem1  21192  selberglem2  21193  pntpbnd1  21233  pntlemg  21245  pntlemf  21252  qabvle  21272  padicabv  21277  padicabvcxp  21279  ostth2lem2  21281  fzsplit3  24103  bcm1n  24104  ltesubnnd  24115  pnfinf  24206  nnlogbexp  24357  logblt  24359  dya2iocress  24577  dya2iocbrsiga  24578  dya2icobrsiga  24579  dya2icoseg  24580  dya2iocucvr  24587  sxbrsigalem2  24589  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemodife  24708  ballotlemimin  24716  ballotlemsgt1  24721  ballotlemsel1i  24723  ballotlemsi  24725  ballotlemsima  24726  ballotlemrv2  24732  ballotlemfrceq  24739  ballotlemfrcn0  24740  ballotlemirc  24742  subfacval3  24828  erdszelem8  24837  erdszelem9  24838  fznatpl1  25151  supfz  25152  inffz  25153  ntrivcvgmul  25183  fprodntriv  25221  fprod1p  25244  fprodeq0  25252  binomfallfaclem1  25306  binomfallfaclem2  25307  axlowdimlem13  25797  axlowdimlem16  25800  bpoly4  26009  ltflcei  26140  leceifl  26141  mblfinlem  26143  itg2addnclem2  26156  mettrifi  26353  cntotbnd  26395  lzunuz  26716  lzenom  26718  diophin  26721  irrapxlem1  26775  irrapxlem2  26776  irrapxlem3  26777  irrapxlem4  26778  pellexlem5  26786  pellexlem6  26787  rmspecfund  26862  rmxypos  26902  ltrmynn0  26903  ltrmxnn0  26904  ltrmy  26907  rmyeq0  26908  rmyeq  26909  lermy  26910  rmyabs  26913  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  jm2.24  26918  rmygeid  26919  acongrep  26935  fzmaxdif  26936  acongeq  26938  jm2.22  26956  jm2.23  26957  jm2.26lem3  26962  jm2.27a  26966  jm3.1lem1  26978  jm3.1lem3  26980  expdiophlem1  26982  hashgcdlem  27384  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climsuselem1  27600  climsuse  27601  stoweidlem3  27619  stoweidlem11  27627  stoweidlem20  27636  stoweidlem26  27642  stoweidlem34  27650  stoweidlem59  27675  stirlinglem5  27694  elfzmlbp  27978
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250  df-z 10239
  Copyright terms: Public domain W3C validator