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

Theorem zred 10974
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 10877 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3487 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   RRcr 9494   ZZcz 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-neg 9813  df-z 10871
This theorem is referenced by:  zcnd  10975  suprfinzcl  10983  eluzelre  11100  uzm1  11120  zsupss  11180  suprzcl2  11181  uzwo3  11186  rpnnen1lem3  11219  rpnnen1lem5  11221  fzsplit2  11719  fzdisj  11721  fzpreddisj  11738  fznatpl1  11743  fzp1disj  11747  uzdisj  11760  fz0fzdiffz0  11791  elfzmlbm  11792  elfzmlbp  11794  difelfznle  11797  nn0disj  11799  elfzolt3  11817  fzonel  11820  fzospliti  11836  fzodisj  11838  fzouzdisj  11840  fzonmapblen  11847  fzoaddel  11852  reflcl  11912  flge  11921  flwordi  11927  fladdz  11937  flhalf  11941  flleceil  11959  fleqceilz  11960  quoremz  11961  uzsup  11969  modmul12d  12020  modaddmodup  12029  modaddmodlo  12030  om2uzlti  12040  om2uzf1oi  12043  seqf1olem1  12125  seqf1olem2  12126  bcval4  12364  bcp1nk  12374  bcval5  12375  fzsdom2  12465  seqcoll  12491  seqcoll2  12492  ccatrn  12585  fzomaxdiflem  13154  fzomaxdif  13155  rexuzre  13164  limsupgre  13283  rlimclim1  13347  isercoll  13469  iseralt  13486  fsumm1  13545  fsum1p  13547  fsum0diaglem  13570  modfsummods  13586  isumsplit  13631  climcndslem1  13640  mertenslem1  13672  fzo0dvdseq  13916  dvdsmod  13920  oexpneg  13926  bitsp1  13958  bitsfzolem  13961  bitsfzo  13962  bitsmod  13963  bitscmp  13965  bitsinv1lem  13968  sadaddlem  13993  bitsres  14000  bitsuz  14001  smumul  14020  gcd0id  14038  gcdneg  14041  nn0seqcvgd  14076  nprm  14108  coprm  14118  isprm5  14130  prmexpb  14135  prmfac1  14136  hashdvds  14182  crt  14185  eulerthlem2  14189  fermltl  14191  prmdiv  14192  prmdiveq  14193  odzdvds  14199  modprm0  14207  modprmn0modprm0  14209  pythagtriplem13  14228  pcxcl  14261  pcaddlem  14284  pcadd  14285  pcfac  14295  qexpz  14297  prmunb  14309  1arithlem4  14321  4sqlem5  14337  4sqlem6  14338  4sqlem7  14339  4sqlem10  14342  4sqlem11  14350  4sqlem12  14351  4sqlem15  14354  4sqlem16  14355  4sqlem17  14356  vdwnnlem3  14392  cshwshashlem3  14459  subgmulg  16089  mndodconglem  16439  odnncl  16443  odmod  16444  oddvds  16445  dfod2  16460  sylow1lem3  16494  efgsp1  16629  efgredleme  16635  telgsumfzs  16892  zringlpirlem1  18382  zringlpirlem3  18384  zlpirlem1  18387  zlpirlem3  18389  znf1o  18463  zcld  21191  ovoliunlem1  21786  ovoliunlem2  21787  dyadss  21876  dyaddisjlem  21877  dyadmaxlem  21879  dvfsumle  22295  dvfsumge  22296  dvfsumabs  22297  dvfsumlem1  22300  dvfsumlem3  22302  degltlem1  22345  plyco0  22462  plyeq0lem  22480  plydivex  22565  aannenlem1  22596  efif1olem2  22802  ang180lem1  23013  ang180lem3  23015  wilthlem2  23215  basellem3  23228  basellem4  23229  ppiprm  23297  chtdif  23304  ppidif  23309  chtub  23359  mersenne  23374  bcmono  23424  bcmax  23425  bposlem1  23431  bposlem3  23433  bposlem5  23435  bposlem6  23436  lgslem4  23446  lgsval2lem  23453  lgsvalmod  23462  lgsneg  23466  lgsmod  23468  lgsdilem  23469  lgsdirprm  23476  lgsdilem2  23478  lgsne0  23480  lgssq  23482  lgssq2  23483  lgsqr  23493  lgsdchr  23495  lgseisenlem1  23496  lgseisenlem2  23497  lgseisenlem3  23498  lgseisenlem4  23499  lgsquadlem1  23501  lgsquadlem2  23502  lgsquadlem3  23503  lgsquad3  23508  2sqlem3  23513  2sqlem8  23519  2sqblem  23524  chebbnd1lem1  23526  chebbnd1lem2  23527  chebbnd1lem3  23528  dchrmusum2  23551  dchrvmasumlem1  23552  dchrvmasum2lem  23553  dchrvmasum2if  23554  dchrvmasumlem3  23556  dchrvmasumiflem2  23559  dchrisum0lem1  23573  dchrmusumlem  23579  mudivsum  23587  mulogsumlem  23588  mulogsum  23589  mulog2sumlem2  23592  mulog2sumlem3  23593  selberglem1  23602  selberglem2  23603  pntpbnd1  23643  pntlemg  23655  pntlemf  23662  qabvle  23682  padicabv  23687  padicabvcxp  23689  ostth2lem2  23691  axlowdimlem13  24129  axlowdimlem16  24132  clwwisshclwwlem1  24677  numclwwlk5  24984  nndiffz1  27468  fzsplit3  27471  bcm1n  27472  ltesubnnd  27485  2sqmod  27509  pnfinf  27600  nnlogbexp  27893  logblt  27895  dya2iocress  28118  dya2iocbrsiga  28119  dya2icobrsiga  28120  dya2icoseg  28121  dya2iocucvr  28128  sxbrsigalem2  28130  ballotlemfc0  28304  ballotlemfcc  28305  ballotlemodife  28309  ballotlemimin  28317  ballotlemsgt1  28322  ballotlemsel1i  28324  ballotlemsi  28326  ballotlemsima  28327  ballotlemrv2  28333  ballotlemfrceq  28340  ballotlemfrcn0  28341  ballotlemirc  28343  eluzmn  28364  subfacval3  28506  erdszelem8  28515  erdszelem9  28516  supfz  28980  inffz  28981  ntrivcvgmul  29011  fprodntriv  29049  fprod1p  29072  fprodeq0  29080  fallfacval4  29140  bpoly4  29796  ltflcei  30018  leceifl  30019  mblfinlem2  30027  dvtanlem  30039  itg2addnclem2  30042  mettrifi  30225  cntotbnd  30267  lzunuz  30676  lzenom  30678  diophin  30681  irrapxlem1  30733  irrapxlem2  30734  irrapxlem3  30735  irrapxlem4  30736  pellexlem5  30744  pellexlem6  30745  rmspecfund  30820  rmxypos  30860  ltrmynn0  30861  ltrmxnn0  30862  ltrmy  30865  rmyeq0  30866  rmyeq  30867  lermy  30868  rmyabs  30871  jm2.24nn  30872  jm2.17a  30873  jm2.17b  30874  jm2.17c  30875  jm2.24  30876  rmygeid  30877  acongrep  30893  fzmaxdif  30894  acongeq  30896  jm2.22  30912  jm2.23  30913  jm2.26lem3  30918  jm2.27a  30922  jm3.1lem1  30934  jm3.1lem3  30936  expdiophlem1  30938  hashgcdlem  31133  prmunb2  31167  isprm7  31168  lcmgcdlem  31188  nzprmdif  31200  hashnzfzclim  31203  zltlesub  31417  monoords  31445  fzisoeu  31449  fperiodmul  31453  fmul01  31502  fmul01lt1lem1  31506  fmul01lt1lem2  31507  climsuselem1  31521  climsuse  31522  sumnnodd  31544  ltmod  31552  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  iblspltprt  31662  itgspltprt  31668  stoweidlem3  31674  stoweidlem11  31682  stoweidlem20  31691  stoweidlem26  31697  stoweidlem34  31705  stoweidlem59  31730  stirlinglem5  31749  dirkertrigeqlem3  31771  dirkeritg  31773  dirkercncflem1  31774  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem4  31782  fourierdlem6  31784  fourierdlem7  31785  fourierdlem11  31789  fourierdlem12  31790  fourierdlem15  31793  fourierdlem19  31797  fourierdlem20  31798  fourierdlem25  31803  fourierdlem26  31804  fourierdlem34  31812  fourierdlem35  31813  fourierdlem41  31819  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem51  31829  fourierdlem54  31832  fourierdlem63  31841  fourierdlem64  31842  fourierdlem65  31843  fourierdlem71  31849  fourierdlem79  31857  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem102  31880  fourierdlem103  31881  fourierdlem104  31882  fourierdlem114  31892  fouriersw  31903  2elfz2melfz  32172  elfzelfzlble  32175  fsummsndifre  32183
  Copyright terms: Public domain W3C validator