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

Theorem readdcld 9619
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
readdcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
readdcld  |-  ( ph  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 readdcl 9571 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767  (class class class)co 6282   RRcr 9487    + caddc 9491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9549
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ltadd2  9684  readdcan  9749  addid1  9755  leadd1  10016  le2add  10030  lesub2  10043  cju  10528  rpnnen1lem5  11208  xralrple  11400  xov1plusxeqvd  11662  fladdz  11922  flhalf  11926  fldiv  11951  modaddmodup  12014  modaddmodlo  12015  discr1  12266  discr  12267  2cshw  12740  remim  12909  remullem  12920  sqrlem7  13041  absrele  13100  abstri  13122  abs3lem  13130  amgm2  13161  mulcn2  13377  o1add  13395  o1sub  13397  lo1add  13408  caucvgrlem  13454  iseraltlem2  13464  iseraltlem3  13465  fsumabs  13574  o1fsum  13586  climcndslem2  13621  tanhlt1  13752  eirrlem  13794  ruclem1  13821  ruclem2  13822  ruclem3  13823  bitscmp  13943  sadcaddlem  13962  sadasslem  13975  smuval2  13987  prmreclem4  14292  4sqlem5  14315  4sqlem6  14316  4sqlem12  14329  4sqlem15  14332  4sqlem16  14333  2expltfac  14431  cshwshashlem2  14435  chfacfscmul0  19126  chfacfscmulgsum  19128  chfacfpmmul0  19130  chfacfpmmulgsum  19132  prdsxmetlem  20606  xblss2ps  20639  metustexhalfOLD  20801  metustexhalf  20802  nrmmetd  20830  ngptgp  20885  nlmvscnlem2  20929  nlmvscnlem1  20930  nmotri  20981  nghmplusg  20982  blcvx  21038  iccntr  21061  icccmplem2  21063  reconnlem2  21067  metdcnlem  21076  metnrmlem3  21100  cnllycmp  21191  lebnumii  21201  tchcphlem1  21413  ipcnlem2  21419  ipcnlem1  21420  csbren  21561  trirn  21562  minveclem2  21576  minveclem3b  21578  minveclem4  21582  ivthlem2  21599  ovolgelb  21626  ovollb2lem  21634  ovolunlem1a  21642  ovolunlem1  21643  ovolfiniun  21647  ovoliunlem1  21648  ovoliunlem2  21649  ovolshftlem1  21655  ovolscalem1  21659  ovolicopnf  21670  ismbl2  21673  nulmbl2  21682  unmbl  21683  voliunlem2  21696  ioombl1lem2  21704  ioombl1lem4  21706  ioombl1  21707  ioorcl2  21716  uniioombllem1  21725  uniioombllem3  21729  uniioombllem4  21730  uniioombllem5  21731  uniioombl  21733  opnmbllem  21745  volcn  21750  itg1addlem4  21841  mbfi1fseqlem4  21860  mbfi1fseqlem6  21862  itg2splitlem  21890  itg2split  21891  itg2monolem3  21894  itg2addlem  21900  ibladdlem  21961  itgaddlem1  21964  itgaddlem2  21965  iblabslem  21969  iblabs  21970  dvferm1lem  22120  dvferm2lem  22122  dvlip2  22131  lhop1lem  22149  lhop1  22150  lhop  22152  dvcnvrelem1  22153  dvcnvrelem2  22154  dvcnvre  22155  dvcvx  22156  dvfsumlem3  22164  dvfsumlem4  22165  dvfsum2  22170  ftc1lem4  22175  coemullem  22381  ulmbdd  22527  ulmcn  22528  ulmdvlem1  22529  radcnvle  22549  pserdvlem1  22556  pserdv  22558  abelthlem7  22567  pilem2  22581  pilem3  22582  cosordlem  22651  abslogle  22731  logccv  22772  cxpaddle  22854  ang180lem2  22870  heron  22897  atanlogaddlem  22972  atans2  22990  cxp2limlem  23033  scvxcvx  23043  jensenlem2  23045  amgmlem  23047  logdiflbnd  23052  harmonicbnd4  23068  fsumharmonic  23069  ftalem5  23078  efnnfsumcl  23104  efchtdvds  23161  chtublem  23214  chtub  23215  logfaclbnd  23225  perfectlem2  23233  bcmono  23280  bposlem7  23293  bposlem9  23295  lgsdirprm  23332  2sqlem8  23375  vmadivsumb  23396  rplogsumlem1  23397  dchrisumlem2  23403  dchrvmasumlem2  23411  dchrvmasumiflem1  23414  dchrisum0re  23426  dchrisum0lem1b  23428  mulog2sumlem1  23447  mulog2sumlem2  23448  logsqvma2  23456  log2sumbnd  23457  selberglem2  23459  selbergb  23462  selberg2b  23465  chpdifbndlem1  23466  chpdifbndlem2  23467  selberg3lem2  23471  selberg3  23472  selberg4lem1  23473  selberg4  23474  pntrsumbnd2  23480  selberg3r  23482  selberg34r  23484  pntsf  23486  pntrlog2bndlem1  23490  pntrlog2bndlem2  23491  pntrlog2bndlem4  23493  pntrlog2bndlem5  23494  pntrlog2bndlem6  23496  pntrlog2bnd  23497  pntpbnd1a  23498  pntpbnd2  23500  pntibndlem2a  23503  pntibndlem2  23504  pntibndlem3  23505  pntlemg  23511  pntlemr  23515  pntlemk  23519  pntlemo  23520  pntlem3  23522  abvcxp  23528  padicabv  23543  ostth2lem2  23547  ostth3  23551  brbtwn2  23884  axsegconlem8  23903  axsegconlem10  23905  axpaschlem  23919  axpasch  23920  axeuclidlem  23941  axcontlem2  23944  vacn  25280  smcnlem  25283  ubthlem2  25463  minvecolem2  25467  minvecolem3  25468  minvecolem4  25472  minvecolem5  25473  nmoptrii  26689  hstle  26825  staddi  26841  stadd3i  26843  lt2addrd  27231  nndiffz1  27264  fsumrp0cl  27347  sqsscirc1  27526  cnre2csqlem  27528  tpr2rico  27530  nexple  27645  dya2iocress  27885  dya2iocbrsiga  27886  dya2icobrsiga  27887  dya2icoseg  27888  dya2iocucvr  27895  sxbrsigalem2  27897  fibp1  27980  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemsgt1  28089  ballotlemsel1i  28091  eluzmn  28131  plymulx0  28144  lgamgulmlem3  28213  lgamgulmlem4  28214  lgamgulmlem5  28215  lgamgulmlem6  28216  lgambdd  28219  lgamucov  28220  regamcl  28243  rescon  28331  faclim  28748  supaddc  29618  supadd  29619  heicant  29626  opnmbllem0  29627  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  mbfposadd  29639  itg2addnclem  29643  itg2addnclem3  29645  itg2addnc  29646  itg2gt0cn  29647  ibladdnclem  29648  itgaddnclem1  29650  itgaddnclem2  29651  iblabsnclem  29655  iblabsnc  29656  iblmulc2nc  29657  ftc1cnnclem  29665  ftc1anclem4  29670  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  areacirclem5  29688  mettrifi  29853  isbnd3  29883  ssbnd  29887  cntotbnd  29895  heibor1lem  29908  bfplem2  29922  rrnequiv  29934  iccbnd  29939  pellexlem2  30370  pell1qrge1  30410  pell14qrgapw  30416  pellqrexplicit  30417  pellqrex  30419  pellfundge  30422  pellfundgt1  30423  rmspecfund  30449  rmxycomplete  30457  ltrmynn0  30490  jm2.24nn  30501  jm2.24  30505  fzmaxdif  30523  jm2.26lem3  30547  jm3.1lem2  30564  areaquad  30789  hashnzfzclim  30827  hashssle  31074  lt3addmuld  31078  absnpncan2d  31079  fperiodmullem  31080  lt4addmuld  31083  absnpncan3d  31084  eliooshift  31105  iccshift  31122  iooshift  31126  climinf  31148  climsuselem1  31149  sumnnodd  31172  lptre2pt  31182  addlimc  31190  0ellimcdiv  31191  limclner  31193  fperdvper  31248  dvdivbd  31253  dvbdfbdioo  31260  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  iblsplit  31284  iblspltprt  31291  itgspltprt  31297  itgiccshift  31298  itgperiod  31299  itgsbtaddcnst  31300  stoweidlem1  31301  stoweidlem11  31311  stoweidlem13  31313  stoweidlem14  31314  stoweidlem20  31320  stoweidlem21  31321  stoweidlem26  31326  stoweidlem44  31344  stoweidlem60  31360  wallispilem3  31367  wallispilem4  31368  wallispilem5  31369  wallispi  31370  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem1  31374  stirlinglem3  31376  stirlinglem5  31378  stirlinglem6  31379  stirlinglem7  31380  stirlinglem10  31383  stirlinglem11  31384  stirlinglem12  31385  dirker2re  31392  dirkerval2  31394  dirkerre  31395  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem2  31399  dirkeritg  31402  dirkercncflem1  31403  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem4  31411  fourierdlem5  31412  fourierdlem6  31413  fourierdlem7  31414  fourierdlem9  31416  fourierdlem19  31426  fourierdlem20  31427  fourierdlem26  31433  fourierdlem28  31435  fourierdlem30  31437  fourierdlem35  31442  fourierdlem40  31447  fourierdlem41  31448  fourierdlem42  31449  fourierdlem45  31452  fourierdlem47  31454  fourierdlem48  31455  fourierdlem49  31456  fourierdlem51  31458  fourierdlem53  31460  fourierdlem57  31464  fourierdlem59  31466  fourierdlem60  31467  fourierdlem61  31468  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem66  31473  fourierdlem68  31475  fourierdlem71  31478  fourierdlem72  31479  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem77  31484  fourierdlem78  31485  fourierdlem79  31486  fourierdlem80  31487  fourierdlem81  31488  fourierdlem82  31489  fourierdlem83  31490  fourierdlem84  31491  fourierdlem88  31495  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem92  31499  fourierdlem93  31500  fourierdlem94  31501  fourierdlem95  31502  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  sqwvfoura  31529  sqwvfourb  31530  fouriersw  31532  zm1nn  31794
  Copyright terms: Public domain W3C validator