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

Theorem readdcld 9071
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 9029 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721  (class class class)co 6040   RRcr 8945    + caddc 8949
This theorem is referenced by:  ltadd2  9133  readdcan  9196  addid1  9202  leadd1  9452  le2add  9466  lesub2  9479  cju  9952  rpnnen1lem5  10560  xralrple  10747  xov1plusxeqvd  10997  fladdz  11182  flhalf  11186  fldiv  11196  discr1  11470  discr  11471  remim  11877  remullem  11888  sqrlem7  12009  absrele  12068  abstri  12089  abs3lem  12097  amgm2  12128  mulcn2  12344  o1add  12362  o1sub  12364  lo1add  12375  caucvgrlem  12421  iseraltlem2  12431  iseraltlem3  12432  fsumabs  12535  o1fsum  12547  climcndslem2  12585  tanhlt1  12716  eirrlem  12758  ruclem1  12785  ruclem2  12786  ruclem3  12787  bitscmp  12905  sadcaddlem  12924  sadasslem  12937  smuval2  12949  prmreclem4  13242  4sqlem5  13265  4sqlem6  13266  4sqlem12  13279  4sqlem15  13282  4sqlem16  13283  2expltfac  13381  prdsxmetlem  18351  xblss2ps  18384  metustexhalfOLD  18546  metustexhalf  18547  nrmmetd  18575  ngptgp  18630  nlmvscnlem2  18674  nlmvscnlem1  18675  nmotri  18726  nghmplusg  18727  blcvx  18782  iccntr  18805  icccmplem2  18807  reconnlem2  18811  metdcnlem  18820  metnrmlem3  18844  cnllycmp  18934  lebnumii  18944  tchcphlem1  19145  ipcnlem2  19151  ipcnlem1  19152  minveclem2  19280  minveclem3b  19282  minveclem4  19286  ivthlem2  19302  ovolgelb  19329  ovollb2lem  19337  ovolunlem1a  19345  ovolunlem1  19346  ovolfiniun  19350  ovoliunlem1  19351  ovoliunlem2  19352  ovolshftlem1  19358  ovolscalem1  19362  ovolicopnf  19373  ismbl2  19376  nulmbl2  19384  unmbl  19385  voliunlem2  19398  ioombl1lem2  19406  ioombl1lem4  19408  ioombl1  19409  ioorcl2  19417  uniioombllem1  19426  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombl  19434  opnmbllem  19446  volcn  19451  itg1addlem4  19544  mbfi1fseqlem4  19563  mbfi1fseqlem6  19565  itg2splitlem  19593  itg2split  19594  itg2monolem3  19597  itg2addlem  19603  ibladdlem  19664  itgaddlem1  19667  itgaddlem2  19668  iblabslem  19672  iblabs  19673  dvferm1lem  19821  dvferm2lem  19823  dvlip2  19832  lhop1lem  19850  lhop1  19851  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  dvcvx  19857  dvfsumlem3  19865  dvfsumlem4  19866  dvfsum2  19871  ftc1lem4  19876  coemullem  20121  ulmbdd  20267  ulmcn  20268  ulmdvlem1  20269  radcnvle  20289  pserdvlem1  20296  pserdv  20298  abelthlem7  20307  pilem2  20321  pilem3  20322  cosordlem  20386  abslogle  20466  logccv  20507  cxpaddle  20589  ang180lem2  20605  atanlogaddlem  20706  atans2  20724  cxp2limlem  20767  scvxcvx  20777  jensenlem2  20779  amgmlem  20781  logdiflbnd  20786  harmonicbnd4  20802  fsumharmonic  20803  ftalem5  20812  efnnfsumcl  20838  efchtdvds  20895  chtublem  20948  chtub  20949  logfaclbnd  20959  perfectlem2  20967  bcmono  21014  bposlem7  21027  bposlem9  21029  lgsdirprm  21066  2sqlem8  21109  vmadivsumb  21130  rplogsumlem1  21131  dchrisumlem2  21137  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0re  21160  dchrisum0lem1b  21162  mulog2sumlem1  21181  mulog2sumlem2  21182  logsqvma2  21190  log2sumbnd  21191  selberglem2  21193  selbergb  21196  selberg2b  21199  chpdifbndlem1  21200  chpdifbndlem2  21201  selberg3lem2  21205  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrsumbnd2  21214  selberg3r  21216  selberg34r  21218  pntsf  21220  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2a  21237  pntibndlem2  21238  pntibndlem3  21239  pntlemg  21245  pntlemr  21249  pntlemk  21253  pntlemo  21254  pntlem3  21256  abvcxp  21262  padicabv  21277  ostth2lem2  21281  ostth3  21285  vacn  22143  smcnlem  22146  ubthlem2  22326  minvecolem2  22330  minvecolem3  22331  minvecolem4  22335  minvecolem5  22336  nmoptrii  23550  hstle  23686  staddi  23702  stadd3i  23704  lt2addrd  24068  fsumrp0cl  24170  sqsscirc1  24259  cnre2csqlem  24261  tpr2rico  24263  dya2iocress  24577  dya2iocbrsiga  24578  dya2icobrsiga  24579  dya2icoseg  24580  dya2iocucvr  24587  sxbrsigalem2  24589  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsgt1  24721  ballotlemsel1i  24723  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgambdd  24774  lgamucov  24775  regamcl  24798  rescon  24886  faclim  25313  brbtwn2  25748  axsegconlem8  25767  axsegconlem10  25769  axpaschlem  25783  axpasch  25784  axeuclidlem  25805  axcontlem2  25808  supaddc  26137  supadd  26138  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  mbfposadd  26153  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  itgaddnclem2  26163  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  ftc1cnnclem  26177  areacirclem6  26186  csbrn  26346  trirn  26347  mettrifi  26353  isbnd3  26383  ssbnd  26387  cntotbnd  26395  heibor1lem  26408  bfplem2  26422  rrnequiv  26434  iccbnd  26439  pellexlem2  26783  pell1qrge1  26823  pell14qrgapw  26829  pellqrexplicit  26830  pellqrex  26832  pellfundge  26835  pellfundgt1  26836  rmspecfund  26862  rmxycomplete  26870  ltrmynn0  26903  jm2.24nn  26914  jm2.24  26918  fzmaxdif  26936  jm2.26lem3  26962  jm3.1lem2  26979  climinf  27599  climsuselem1  27600  stoweidlem1  27617  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem20  27636  stoweidlem21  27637  stoweidlem26  27642  stoweidlem44  27660  stoweidlem60  27676  wallispilem3  27683  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem1  27690  stirlinglem3  27692  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 9007
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator