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

Theorem zred 11047
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 10951 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3462 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   RRcr 9545   ZZcz 10944
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 6308  df-neg 9870  df-z 10945
This theorem is referenced by:  zcnd  11048  suprfinzcl  11057  eluzelre  11176  uzm1  11196  zsupss  11260  suprzcl2  11261  uzwo3  11266  rpnnen1lem3  11299  rpnnen1lem5  11301  fzsplit2  11831  fzdisj  11833  fzpreddisj  11852  fznatpl1  11857  fzp1disj  11861  uzdisj  11874  fzm1  11881  fz0fzdiffz0  11906  elfzmlbm  11907  elfzmlbp  11909  difelfznle  11912  nn0disj  11914  elfzolt3  11937  fzonel  11940  fzospliti  11957  fzodisj  11959  fzouzdisj  11961  fzonmapblen  11968  fzoaddel  11973  elincfzoext  11978  reflcl  12038  flge  12047  flwordi  12053  fladdz  12064  flhalf  12068  flleceil  12086  fleqceilz  12087  quoremz  12088  uzsup  12096  modmul12d  12150  modaddmodup  12159  modaddmodlo  12160  om2uzlti  12170  om2uzf1oi  12173  seqf1olem1  12258  seqf1olem2  12259  bcval4  12498  bcp1nk  12508  bcval5  12509  fzsdom2  12604  seqcoll  12631  seqcoll2  12632  ccatrn  12737  fzomaxdiflem  13405  fzomaxdif  13406  rexuzre  13415  limsupgre  13541  limsupgreOLD  13542  rlimclim1  13608  isercoll  13730  iseralt  13750  fsumm1  13811  fsum1p  13813  fsum0diaglem  13836  modfsummods  13852  isumsplit  13897  climcndslem1  13906  mertenslem1  13939  ntrivcvgmul  13957  fprodntriv  13995  fprod1p  14021  fprodeq0  14028  fallfacval4  14095  bpoly4  14111  fzo0dvdseq  14357  dvdsmod  14361  oexpneg  14367  bitsp1  14403  bitsfzolem  14406  bitsfzolemOLD  14407  bitsfzo  14408  bitsmod  14409  bitscmp  14411  bitsinv1lem  14414  sadaddlem  14439  bitsres  14446  bitsuz  14447  smumul  14466  gcd0id  14486  gcdneg  14489  nn0seqcvgd  14528  lcmgcdlem  14570  nprm  14637  prmdvdsfz  14648  isprm5  14650  coprm  14656  prmexpb  14669  prmfac1  14670  hashdvds  14722  crt  14725  eulerthlem2  14729  fermltl  14731  prmdiv  14732  prmdiveq  14733  odzdvds  14739  odzdvdsOLD  14745  vfermltlALT  14752  modprm0  14755  modprmn0modprm0  14757  pythagtriplem13  14776  pcxcl  14809  pcaddlem  14832  pcadd  14833  pcfac  14843  qexpz  14845  prmunb  14857  1arithlem4  14869  4sqlem5  14885  4sqlem6  14886  4sqlem7  14887  4sqlem10  14890  4sqlem11  14898  4sqlem12  14899  4sqlem15OLD  14902  4sqlem16OLD  14903  4sqlem17OLD  14904  4sqlem15  14908  4sqlem16  14909  4sqlem17  14910  vdwnnlem3  14946  prmgaplem7  15026  cshwshashlem3  15067  subgmulg  16830  mndodconglem  17189  odnncl  17193  odmod  17194  oddvds  17195  dfod2  17214  sylow1lem3  17251  efgsp1  17386  efgredleme  17392  telgsumfzs  17618  zringlpirlem1  19051  zringlpirlem3OLD  19053  zringlpirlem3  19055  znf1o  19120  zcld  21829  ovoliunlem1  22453  ovoliunlem2  22454  dyadss  22550  dyaddisjlem  22551  dyadmaxlem  22553  dvfsumle  22971  dvfsumge  22972  dvfsumabs  22973  dvfsumlem1  22976  dvfsumlem3  22978  degltlem1  23019  plyco0  23144  plyeq0lem  23162  plydivex  23248  aannenlem1  23282  efif1olem2  23490  nnlogbexp  23716  logblt  23719  ang180lem1  23736  ang180lem3  23738  wilthlem2  23992  basellem3  24007  basellem4  24008  ppiprm  24076  chtdif  24083  ppidif  24088  chtub  24138  mersenne  24153  bcmono  24203  bcmax  24204  bposlem1  24210  bposlem3  24212  bposlem5  24214  bposlem6  24215  lgslem4  24225  lgsval2lem  24232  lgsvalmod  24241  lgsneg  24245  lgsmod  24247  lgsdilem  24248  lgsdirprm  24255  lgsdilem2  24257  lgsne0  24259  lgssq  24261  lgssq2  24262  lgsqr  24272  lgsdchr  24274  lgseisenlem1  24275  lgseisenlem2  24276  lgseisenlem3  24277  lgseisenlem4  24278  lgsquadlem1  24280  lgsquadlem2  24281  lgsquadlem3  24282  lgsquad3  24287  2sqlem3  24292  2sqlem8  24298  2sqblem  24303  chebbnd1lem1  24305  chebbnd1lem2  24306  chebbnd1lem3  24307  dchrmusum2  24330  dchrvmasumlem1  24331  dchrvmasum2lem  24332  dchrvmasum2if  24333  dchrvmasumlem3  24335  dchrvmasumiflem2  24338  dchrisum0lem1  24352  dchrmusumlem  24358  mudivsum  24366  mulogsumlem  24367  mulogsum  24368  mulog2sumlem2  24371  mulog2sumlem3  24372  selberglem1  24381  selberglem2  24382  pntpbnd1  24422  pntlemg  24434  pntlemf  24441  qabvle  24461  padicabv  24466  padicabvcxp  24468  ostth2lem2  24470  axlowdimlem13  24982  axlowdimlem16  24985  clwwisshclwwlem1  25531  numclwwlk5  25838  nndiffz1  28372  fzsplit3  28376  bcm1n  28377  ltesubnnd  28392  2sqmod  28416  pnfinf  28507  dya2iocress  29104  dya2iocbrsiga  29105  dya2icobrsiga  29106  dya2icoseg  29107  dya2iocucvr  29114  sxbrsigalem2  29116  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemodife  29338  ballotlemimin  29346  ballotlemsgt1  29351  ballotlemsel1i  29353  ballotlemsi  29355  ballotlemsima  29356  ballotlemrv2  29362  ballotlemfrceq  29369  ballotlemfrcn0  29370  ballotlemirc  29372  ballotlemiminOLD  29384  ballotlemsgt1OLD  29389  ballotlemsel1iOLD  29391  ballotlemsiOLD  29393  ballotlemsimaOLD  29394  ballotlemrv2OLD  29400  ballotlemfrceqOLD  29407  ballotlemfrcn0OLD  29408  ballotlemircOLD  29410  eluzmn  29431  subfacval3  29920  erdszelem8  29929  erdszelem9  29930  supfz  30369  inffz  30370  ltflcei  31897  leceifl  31898  poimirlem1  31905  poimirlem2  31906  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem15  31919  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem23  31927  poimirlem24  31928  poimirlem27  31931  poimirlem29  31933  poimirlem31  31935  poimirlem32  31936  mblfinlem2  31942  dvtanlemOLD  31955  itg2addnclem2  31958  mettrifi  32050  cntotbnd  32092  lzunuz  35579  lzenom  35581  diophin  35584  irrapxlem1  35636  irrapxlem2  35637  irrapxlem3  35638  irrapxlem4  35639  pellexlem5  35647  pellexlem6  35648  rmspecfund  35727  rmxypos  35767  ltrmynn0  35768  ltrmxnn0  35769  ltrmy  35772  rmyeq0  35773  rmyeq  35774  lermy  35775  rmyabs  35778  jm2.24nn  35779  jm2.17a  35780  jm2.17b  35781  jm2.17c  35782  jm2.24  35783  rmygeid  35784  acongrep  35800  fzmaxdif  35801  acongeq  35803  jm2.22  35820  jm2.23  35821  jm2.26lem3  35826  jm2.27a  35830  jm3.1lem1  35842  jm3.1lem3  35844  expdiophlem1  35846  hashgcdlem  36044  prmunb2  36629  isprm7  36630  nzprmdif  36638  hashnzfzclim  36641  binomcxplemnn0  36668  uzwo4  37365  zltlesub  37449  monoords  37468  fzisoeu  37472  fperiodmul  37476  fzdifsuc2  37484  iuneqfzuzlem  37511  fmul01  37598  fmul01lt1lem1  37602  fmul01lt1lem2  37603  climsuselem1  37626  climsuse  37627  sumnnodd  37650  ltmod  37658  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvnmul  37758  dvnprodlem1  37761  dvnprodlem2  37762  iblspltprt  37790  itgspltprt  37796  stoweidlem3  37803  stoweidlem11  37811  stoweidlem20  37820  stoweidlem26  37826  stoweidlem34  37835  stoweidlem59  37860  stirlinglem5  37880  dirkertrigeqlem3  37902  dirkeritg  37904  dirkercncflem1  37905  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem4  37913  fourierdlem6  37915  fourierdlem7  37916  fourierdlem11  37920  fourierdlem12  37921  fourierdlem15  37924  fourierdlem19  37928  fourierdlem20  37929  fourierdlem25  37934  fourierdlem26  37935  fourierdlem34  37944  fourierdlem35  37945  fourierdlem41  37951  fourierdlem48  37958  fourierdlem49  37959  fourierdlem50  37960  fourierdlem51  37961  fourierdlem54  37964  fourierdlem63  37973  fourierdlem64  37974  fourierdlem65  37975  fourierdlem71  37981  fourierdlem79  37989  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem102  38012  fourierdlem103  38013  fourierdlem104  38014  fourierdlem114  38024  fouriersw  38035  elaa2lem  38037  elaa2lemOLD  38038  etransclem3  38042  etransclem4  38043  etransclem7  38046  etransclem10  38049  etransclem15  38054  etransclem19  38058  etransclem23  38062  etransclem24  38063  etransclem25  38064  etransclem27  38066  etransclem31  38070  etransclem32  38071  etransclem35  38074  etransclem41  38080  etransclem44  38083  etransclem46  38085  etransclem48OLD  38087  etransclem48  38088  iundjiun  38206  caratheodorylem1  38255  fzopredsuc  38590  mod2eq1n2dvds  38595  iccpartgt  38611  icceuelpartlem  38619  icceuelpart  38620  iccpartnel  38622  dfodd4  38658  oexpnegALTV  38676  nnoALTV  38694  gbogt5  38733  gboage9  38735  stgoldbwt  38747  bgoldbst  38749  sgoldbalt  38752  bgoldbtbndlem1  38770  bgoldbtbndlem2  38771  bgoldbtbndlem3  38772  bgoldbtbnd  38774  bgoldbachlt  38776  tgblthelfgott  38778  tgoldbach  38781  proththd  38784  2elfz2melfz  38912  elfzelfzlble  38915  fsummsndifre  38921  pw2m1lepw2m1  39939  m1modmmod  39945  difmodm1lt  39946  fllogbd  39992  logbpw2m1  39999  fllog2  40000  nnpw2blen  40012  nnolog2flm1  40022  dignn0flhalflem1  40047  dignn0flhalflem2  40048
  Copyright terms: Public domain W3C validator