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

Theorem zred 10735
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 10641 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3342 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   RRcr 9269   ZZcz 10634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9586  df-z 10635
This theorem is referenced by:  zcnd  10736  eluzelre  10859  uzm1  10879  zsupss  10932  suprzcl2  10933  uzwo3  10936  rpnnen1lem3  10969  rpnnen1lem5  10971  fzsplit2  11461  fzdisj  11463  fz0fzdiffz0  11476  elfzmlbp  11478  fznatpl1  11495  fzp1disj  11500  uzdisj  11515  elfzolt3  11546  fzonel  11549  fzospliti  11565  fzodisj  11567  fzouzdisj  11569  fzonmapblen  11576  fzoaddel  11581  reflcl  11630  flge  11639  flwordi  11644  fladdz  11654  flhalf  11658  flleceil  11676  fleqceilz  11677  quoremz  11678  uzsup  11686  modmul12d  11737  modaddmodup  11746  modaddmodlo  11747  om2uzlti  11757  om2uzf1oi  11760  seqf1olem1  11829  seqf1olem2  11830  bcval4  12067  bcp1nk  12077  bcval5  12078  fzsdom2  12173  seqcoll  12200  seqcoll2  12201  fzomaxdiflem  12814  fzomaxdif  12815  rexuzre  12824  limsupgre  12943  rlimclim1  13007  isercoll  13129  iseralt  13146  fsumm1  13204  fsum1p  13206  fsum0diaglem  13227  isumsplit  13286  climcndslem1  13295  mertenslem1  13327  fzo0dvdseq  13569  dvdsmod  13573  oexpneg  13578  bitsp1  13610  bitsfzolem  13613  bitsfzo  13614  bitsmod  13615  bitscmp  13617  bitsinv1lem  13620  sadaddlem  13645  bitsres  13652  bitsuz  13653  smumul  13672  gcd0id  13690  gcdneg  13693  nn0seqcvgd  13728  nprm  13760  coprm  13769  isprm5  13781  prmexpb  13786  prmfac1  13787  hashdvds  13833  crt  13836  eulerthlem2  13840  fermltl  13842  prmdiv  13843  prmdiveq  13844  odzdvds  13850  modprm0  13856  modprmn0modprm0  13858  pythagtriplem13  13877  pcxcl  13910  pcaddlem  13933  pcadd  13934  pcfac  13944  qexpz  13946  prmunb  13958  1arithlem4  13970  4sqlem5  13986  4sqlem6  13987  4sqlem7  13988  4sqlem10  13991  4sqlem11  13999  4sqlem12  14000  4sqlem15  14003  4sqlem16  14004  4sqlem17  14005  vdwnnlem3  14041  cshwshashlem3  14107  subgmulg  15675  mndodconglem  16024  odnncl  16028  odmod  16029  oddvds  16030  dfod2  16045  sylow1lem3  16079  efgsp1  16214  efgredleme  16220  zringlpirlem1  17745  zringlpirlem3  17747  zlpirlem1  17750  zlpirlem3  17752  znf1o  17826  zcld  20232  ovoliunlem1  20827  ovoliunlem2  20828  dyadss  20916  dyaddisjlem  20917  dyadmaxlem  20919  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvfsumlem1  21340  dvfsumlem3  21342  degltlem1  21428  plyco0  21545  plyeq0lem  21563  plydivex  21648  aannenlem1  21679  efif1olem2  21884  ang180lem1  22090  ang180lem3  22092  wilthlem2  22292  basellem3  22305  basellem4  22306  ppiprm  22374  chtdif  22381  ppidif  22386  chtub  22436  mersenne  22451  bcmono  22501  bcmax  22502  bposlem1  22508  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgslem4  22523  lgsval2lem  22530  lgsvalmod  22539  lgsneg  22543  lgsmod  22545  lgsdilem  22546  lgsdirprm  22553  lgsdilem2  22555  lgsne0  22557  lgssq  22559  lgssq2  22560  lgsqr  22570  lgsdchr  22572  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  lgsquad3  22585  2sqlem3  22590  2sqlem8  22596  2sqblem  22601  chebbnd1lem1  22603  chebbnd1lem2  22604  chebbnd1lem3  22605  dchrmusum2  22628  dchrvmasumlem1  22629  dchrvmasum2lem  22630  dchrvmasum2if  22631  dchrvmasumlem3  22633  dchrvmasumiflem2  22636  dchrisum0lem1  22650  dchrmusumlem  22656  mudivsum  22664  mulogsumlem  22665  mulogsum  22666  mulog2sumlem2  22669  mulog2sumlem3  22670  selberglem1  22679  selberglem2  22680  pntpbnd1  22720  pntlemg  22732  pntlemf  22739  qabvle  22759  padicabv  22764  padicabvcxp  22766  ostth2lem2  22768  axlowdimlem13  23023  axlowdimlem16  23026  nndiffz1  25898  fzsplit3  25901  bcm1n  25902  ltesubnnd  25914  pnfinf  26024  nnlogbexp  26317  logblt  26319  dya2iocress  26543  dya2iocbrsiga  26544  dya2icobrsiga  26545  dya2icoseg  26546  dya2iocucvr  26553  sxbrsigalem2  26555  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemodife  26728  ballotlemimin  26736  ballotlemsgt1  26741  ballotlemsel1i  26743  ballotlemsi  26745  ballotlemsima  26746  ballotlemrv2  26752  ballotlemfrceq  26759  ballotlemfrcn0  26760  ballotlemirc  26762  eluzmn  26783  subfacval3  26925  erdszelem8  26934  erdszelem9  26935  supfz  27233  inffz  27234  ntrivcvgmul  27264  fprodntriv  27302  fprod1p  27325  fprodeq0  27333  fallfacval4  27393  bpoly4  28049  ltflcei  28263  leceifl  28264  mblfinlem2  28273  dvtanlem  28285  itg2addnclem2  28288  mettrifi  28497  cntotbnd  28539  lzunuz  28951  lzenom  28953  diophin  28956  irrapxlem1  29008  irrapxlem2  29009  irrapxlem3  29010  irrapxlem4  29011  pellexlem5  29019  pellexlem6  29020  rmspecfund  29095  rmxypos  29135  ltrmynn0  29136  ltrmxnn0  29137  ltrmy  29140  rmyeq0  29141  rmyeq  29142  lermy  29143  rmyabs  29146  jm2.24nn  29147  jm2.17a  29148  jm2.17b  29149  jm2.17c  29150  jm2.24  29151  rmygeid  29152  acongrep  29168  fzmaxdif  29169  acongeq  29171  jm2.22  29189  jm2.23  29190  jm2.26lem3  29195  jm2.27a  29199  jm3.1lem1  29211  jm3.1lem3  29213  expdiophlem1  29215  hashgcdlem  29410  fmul01  29606  fmul01lt1lem1  29610  fmul01lt1lem2  29611  climsuselem1  29626  climsuse  29627  stoweidlem3  29644  stoweidlem11  29652  stoweidlem20  29661  stoweidlem26  29667  stoweidlem34  29675  stoweidlem59  29700  stirlinglem5  29719  2elfz2melfz  30048  elfzelfzlble  30055  fsummsndifre  30083  modfsummods  30090  clwwisshclwwlem1  30315  difelfznle  30334  numclwwlk5  30551
  Copyright terms: Public domain W3C validator