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

Theorem zred 11040
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 10944 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3468 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   RRcr 9537   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
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 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-neg 9862  df-z 10938
This theorem is referenced by:  zcnd  11041  suprfinzcl  11050  eluzelre  11169  uzm1  11189  zsupss  11253  suprzcl2  11254  uzwo3  11259  rpnnen1lem3  11292  rpnnen1lem5  11294  fzsplit2  11822  fzdisj  11824  fzpreddisj  11843  fznatpl1  11848  fzp1disj  11852  uzdisj  11865  fzm1  11872  fz0fzdiffz0  11897  elfzmlbm  11898  elfzmlbp  11900  difelfznle  11903  nn0disj  11905  elfzolt3  11928  fzonel  11931  fzospliti  11948  fzodisj  11950  fzouzdisj  11952  fzonmapblen  11959  fzoaddel  11964  elincfzoext  11969  reflcl  12029  flge  12038  flwordi  12044  fladdz  12055  flhalf  12059  flleceil  12077  fleqceilz  12078  quoremz  12079  uzsup  12087  modmul12d  12141  modaddmodup  12150  modaddmodlo  12151  om2uzlti  12161  om2uzf1oi  12164  seqf1olem1  12249  seqf1olem2  12250  bcval4  12489  bcp1nk  12499  bcval5  12500  fzsdom2  12595  seqcoll  12621  seqcoll2  12622  ccatrn  12720  fzomaxdiflem  13384  fzomaxdif  13385  rexuzre  13394  limsupgre  13520  limsupgreOLD  13521  rlimclim1  13587  isercoll  13709  iseralt  13729  fsumm1  13790  fsum1p  13792  fsum0diaglem  13815  modfsummods  13831  isumsplit  13876  climcndslem1  13885  mertenslem1  13918  ntrivcvgmul  13936  fprodntriv  13974  fprod1p  14000  fprodeq0  14007  fallfacval4  14074  bpoly4  14090  fzo0dvdseq  14336  dvdsmod  14340  oexpneg  14346  bitsp1  14379  bitsfzolem  14382  bitsfzo  14383  bitsmod  14384  bitscmp  14386  bitsinv1lem  14389  sadaddlem  14414  bitsres  14421  bitsuz  14422  smumul  14441  gcd0id  14461  gcdneg  14464  nn0seqcvgd  14500  lcmgcdlem  14542  nprm  14609  prmdvdsfz  14620  isprm5  14622  coprm  14628  prmexpb  14641  prmfac1  14642  hashdvds  14692  crt  14695  eulerthlem2  14699  fermltl  14701  prmdiv  14702  prmdiveq  14703  odzdvds  14709  vfermltlALT  14716  modprm0  14719  modprmn0modprm0  14721  pythagtriplem13  14740  pcxcl  14773  pcaddlem  14796  pcadd  14797  pcfac  14807  qexpz  14809  prmunb  14821  1arithlem4  14833  4sqlem5  14849  4sqlem6  14850  4sqlem7  14851  4sqlem10  14854  4sqlem11  14862  4sqlem12  14863  4sqlem15OLD  14866  4sqlem16OLD  14867  4sqlem17OLD  14868  4sqlem15  14872  4sqlem16  14873  4sqlem17  14874  vdwnnlem3  14910  prmgaplem7  14990  cshwshashlem3  15031  subgmulg  16782  mndodconglem  17132  odnncl  17136  odmod  17137  oddvds  17138  dfod2  17153  sylow1lem3  17187  efgsp1  17322  efgredleme  17328  telgsumfzs  17554  zringlpirlem1  18987  zringlpirlem3  18989  znf1o  19053  zcld  21742  ovoliunlem1  22333  ovoliunlem2  22334  dyadss  22429  dyaddisjlem  22430  dyadmaxlem  22432  dvfsumle  22850  dvfsumge  22851  dvfsumabs  22852  dvfsumlem1  22855  dvfsumlem3  22857  degltlem1  22898  plyco0  23014  plyeq0lem  23032  plydivex  23118  aannenlem1  23149  efif1olem2  23357  nnlogbexp  23583  logblt  23586  ang180lem1  23603  ang180lem3  23605  wilthlem2  23859  basellem3  23872  basellem4  23873  ppiprm  23941  chtdif  23948  ppidif  23953  chtub  24003  mersenne  24018  bcmono  24068  bcmax  24069  bposlem1  24075  bposlem3  24077  bposlem5  24079  bposlem6  24080  lgslem4  24090  lgsval2lem  24097  lgsvalmod  24106  lgsneg  24110  lgsmod  24112  lgsdilem  24113  lgsdirprm  24120  lgsdilem2  24122  lgsne0  24124  lgssq  24126  lgssq2  24127  lgsqr  24137  lgsdchr  24139  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgseisenlem4  24143  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  lgsquad3  24152  2sqlem3  24157  2sqlem8  24163  2sqblem  24168  chebbnd1lem1  24170  chebbnd1lem2  24171  chebbnd1lem3  24172  dchrmusum2  24195  dchrvmasumlem1  24196  dchrvmasum2lem  24197  dchrvmasum2if  24198  dchrvmasumlem3  24200  dchrvmasumiflem2  24203  dchrisum0lem1  24217  dchrmusumlem  24223  mudivsum  24231  mulogsumlem  24232  mulogsum  24233  mulog2sumlem2  24236  mulog2sumlem3  24237  selberglem1  24246  selberglem2  24247  pntpbnd1  24287  pntlemg  24299  pntlemf  24306  qabvle  24326  padicabv  24331  padicabvcxp  24333  ostth2lem2  24335  axlowdimlem13  24830  axlowdimlem16  24833  clwwisshclwwlem1  25378  numclwwlk5  25685  nndiffz1  28202  fzsplit3  28206  bcm1n  28207  ltesubnnd  28223  2sqmod  28247  pnfinf  28338  dya2iocress  28935  dya2iocbrsiga  28936  dya2icobrsiga  28937  dya2icoseg  28938  dya2iocucvr  28945  sxbrsigalem2  28947  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemodife  29156  ballotlemimin  29164  ballotlemsgt1  29169  ballotlemsel1i  29171  ballotlemsi  29173  ballotlemsima  29174  ballotlemrv2  29180  ballotlemfrceq  29187  ballotlemfrcn0  29188  ballotlemirc  29190  eluzmn  29211  subfacval3  29700  erdszelem8  29709  erdszelem9  29710  supfz  30149  inffz  30150  ltflcei  31637  leceifl  31638  poimirlem1  31645  poimirlem2  31646  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem23  31667  poimirlem24  31668  poimirlem27  31671  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  mblfinlem2  31682  dvtanlemOLD  31695  itg2addnclem2  31698  mettrifi  31790  cntotbnd  31832  lzunuz  35319  lzenom  35321  diophin  35324  irrapxlem1  35376  irrapxlem2  35377  irrapxlem3  35378  irrapxlem4  35379  pellexlem5  35387  pellexlem6  35388  rmspecfund  35463  rmxypos  35503  ltrmynn0  35504  ltrmxnn0  35505  ltrmy  35508  rmyeq0  35509  rmyeq  35510  lermy  35511  rmyabs  35514  jm2.24nn  35515  jm2.17a  35516  jm2.17b  35517  jm2.17c  35518  jm2.24  35519  rmygeid  35520  acongrep  35536  fzmaxdif  35537  acongeq  35539  jm2.22  35556  jm2.23  35557  jm2.26lem3  35562  jm2.27a  35566  jm3.1lem1  35578  jm3.1lem3  35580  expdiophlem1  35582  hashgcdlem  35773  prmunb2  36296  isprm7  36297  nzprmdif  36305  hashnzfzclim  36308  binomcxplemnn0  36335  uzwo4  37033  zltlesub  37104  monoords  37123  fzisoeu  37127  fperiodmul  37131  fzdifsuc2  37139  iuneqfzuzlem  37166  fmul01  37230  fmul01lt1lem1  37234  fmul01lt1lem2  37235  climsuselem1  37258  climsuse  37259  sumnnodd  37282  ltmod  37290  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  dvnmul  37387  dvnprodlem1  37390  dvnprodlem2  37391  iblspltprt  37419  itgspltprt  37425  stoweidlem3  37432  stoweidlem11  37440  stoweidlem20  37449  stoweidlem26  37455  stoweidlem34  37464  stoweidlem59  37489  stirlinglem5  37509  dirkertrigeqlem3  37531  dirkeritg  37533  dirkercncflem1  37534  dirkercncflem2  37535  dirkercncflem4  37537  fourierdlem4  37542  fourierdlem6  37544  fourierdlem7  37545  fourierdlem11  37549  fourierdlem12  37550  fourierdlem15  37553  fourierdlem19  37557  fourierdlem20  37558  fourierdlem25  37563  fourierdlem26  37564  fourierdlem34  37572  fourierdlem35  37573  fourierdlem41  37579  fourierdlem48  37586  fourierdlem49  37587  fourierdlem50  37588  fourierdlem51  37589  fourierdlem54  37592  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  fourierdlem71  37609  fourierdlem79  37617  fourierdlem89  37627  fourierdlem90  37628  fourierdlem91  37629  fourierdlem102  37640  fourierdlem103  37641  fourierdlem104  37642  fourierdlem114  37652  fouriersw  37663  elaa2lem  37665  etransclem3  37669  etransclem4  37670  etransclem7  37673  etransclem10  37676  etransclem15  37681  etransclem19  37685  etransclem23  37689  etransclem24  37690  etransclem25  37691  etransclem27  37693  etransclem31  37697  etransclem32  37698  etransclem35  37701  etransclem41  37707  etransclem44  37710  etransclem46  37712  etransclem48  37714  iundjiun  37807  caratheodorylem1  37856  fzopredsuc  38110  mod2eq1n2dvds  38115  iccpartgt  38131  icceuelpartlem  38139  icceuelpart  38140  iccpartnel  38142  dfodd4  38178  oexpnegALTV  38196  nnoALTV  38214  gbogt5  38253  gboage9  38255  stgoldbwt  38267  bgoldbst  38269  sgoldbalt  38272  bgoldbtbndlem1  38290  bgoldbtbndlem2  38291  bgoldbtbndlem3  38292  bgoldbtbnd  38294  bgoldbachlt  38296  tgblthelfgott  38298  tgoldbach  38301  proththd  38304  2elfz2melfz  38407  elfzelfzlble  38410  fsummsndifre  38415  pw2m1lepw2m1  39079  m1modmmod  39085  difmodm1lt  39086  fllogbd  39132  logbpw2m1  39139  fllog2  39140  nnpw2blen  39152  nnolog2flm1  39162  dignn0flhalflem1  39187  dignn0flhalflem2  39188
  Copyright terms: Public domain W3C validator