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

Theorem zred 10965
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 10867 . 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 1823   RRcr 9480   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-neg 9799  df-z 10861
This theorem is referenced by:  zcnd  10966  suprfinzcl  10975  eluzelre  11092  uzm1  11112  zsupss  11172  suprzcl2  11173  uzwo3  11178  rpnnen1lem3  11211  rpnnen1lem5  11213  fzsplit2  11713  fzdisj  11715  fzpreddisj  11733  fznatpl1  11738  fzp1disj  11742  uzdisj  11755  fzm1  11762  fz0fzdiffz0  11787  elfzmlbm  11788  elfzmlbp  11790  difelfznle  11793  nn0disj  11795  elfzolt3  11814  fzonel  11817  fzospliti  11834  fzodisj  11836  fzouzdisj  11838  fzonmapblen  11845  fzoaddel  11850  elincfzoext  11855  reflcl  11914  flge  11923  flwordi  11929  fladdz  11940  flhalf  11944  flleceil  11962  fleqceilz  11963  quoremz  11964  uzsup  11972  modmul12d  12023  modaddmodup  12032  modaddmodlo  12033  om2uzlti  12043  om2uzf1oi  12046  seqf1olem1  12128  seqf1olem2  12129  bcval4  12367  bcp1nk  12377  bcval5  12378  fzsdom2  12470  seqcoll  12496  seqcoll2  12497  ccatrn  12595  fzomaxdiflem  13257  fzomaxdif  13258  rexuzre  13267  limsupgre  13386  rlimclim1  13450  isercoll  13572  iseralt  13589  fsumm1  13648  fsum1p  13650  fsum0diaglem  13673  modfsummods  13689  isumsplit  13734  climcndslem1  13743  mertenslem1  13775  ntrivcvgmul  13793  fprodntriv  13831  fprod1p  13854  fprodeq0  13861  fzo0dvdseq  14123  dvdsmod  14127  oexpneg  14133  bitsp1  14165  bitsfzolem  14168  bitsfzo  14169  bitsmod  14170  bitscmp  14172  bitsinv1lem  14175  sadaddlem  14200  bitsres  14207  bitsuz  14208  smumul  14227  gcd0id  14245  gcdneg  14248  nn0seqcvgd  14283  nprm  14315  coprm  14325  isprm5  14337  prmexpb  14342  prmfac1  14343  hashdvds  14389  crt  14392  eulerthlem2  14396  fermltl  14398  prmdiv  14399  prmdiveq  14400  odzdvds  14406  modprm0  14414  modprmn0modprm0  14416  pythagtriplem13  14435  pcxcl  14468  pcaddlem  14491  pcadd  14492  pcfac  14502  qexpz  14504  prmunb  14516  1arithlem4  14528  4sqlem5  14544  4sqlem6  14545  4sqlem7  14546  4sqlem10  14549  4sqlem11  14557  4sqlem12  14558  4sqlem15  14561  4sqlem16  14562  4sqlem17  14563  vdwnnlem3  14599  cshwshashlem3  14666  subgmulg  16414  mndodconglem  16764  odnncl  16768  odmod  16769  oddvds  16770  dfod2  16785  sylow1lem3  16819  efgsp1  16954  efgredleme  16960  telgsumfzs  17213  zringlpirlem1  18697  zringlpirlem3  18699  znf1o  18763  zcld  21484  ovoliunlem1  22079  ovoliunlem2  22080  dyadss  22169  dyaddisjlem  22170  dyadmaxlem  22172  dvfsumle  22588  dvfsumge  22589  dvfsumabs  22590  dvfsumlem1  22593  dvfsumlem3  22595  degltlem1  22638  plyco0  22755  plyeq0lem  22773  plydivex  22859  aannenlem1  22890  efif1olem2  23096  nnlogbexp  23320  logblt  23323  ang180lem1  23340  ang180lem3  23342  wilthlem2  23541  basellem3  23554  basellem4  23555  ppiprm  23623  chtdif  23630  ppidif  23635  chtub  23685  mersenne  23700  bcmono  23750  bcmax  23751  bposlem1  23757  bposlem3  23759  bposlem5  23761  bposlem6  23762  lgslem4  23772  lgsval2lem  23779  lgsvalmod  23788  lgsneg  23792  lgsmod  23794  lgsdilem  23795  lgsdirprm  23802  lgsdilem2  23804  lgsne0  23806  lgssq  23808  lgssq2  23809  lgsqr  23819  lgsdchr  23821  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem3  23824  lgseisenlem4  23825  lgsquadlem1  23827  lgsquadlem2  23828  lgsquadlem3  23829  lgsquad3  23834  2sqlem3  23839  2sqlem8  23845  2sqblem  23850  chebbnd1lem1  23852  chebbnd1lem2  23853  chebbnd1lem3  23854  dchrmusum2  23877  dchrvmasumlem1  23878  dchrvmasum2lem  23879  dchrvmasum2if  23880  dchrvmasumlem3  23882  dchrvmasumiflem2  23885  dchrisum0lem1  23899  dchrmusumlem  23905  mudivsum  23913  mulogsumlem  23914  mulogsum  23915  mulog2sumlem2  23918  mulog2sumlem3  23919  selberglem1  23928  selberglem2  23929  pntpbnd1  23969  pntlemg  23981  pntlemf  23988  qabvle  24008  padicabv  24013  padicabvcxp  24015  ostth2lem2  24017  axlowdimlem13  24459  axlowdimlem16  24462  clwwisshclwwlem1  25007  numclwwlk5  25314  nndiffz1  27830  fzsplit3  27833  bcm1n  27834  ltesubnnd  27846  2sqmod  27870  pnfinf  27961  dya2iocress  28482  dya2iocbrsiga  28483  dya2icobrsiga  28484  dya2icoseg  28485  dya2iocucvr  28492  sxbrsigalem2  28494  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemodife  28700  ballotlemimin  28708  ballotlemsgt1  28713  ballotlemsel1i  28715  ballotlemsi  28717  ballotlemsima  28718  ballotlemrv2  28724  ballotlemfrceq  28731  ballotlemfrcn0  28732  ballotlemirc  28734  eluzmn  28755  subfacval3  28897  erdszelem8  28906  erdszelem9  28907  supfz  29348  inffz  29349  fallfacval4  29406  bpoly4  30049  ltflcei  30283  leceifl  30284  mblfinlem2  30292  dvtanlem  30304  itg2addnclem2  30307  mettrifi  30490  cntotbnd  30532  lzunuz  30940  lzenom  30942  diophin  30945  irrapxlem1  30997  irrapxlem2  30998  irrapxlem3  30999  irrapxlem4  31000  pellexlem5  31008  pellexlem6  31009  rmspecfund  31084  rmxypos  31124  ltrmynn0  31125  ltrmxnn0  31126  ltrmy  31129  rmyeq0  31130  rmyeq  31131  lermy  31132  rmyabs  31135  jm2.24nn  31136  jm2.17a  31137  jm2.17b  31138  jm2.17c  31139  jm2.24  31140  rmygeid  31141  acongrep  31157  fzmaxdif  31158  acongeq  31160  jm2.22  31176  jm2.23  31177  jm2.26lem3  31182  jm2.27a  31186  jm3.1lem1  31198  jm3.1lem3  31200  expdiophlem1  31202  hashgcdlem  31398  prmunb2  31432  isprm7  31433  lcmgcdlem  31453  nzprmdif  31465  hashnzfzclim  31468  binomcxplemnn0  31495  zltlesub  31708  monoords  31735  fzisoeu  31739  fperiodmul  31743  fzdifsuc2  31751  fmul01  31813  fmul01lt1lem1  31817  fmul01lt1lem2  31818  climsuselem1  31852  climsuse  31853  sumnnodd  31875  ltmod  31883  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnmul  31979  dvnprodlem1  31982  dvnprodlem2  31983  iblspltprt  32011  itgspltprt  32017  stoweidlem3  32024  stoweidlem11  32032  stoweidlem20  32041  stoweidlem26  32047  stoweidlem34  32055  stoweidlem59  32080  stirlinglem5  32099  dirkertrigeqlem3  32121  dirkeritg  32123  dirkercncflem1  32124  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem4  32132  fourierdlem6  32134  fourierdlem7  32135  fourierdlem11  32139  fourierdlem12  32140  fourierdlem15  32143  fourierdlem19  32147  fourierdlem20  32148  fourierdlem25  32153  fourierdlem26  32154  fourierdlem34  32162  fourierdlem35  32163  fourierdlem41  32169  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem54  32182  fourierdlem63  32191  fourierdlem64  32192  fourierdlem65  32193  fourierdlem71  32199  fourierdlem79  32207  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem114  32242  fouriersw  32253  elaa2lem  32255  etransclem3  32259  etransclem4  32260  etransclem7  32263  etransclem10  32266  etransclem15  32271  etransclem19  32275  etransclem23  32279  etransclem24  32280  etransclem25  32281  etransclem27  32283  etransclem31  32287  etransclem32  32288  etransclem35  32291  etransclem41  32297  etransclem44  32300  etransclem46  32302  etransclem48  32304  mod2eq1n2dvds  32534  dfodd4  32570  oexpnegALTV  32583  nnoALTV  32601  2elfz2melfz  32708  elfzelfzlble  32711  fsummsndifre  32717  pw2m1lepw2m1  33381  m1modmmod  33388  difmodm1lt  33389  fllogbd  33435  logbpw2m1  33442  fllog2  33443  nnpw2blen  33455  nnolog2flm1  33465  dignn0flhalflem1  33490  dignn0flhalflem2  33491
  Copyright terms: Public domain W3C validator