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

Theorem zred 11030
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 10934 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3398 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1891   RRcr 9525   ZZcz 10927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-rex 2743  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-iota 5525  df-fv 5569  df-ov 6279  df-neg 9850  df-z 10928
This theorem is referenced by:  zcnd  11031  suprfinzcl  11040  eluzelre  11159  uzm1  11179  zsupss  11243  suprzcl2  11244  uzwo3  11249  rpnnen1lem3  11282  rpnnen1lem5  11284  fzsplit2  11815  fzdisj  11817  fzpreddisj  11836  fznatpl1  11841  fzp1disj  11845  uzdisj  11858  fzm1  11865  fz0fzdiffz0  11891  elfzmlbm  11892  elfzmlbp  11894  difelfznle  11897  nn0disj  11899  elfzolt3  11923  fzonel  11926  fzospliti  11943  fzodisj  11945  fzouzdisj  11947  fzonmapblen  11954  fzoaddel  11960  elincfzoext  11965  reflcl  12026  flge  12035  flwordi  12041  fladdz  12052  flhalf  12056  flleceil  12074  fleqceilz  12075  quoremz  12076  uzsup  12084  modmul12d  12138  modaddmodup  12147  modaddmodlo  12148  om2uzlti  12158  om2uzf1oi  12161  seqf1olem1  12246  seqf1olem2  12247  bcval4  12486  bcp1nk  12496  bcval5  12497  fzsdom2  12595  seqcoll  12622  seqcoll2  12623  ccatrn  12731  fzomaxdiflem  13416  fzomaxdif  13417  rexuzre  13426  limsupgre  13553  limsupgreOLD  13554  rlimclim1  13620  isercoll  13742  iseralt  13762  fsumm1  13823  fsum1p  13825  fsum0diaglem  13848  modfsummods  13864  isumsplit  13909  climcndslem1  13918  mertenslem1  13951  ntrivcvgmul  13969  fprodntriv  14007  fprod1p  14033  fprodeq0  14040  fallfacval4  14107  bpoly4  14123  fzo0dvdseq  14369  dvdsmod  14373  oexpneg  14379  bitsp1  14415  bitsfzolem  14418  bitsfzolemOLD  14419  bitsfzo  14420  bitsmod  14421  bitscmp  14423  bitsinv1lem  14426  sadaddlem  14451  bitsres  14458  bitsuz  14459  smumul  14478  gcd0id  14498  gcdneg  14501  nn0seqcvgd  14540  lcmgcdlem  14582  nprm  14649  prmdvdsfz  14660  isprm5  14662  coprm  14668  prmexpb  14681  prmfac1  14682  hashdvds  14734  crt  14737  eulerthlem2  14741  fermltl  14743  prmdiv  14744  prmdiveq  14745  odzdvds  14751  odzdvdsOLD  14757  vfermltlALT  14764  modprm0  14767  modprmn0modprm0  14769  pythagtriplem13  14788  pcxcl  14821  pcaddlem  14844  pcadd  14845  pcfac  14855  qexpz  14857  prmunb  14869  1arithlem4  14881  4sqlem5  14897  4sqlem6  14898  4sqlem7  14899  4sqlem10  14902  4sqlem11  14910  4sqlem12  14911  4sqlem15OLD  14914  4sqlem16OLD  14915  4sqlem17OLD  14916  4sqlem15  14920  4sqlem16  14921  4sqlem17  14922  vdwnnlem3  14958  prmgaplem7  15038  cshwshashlem3  15079  subgmulg  16842  mndodconglem  17201  odnncl  17205  odmod  17206  oddvds  17207  dfod2  17226  sylow1lem3  17263  efgsp1  17398  efgredleme  17404  telgsumfzs  17630  zringlpirlem1  19064  zringlpirlem3OLD  19066  zringlpirlem3  19068  znf1o  19133  zcld  21842  ovoliunlem1  22466  ovoliunlem2  22467  dyadss  22564  dyaddisjlem  22565  dyadmaxlem  22567  dvfsumle  22985  dvfsumge  22986  dvfsumabs  22987  dvfsumlem1  22990  dvfsumlem3  22992  degltlem1  23033  plyco0  23158  plyeq0lem  23176  plydivex  23262  aannenlem1  23296  efif1olem2  23504  nnlogbexp  23730  logblt  23733  ang180lem1  23750  ang180lem3  23752  wilthlem2  24006  basellem3  24021  basellem4  24022  ppiprm  24090  chtdif  24097  ppidif  24102  chtub  24152  mersenne  24167  bcmono  24217  bcmax  24218  bposlem1  24224  bposlem3  24226  bposlem5  24228  bposlem6  24229  lgslem4  24239  lgsval2lem  24246  lgsvalmod  24255  lgsneg  24259  lgsmod  24261  lgsdilem  24262  lgsdirprm  24269  lgsdilem2  24271  lgsne0  24273  lgssq  24275  lgssq2  24276  lgsqr  24286  lgsdchr  24288  lgseisenlem1  24289  lgseisenlem2  24290  lgseisenlem3  24291  lgseisenlem4  24292  lgsquadlem1  24294  lgsquadlem2  24295  lgsquadlem3  24296  lgsquad3  24301  2sqlem3  24306  2sqlem8  24312  2sqblem  24317  chebbnd1lem1  24319  chebbnd1lem2  24320  chebbnd1lem3  24321  dchrmusum2  24344  dchrvmasumlem1  24345  dchrvmasum2lem  24346  dchrvmasum2if  24347  dchrvmasumlem3  24349  dchrvmasumiflem2  24352  dchrisum0lem1  24366  dchrmusumlem  24372  mudivsum  24380  mulogsumlem  24381  mulogsum  24382  mulog2sumlem2  24385  mulog2sumlem3  24386  selberglem1  24395  selberglem2  24396  pntpbnd1  24436  pntlemg  24448  pntlemf  24455  qabvle  24475  padicabv  24480  padicabvcxp  24482  ostth2lem2  24484  axlowdimlem13  24996  axlowdimlem16  24999  clwwisshclwwlem1  25545  numclwwlk5  25852  nndiffz1  28374  fzsplit3  28378  bcm1n  28379  ltesubnnd  28393  2sqmod  28417  pnfinf  28507  dya2iocress  29102  dya2iocbrsiga  29103  dya2icobrsiga  29104  dya2icoseg  29105  dya2iocucvr  29112  sxbrsigalem2  29114  ballotlemfc0  29331  ballotlemfcc  29332  ballotlemodife  29336  ballotlemimin  29344  ballotlemsgt1  29349  ballotlemsel1i  29351  ballotlemsi  29353  ballotlemsima  29354  ballotlemrv2  29360  ballotlemfrceq  29367  ballotlemfrcn0  29368  ballotlemirc  29370  ballotlemiminOLD  29382  ballotlemsgt1OLD  29387  ballotlemsel1iOLD  29389  ballotlemsiOLD  29391  ballotlemsimaOLD  29392  ballotlemrv2OLD  29398  ballotlemfrceqOLD  29405  ballotlemfrcn0OLD  29406  ballotlemircOLD  29408  eluzmn  29429  subfacval3  29918  erdszelem8  29927  erdszelem9  29928  supfz  30368  inffz  30369  ltflcei  31935  leceifl  31936  poimirlem1  31943  poimirlem2  31944  poimirlem6  31948  poimirlem7  31949  poimirlem8  31950  poimirlem15  31957  poimirlem16  31958  poimirlem17  31959  poimirlem19  31961  poimirlem20  31962  poimirlem23  31965  poimirlem24  31966  poimirlem27  31969  poimirlem29  31971  poimirlem31  31973  poimirlem32  31974  mblfinlem2  31980  dvtanlemOLD  31993  itg2addnclem2  31996  mettrifi  32088  cntotbnd  32130  lzunuz  35612  lzenom  35614  diophin  35617  irrapxlem1  35668  irrapxlem2  35669  irrapxlem3  35670  irrapxlem4  35671  pellexlem5  35679  pellexlem6  35680  rmspecfund  35759  rmxypos  35799  ltrmynn0  35800  ltrmxnn0  35801  ltrmy  35804  rmyeq0  35805  rmyeq  35806  lermy  35807  rmyabs  35810  jm2.24nn  35811  jm2.17a  35812  jm2.17b  35813  jm2.17c  35814  jm2.24  35815  rmygeid  35816  acongrep  35832  fzmaxdif  35833  acongeq  35835  jm2.22  35852  jm2.23  35853  jm2.26lem3  35858  jm2.27a  35862  jm3.1lem1  35874  jm3.1lem3  35876  expdiophlem1  35878  hashgcdlem  36076  prmunb2  36660  isprm7  36661  nzprmdif  36669  hashnzfzclim  36672  binomcxplemnn0  36699  uzwo4  37387  zltlesub  37526  monoords  37545  fzisoeu  37549  fperiodmul  37553  fzdifsuc2  37561  iuneqfzuzlem  37588  fmul01  37700  fmul01lt1lem1  37704  fmul01lt1lem2  37705  climsuselem1  37728  climsuse  37729  sumnnodd  37752  ltmod  37760  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  dvnmul  37860  dvnprodlem1  37863  dvnprodlem2  37864  iblspltprt  37892  itgspltprt  37898  stoweidlem3  37920  stoweidlem11  37928  stoweidlem20  37937  stoweidlem26  37943  stoweidlem34  37952  stoweidlem59  37977  stirlinglem5  37997  dirkertrigeqlem3  38019  dirkeritg  38021  dirkercncflem1  38022  dirkercncflem2  38023  dirkercncflem4  38025  fourierdlem4  38030  fourierdlem6  38032  fourierdlem7  38033  fourierdlem11  38037  fourierdlem12  38038  fourierdlem15  38041  fourierdlem19  38045  fourierdlem20  38046  fourierdlem25  38051  fourierdlem26  38052  fourierdlem34  38061  fourierdlem35  38062  fourierdlem41  38068  fourierdlem48  38075  fourierdlem49  38076  fourierdlem50  38077  fourierdlem51  38078  fourierdlem54  38081  fourierdlem63  38090  fourierdlem64  38091  fourierdlem65  38092  fourierdlem71  38098  fourierdlem79  38106  fourierdlem89  38116  fourierdlem90  38117  fourierdlem91  38118  fourierdlem102  38129  fourierdlem103  38130  fourierdlem104  38131  fourierdlem114  38141  fouriersw  38152  elaa2lem  38154  elaa2lemOLD  38155  etransclem3  38159  etransclem4  38160  etransclem7  38163  etransclem10  38166  etransclem15  38171  etransclem19  38175  etransclem23  38179  etransclem24  38180  etransclem25  38181  etransclem27  38183  etransclem31  38187  etransclem32  38188  etransclem35  38191  etransclem41  38197  etransclem44  38200  etransclem46  38202  etransclem48OLD  38204  etransclem48  38205  iundjiun  38359  caratheodorylem1  38411  fzopredsuc  38811  mod2eq1n2dvds  38816  iccpartgt  38832  icceuelpartlem  38840  icceuelpart  38841  iccpartnel  38843  dfodd4  38879  oexpnegALTV  38897  nnoALTV  38915  gbogt5  38954  gboage9  38956  stgoldbwt  38968  bgoldbst  38970  sgoldbalt  38973  bgoldbtbndlem1  38991  bgoldbtbndlem2  38992  bgoldbtbndlem3  38993  bgoldbtbnd  38995  bgoldbachlt  38997  tgblthelfgott  38999  tgoldbach  39002  proththd  39005  2elfz2melfz  39152  elfzelfzlble  39155  fsummsndifre  39189  pthdlem1  39844  pw2m1lepw2m1  40643  m1modmmod  40649  difmodm1lt  40650  fllogbd  40696  logbpw2m1  40703  fllog2  40704  nnpw2blen  40716  nnolog2flm1  40726  dignn0flhalflem1  40751  dignn0flhalflem2  40752
  Copyright terms: Public domain W3C validator