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

Theorem zred 10380
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 10294 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3348 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RRcr 8994   ZZcz 10287
This theorem is referenced by:  zcnd  10381  eluzelre  10502  uzm1  10521  zsupss  10570  suprzcl2  10571  uzwo3  10574  rpnnen1lem3  10607  rpnnen1lem5  10609  fzsplit2  11081  fzdisj  11083  fzp1disj  11110  uzdisj  11124  elfzolt3  11154  fzonel  11157  fzospliti  11170  fzodisj  11172  fzouzdisj  11174  fzoaddel  11180  reflcl  11210  flge  11219  flwordi  11224  fladdz  11232  flhalf  11236  quoremz  11241  uzsup  11249  modmul12d  11285  om2uzlti  11295  om2uzf1oi  11298  seqf1olem1  11367  seqf1olem2  11368  bcval4  11603  bcp1nk  11613  bcval5  11614  fzsdom2  11698  seqcoll  11717  seqcoll2  11718  fzomaxdiflem  12151  fzomaxdif  12152  rexuzre  12161  limsupgre  12280  rlimclim1  12344  isercoll  12466  iseralt  12483  fsumm1  12542  fsum1p  12544  fsum0diaglem  12565  isumsplit  12625  climcndslem1  12634  mertenslem1  12666  fzo0dvdseq  12907  dvdsmod  12911  oexpneg  12916  bitsp1  12948  bitsfzolem  12951  bitsfzo  12952  bitsmod  12953  bitscmp  12955  bitsinv1lem  12958  sadaddlem  12983  bitsres  12990  bitsuz  12991  smumul  13010  gcd0id  13028  gcdneg  13031  nn0seqcvgd  13066  nprm  13098  coprm  13105  isprm5  13117  prmexpb  13122  prmfac1  13123  hashdvds  13169  crt  13172  eulerthlem2  13176  fermltl  13178  prmdiv  13179  prmdiveq  13180  odzdvds  13186  pythagtriplem13  13206  pcxcl  13239  pcaddlem  13262  pcadd  13263  pcfac  13273  qexpz  13275  prmunb  13287  1arithlem4  13299  4sqlem5  13315  4sqlem6  13316  4sqlem7  13317  4sqlem10  13320  4sqlem11  13328  4sqlem12  13329  4sqlem15  13332  4sqlem16  13333  4sqlem17  13334  vdwnnlem3  13370  subgmulg  14963  mndodconglem  15184  odnncl  15188  odmod  15189  oddvds  15190  dfod2  15205  sylow1lem3  15239  efgsp1  15374  efgredleme  15380  zlpirlem1  16773  zlpirlem3  16775  znf1o  16837  zcld  18849  ovoliunlem1  19403  ovoliunlem2  19404  dyadss  19491  dyaddisjlem  19492  dyadmaxlem  19494  dvfsumle  19910  dvfsumge  19911  dvfsumabs  19912  dvfsumlem1  19915  dvfsumlem3  19917  degltlem1  20000  plyco0  20116  plyeq0lem  20134  plydivex  20219  aannenlem1  20250  efif1olem2  20450  ang180lem1  20656  ang180lem3  20658  wilthlem2  20857  basellem3  20870  basellem4  20871  ppiprm  20939  chtdif  20946  ppidif  20951  chtub  21001  mersenne  21016  bcmono  21066  bcmax  21067  bposlem1  21073  bposlem3  21075  bposlem5  21077  bposlem6  21078  lgslem4  21088  lgsval2lem  21095  lgsvalmod  21104  lgsneg  21108  lgsmod  21110  lgsdilem  21111  lgsdirprm  21118  lgsdilem2  21120  lgsne0  21122  lgssq  21124  lgssq2  21125  lgsqr  21135  lgsdchr  21137  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem3  21140  lgseisenlem4  21141  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  lgsquad3  21150  2sqlem3  21155  2sqlem8  21161  2sqblem  21166  chebbnd1lem1  21168  chebbnd1lem2  21169  chebbnd1lem3  21170  dchrmusum2  21193  dchrvmasumlem1  21194  dchrvmasum2lem  21195  dchrvmasum2if  21196  dchrvmasumlem3  21198  dchrvmasumiflem2  21201  dchrisum0lem1  21215  dchrmusumlem  21221  mudivsum  21229  mulogsumlem  21230  mulogsum  21231  mulog2sumlem2  21234  mulog2sumlem3  21235  selberglem1  21244  selberglem2  21245  pntpbnd1  21285  pntlemg  21297  pntlemf  21304  qabvle  21324  padicabv  21329  padicabvcxp  21331  ostth2lem2  21333  fzsplit3  24155  bcm1n  24156  ltesubnnd  24167  pnfinf  24258  nnlogbexp  24409  logblt  24411  dya2iocress  24629  dya2iocbrsiga  24630  dya2icobrsiga  24631  dya2icoseg  24632  dya2iocucvr  24639  sxbrsigalem2  24641  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemodife  24760  ballotlemimin  24768  ballotlemsgt1  24773  ballotlemsel1i  24775  ballotlemsi  24777  ballotlemsima  24778  ballotlemrv2  24784  ballotlemfrceq  24791  ballotlemfrcn0  24792  ballotlemirc  24794  subfacval3  24880  erdszelem8  24889  erdszelem9  24890  fznatpl1  25203  supfz  25204  inffz  25205  ntrivcvgmul  25235  fprodntriv  25273  fprod1p  25296  fprodeq0  25304  fallfacval4  25364  axlowdimlem13  25898  axlowdimlem16  25901  bpoly4  26110  ltflcei  26247  leceifl  26248  mblfinlem2  26256  dvtanlem  26268  itg2addnclem2  26271  mettrifi  26477  cntotbnd  26519  lzunuz  26840  lzenom  26842  diophin  26845  irrapxlem1  26899  irrapxlem2  26900  irrapxlem3  26901  irrapxlem4  26902  pellexlem5  26910  pellexlem6  26911  rmspecfund  26986  rmxypos  27026  ltrmynn0  27027  ltrmxnn0  27028  ltrmy  27031  rmyeq0  27032  rmyeq  27033  lermy  27034  rmyabs  27037  jm2.24nn  27038  jm2.17a  27039  jm2.17b  27040  jm2.17c  27041  jm2.24  27042  rmygeid  27043  acongrep  27059  fzmaxdif  27060  acongeq  27062  jm2.22  27080  jm2.23  27081  jm2.26lem3  27086  jm2.27a  27090  jm3.1lem1  27102  jm3.1lem3  27104  expdiophlem1  27106  hashgcdlem  27507  fmul01  27700  fmul01lt1lem1  27704  fmul01lt1lem2  27705  climsuselem1  27723  climsuse  27724  stoweidlem3  27742  stoweidlem11  27750  stoweidlem20  27759  stoweidlem26  27765  stoweidlem34  27773  stoweidlem59  27798  stirlinglem5  27817  elfzmlbp  28130  2elfz2melfz  28140  fz0fzdiffz0  28142  fzonmapblen  28157  modprm0  28262  2cshw2lem1  28286  2cshwmod  28291  cshweqrep  28308  cshwssizelem4  28318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-neg 9299  df-z 10288
  Copyright terms: Public domain W3C validator