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

Theorem zred 10859
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 10765 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3463 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   RRcr 9393   ZZcz 10758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-iota 5490  df-fv 5535  df-ov 6204  df-neg 9710  df-z 10759
This theorem is referenced by:  zcnd  10860  eluzelre  10983  uzm1  11003  zsupss  11056  suprzcl2  11057  uzwo3  11060  rpnnen1lem3  11093  rpnnen1lem5  11095  fzsplit2  11592  fzdisj  11594  fz0fzdiffz0  11607  elfzmlbp  11609  fzpreddisj  11622  fznatpl1  11628  fzp1disj  11633  uzdisj  11649  elfzolt3  11680  fzonel  11683  fzospliti  11699  fzodisj  11701  fzouzdisj  11703  fzonmapblen  11710  fzoaddel  11715  reflcl  11764  flge  11773  flwordi  11778  fladdz  11788  flhalf  11792  flleceil  11810  fleqceilz  11811  quoremz  11812  uzsup  11820  modmul12d  11871  modaddmodup  11880  modaddmodlo  11881  om2uzlti  11891  om2uzf1oi  11894  seqf1olem1  11963  seqf1olem2  11964  bcval4  12201  bcp1nk  12211  bcval5  12212  fzsdom2  12308  seqcoll  12335  seqcoll2  12336  fzomaxdiflem  12949  fzomaxdif  12950  rexuzre  12959  limsupgre  13078  rlimclim1  13142  isercoll  13264  iseralt  13281  fsumm1  13339  fsum1p  13341  fsum0diaglem  13362  isumsplit  13422  climcndslem1  13431  mertenslem1  13463  fzo0dvdseq  13705  dvdsmod  13709  oexpneg  13714  bitsp1  13746  bitsfzolem  13749  bitsfzo  13750  bitsmod  13751  bitscmp  13753  bitsinv1lem  13756  sadaddlem  13781  bitsres  13788  bitsuz  13789  smumul  13808  gcd0id  13826  gcdneg  13829  nn0seqcvgd  13864  nprm  13896  coprm  13905  isprm5  13917  prmexpb  13922  prmfac1  13923  hashdvds  13969  crt  13972  eulerthlem2  13976  fermltl  13978  prmdiv  13979  prmdiveq  13980  odzdvds  13986  modprm0  13992  modprmn0modprm0  13994  pythagtriplem13  14013  pcxcl  14046  pcaddlem  14069  pcadd  14070  pcfac  14080  qexpz  14082  prmunb  14094  1arithlem4  14106  4sqlem5  14122  4sqlem6  14123  4sqlem7  14124  4sqlem10  14127  4sqlem11  14135  4sqlem12  14136  4sqlem15  14139  4sqlem16  14140  4sqlem17  14141  vdwnnlem3  14177  cshwshashlem3  14243  subgmulg  15815  mndodconglem  16166  odnncl  16170  odmod  16171  oddvds  16172  dfod2  16187  sylow1lem3  16221  efgsp1  16356  efgredleme  16362  zringlpirlem1  18029  zringlpirlem3  18031  zlpirlem1  18034  zlpirlem3  18036  znf1o  18110  zcld  20523  ovoliunlem1  21118  ovoliunlem2  21119  dyadss  21208  dyaddisjlem  21209  dyadmaxlem  21211  dvfsumle  21627  dvfsumge  21628  dvfsumabs  21629  dvfsumlem1  21632  dvfsumlem3  21634  degltlem1  21677  plyco0  21794  plyeq0lem  21812  plydivex  21897  aannenlem1  21928  efif1olem2  22133  ang180lem1  22339  ang180lem3  22341  wilthlem2  22541  basellem3  22554  basellem4  22555  ppiprm  22623  chtdif  22630  ppidif  22635  chtub  22685  mersenne  22700  bcmono  22750  bcmax  22751  bposlem1  22757  bposlem3  22759  bposlem5  22761  bposlem6  22762  lgslem4  22772  lgsval2lem  22779  lgsvalmod  22788  lgsneg  22792  lgsmod  22794  lgsdilem  22795  lgsdirprm  22802  lgsdilem2  22804  lgsne0  22806  lgssq  22808  lgssq2  22809  lgsqr  22819  lgsdchr  22821  lgseisenlem1  22822  lgseisenlem2  22823  lgseisenlem3  22824  lgseisenlem4  22825  lgsquadlem1  22827  lgsquadlem2  22828  lgsquadlem3  22829  lgsquad3  22834  2sqlem3  22839  2sqlem8  22845  2sqblem  22850  chebbnd1lem1  22852  chebbnd1lem2  22853  chebbnd1lem3  22854  dchrmusum2  22877  dchrvmasumlem1  22878  dchrvmasum2lem  22879  dchrvmasum2if  22880  dchrvmasumlem3  22882  dchrvmasumiflem2  22885  dchrisum0lem1  22899  dchrmusumlem  22905  mudivsum  22913  mulogsumlem  22914  mulogsum  22915  mulog2sumlem2  22918  mulog2sumlem3  22919  selberglem1  22928  selberglem2  22929  pntpbnd1  22969  pntlemg  22981  pntlemf  22988  qabvle  23008  padicabv  23013  padicabvcxp  23015  ostth2lem2  23017  axlowdimlem13  23353  axlowdimlem16  23356  nndiffz1  26221  fzsplit3  26224  bcm1n  26225  ltesubnnd  26237  pnfinf  26346  nnlogbexp  26609  logblt  26611  dya2iocress  26834  dya2iocbrsiga  26835  dya2icobrsiga  26836  dya2icoseg  26837  dya2iocucvr  26844  sxbrsigalem2  26846  ballotlemfc0  27020  ballotlemfcc  27021  ballotlemodife  27025  ballotlemimin  27033  ballotlemsgt1  27038  ballotlemsel1i  27040  ballotlemsi  27042  ballotlemsima  27043  ballotlemrv2  27049  ballotlemfrceq  27056  ballotlemfrcn0  27057  ballotlemirc  27059  eluzmn  27080  subfacval3  27222  erdszelem8  27231  erdszelem9  27232  supfz  27531  inffz  27532  ntrivcvgmul  27562  fprodntriv  27600  fprod1p  27623  fprodeq0  27631  fallfacval4  27691  bpoly4  28347  ltflcei  28568  leceifl  28569  mblfinlem2  28578  dvtanlem  28590  itg2addnclem2  28593  mettrifi  28802  cntotbnd  28844  lzunuz  29255  lzenom  29257  diophin  29260  irrapxlem1  29312  irrapxlem2  29313  irrapxlem3  29314  irrapxlem4  29315  pellexlem5  29323  pellexlem6  29324  rmspecfund  29399  rmxypos  29439  ltrmynn0  29440  ltrmxnn0  29441  ltrmy  29444  rmyeq0  29445  rmyeq  29446  lermy  29447  rmyabs  29450  jm2.24nn  29451  jm2.17a  29452  jm2.17b  29453  jm2.17c  29454  jm2.24  29455  rmygeid  29456  acongrep  29472  fzmaxdif  29473  acongeq  29475  jm2.22  29493  jm2.23  29494  jm2.26lem3  29499  jm2.27a  29503  jm3.1lem1  29515  jm3.1lem3  29517  expdiophlem1  29519  hashgcdlem  29714  fmul01  29910  fmul01lt1lem1  29914  fmul01lt1lem2  29915  climsuselem1  29929  climsuse  29930  stoweidlem3  29947  stoweidlem11  29955  stoweidlem20  29964  stoweidlem26  29970  stoweidlem34  29978  stoweidlem59  30003  stirlinglem5  30022  2elfz2melfz  30351  elfzelfzlble  30358  fsummsndifre  30386  modfsummods  30393  clwwisshclwwlem1  30618  difelfznle  30637  numclwwlk5  30854  nn0disj  30887  suprfinzcl  30894  telescfzgsum  30963
  Copyright terms: Public domain W3C validator