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

Theorem readdcld 9644
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1
readdcld.2
Assertion
Ref Expression
readdcld

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2
2 readdcld.2 . 2
3 readdcl 9596 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  (class class class)co 6296   cr 9512   caddc 9516
This theorem is referenced by:  ltadd2  9709  readdcan  9775  addid1  9781  leadd1  10045  le2add  10059  lesub2  10072  cju  10557  rpnnen1lem5  11241  xralrple  11433  xov1plusxeqvd  11695  fladdz  11958  flhalf  11962  fldiv  11987  modaddmodup  12050  modaddmodlo  12051  discr1  12302  discr  12303  2cshw  12781  remim  12950  remullem  12961  sqrlem7  13082  absrele  13141  abstri  13163  abs3lem  13171  amgm2  13202  mulcn2  13418  o1add  13436  o1sub  13438  lo1add  13449  caucvgrlem  13495  iseraltlem2  13505  iseraltlem3  13506  fsumabs  13615  o1fsum  13627  climcndslem2  13662  tanhlt1  13895  eirrlem  13937  ruclem1  13964  ruclem2  13965  ruclem3  13966  bitscmp  14088  sadcaddlem  14107  sadasslem  14120  smuval2  14132  prmreclem4  14437  4sqlem5  14460  4sqlem6  14461  4sqlem12  14474  4sqlem15  14477  4sqlem16  14478  2expltfac  14577  cshwshashlem2  14581  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  prdsxmetlem  20871  xblss2ps  20904  metustexhalfOLD  21066  metustexhalf  21067  nrmmetd  21095  ngptgp  21150  nlmvscnlem2  21194  nlmvscnlem1  21195  nmotri  21246  nghmplusg  21247  blcvx  21303  iccntr  21326  icccmplem2  21328  reconnlem2  21332  metdcnlem  21341  metnrmlem3  21365  cnllycmp  21456  lebnumii  21466  tchcphlem1  21678  ipcnlem2  21684  ipcnlem1  21685  csbren  21826  trirn  21827  minveclem2  21841  minveclem3b  21843  minveclem4  21847  ivthlem2  21864  ovolgelb  21891  ovollb2lem  21899  ovolunlem1a  21907  ovolunlem1  21908  ovolfiniun  21912  ovoliunlem1  21913  ovoliunlem2  21914  ovolshftlem1  21920  ovolscalem1  21924  ovolicopnf  21935  ismbl2  21938  nulmbl2  21947  unmbl  21948  voliunlem2  21961  ioombl1lem2  21969  ioombl1lem4  21971  ioombl1  21972  ioorcl2  21981  uniioombllem1  21990  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombl  21998  opnmbllem  22010  volcn  22015  itg1addlem4  22106  mbfi1fseqlem4  22125  mbfi1fseqlem6  22127  itg2splitlem  22155  itg2split  22156  itg2monolem3  22159  itg2addlem  22165  ibladdlem  22226  itgaddlem1  22229  itgaddlem2  22230  iblabslem  22234  iblabs  22235  dvferm1lem  22385  dvferm2lem  22387  dvlip2  22396  lhop1lem  22414  lhop1  22415  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvcvx  22421  dvfsumlem3  22429  dvfsumlem4  22430  dvfsum2  22435  ftc1lem4  22440  coemullem  22647  ulmbdd  22793  ulmcn  22794  ulmdvlem1  22795  radcnvle  22815  pserdvlem1  22822  pserdv  22824  abelthlem7  22833  pilem2  22847  pilem3  22848  cosordlem  22918  abslogle  23003  logccv  23044  cxpaddle  23126  ang180lem2  23142  heron  23169  atanlogaddlem  23244  atans2  23262  cxp2limlem  23305  scvxcvx  23315  jensenlem2  23317  amgmlem  23319  logdiflbnd  23324  harmonicbnd4  23340  fsumharmonic  23341  ftalem5  23350  efnnfsumcl  23376  efchtdvds  23433  chtublem  23486  chtub  23487  logfaclbnd  23497  perfectlem2  23505  bcmono  23552  bposlem7  23565  bposlem9  23567  lgsdirprm  23604  2sqlem8  23647  chpchtlim  23664  vmadivsumb  23668  rplogsumlem1  23669  dchrisumlem2  23675  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  dchrisum0re  23698  dchrisum0lem1b  23700  mulog2sumlem1  23719  mulog2sumlem2  23720  logsqvma2  23728  log2sumbnd  23729  selberglem2  23731  selbergb  23734  selberg2b  23737  chpdifbndlem1  23738  chpdifbndlem2  23739  selberg3lem2  23743  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrsumbnd2  23752  selberg3r  23754  selberg34r  23756  pntsf  23758  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem2a  23775  pntibndlem2  23776  pntibndlem3  23777  pntlemg  23783  pntlemr  23787  pntlemk  23791  pntlemo  23792  pntlem3  23794  abvcxp  23800  padicabv  23815  ostth2lem2  23819  ostth3  23823  brbtwn2  24208  axsegconlem8  24227  axsegconlem10  24229  axpaschlem  24243  axpasch  24244  axeuclidlem  24265  axcontlem2  24268  vacn  25604  smcnlem  25607  ubthlem2  25787  minvecolem2  25791  minvecolem3  25792  minvecolem4  25796  minvecolem5  25797  nmoptrii  27013  hstle  27149  staddi  27165  stadd3i  27167  lt2addrd  27563  nndiffz1  27596  bhmafibid1  27632  fsumrp0cl  27685  sqsscirc1  27890  cnre2csqlem  27892  tpr2rico  27894  nexple  28005  dya2iocress  28245  dya2iocbrsiga  28246  dya2icobrsiga  28247  dya2icoseg  28248  dya2iocucvr  28255  sxbrsigalem2  28257  fibp1  28340  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsgt1  28449  ballotlemsel1i  28451  eluzmn  28491  plymulx0  28504  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgambdd  28579  lgamucov  28580  regamcl  28603  rescon  28691  faclim  29171  supaddc  30041  supadd  30042  heicant  30049  opnmbllem0  30050  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  mbfposadd  30062  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem1  30073  itgaddnclem2  30074  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  ftc1cnnclem  30088  ftc1anclem4  30093  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem5  30111  mettrifi  30250  isbnd3  30280  ssbnd  30284  cntotbnd  30292  heibor1lem  30305  bfplem2  30319  rrnequiv  30331  iccbnd  30336  pellexlem2  30766  pell1qrge1  30806  pell14qrgapw  30812  pellqrexplicit  30813  pellqrex  30815  pellfundge  30818  pellfundgt1  30819  rmspecfund  30845  rmxycomplete  30853  ltrmynn0  30886  jm2.24nn  30897  jm2.24  30901  fzmaxdif  30919  jm2.26lem3  30943  jm3.1lem2  30960  areaquad  31184  hashnzfzclim  31227  binomcxplemnotnn0  31261  zltlesub  31468  lt3addmuld  31501  absnpncan2d  31502  fperiodmullem  31503  lt4addmuld  31506  absnpncan3d  31507  leadd12dd  31521  eliooshift  31541  iccshift  31558  iooshift  31562  fsumnncl  31572  climinf  31612  climsuselem1  31613  sumnnodd  31636  lptre2pt  31646  addlimc  31654  0ellimcdiv  31655  limclner  31657  fperdvper  31715  dvdivbd  31720  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvxpaek  31737  dvnmul  31740  iblsplit  31765  iblspltprt  31772  itgspltprt  31778  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem1  31783  stoweidlem11  31793  stoweidlem13  31795  stoweidlem14  31796  stoweidlem20  31802  stoweidlem21  31803  stoweidlem26  31808  stoweidlem44  31826  stoweidlem60  31842  wallispilem3  31849  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  stirlinglem1  31856  stirlinglem3  31858  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  dirker2re  31874  dirkerval2  31876  dirkerre  31877  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkeritg  31884  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem5  31894  fourierdlem6  31895  fourierdlem7  31896  fourierdlem9  31898  fourierdlem10  31899  fourierdlem18  31907  fourierdlem19  31908  fourierdlem20  31909  fourierdlem26  31915  fourierdlem28  31917  fourierdlem30  31919  fourierdlem35  31924  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem47  31936  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem53  31942  fourierdlem57  31946  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem66  31955  fourierdlem68  31957  fourierdlem71  31960  fourierdlem72  31961  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem80  31969  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem84  31973  fourierdlem87  31976  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem94  31983  fourierdlem95  31984  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  zm1nn  32325  imo72b2lem0  37982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9574
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator