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

Theorem readdcld 9146
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 9104 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1727  (class class class)co 6110   RRcr 9020    + caddc 9024
This theorem is referenced by:  ltadd2  9208  readdcan  9271  addid1  9277  leadd1  9527  le2add  9541  lesub2  9554  cju  10027  rpnnen1lem5  10635  xralrple  10822  xov1plusxeqvd  11072  fladdz  11258  flhalf  11262  fldiv  11272  discr1  11546  discr  11547  remim  11953  remullem  11964  sqrlem7  12085  absrele  12144  abstri  12165  abs3lem  12173  amgm2  12204  mulcn2  12420  o1add  12438  o1sub  12440  lo1add  12451  caucvgrlem  12497  iseraltlem2  12507  iseraltlem3  12508  fsumabs  12611  o1fsum  12623  climcndslem2  12661  tanhlt1  12792  eirrlem  12834  ruclem1  12861  ruclem2  12862  ruclem3  12863  bitscmp  12981  sadcaddlem  13000  sadasslem  13013  smuval2  13025  prmreclem4  13318  4sqlem5  13341  4sqlem6  13342  4sqlem12  13355  4sqlem15  13358  4sqlem16  13359  2expltfac  13457  prdsxmetlem  18429  xblss2ps  18462  metustexhalfOLD  18624  metustexhalf  18625  nrmmetd  18653  ngptgp  18708  nlmvscnlem2  18752  nlmvscnlem1  18753  nmotri  18804  nghmplusg  18805  blcvx  18860  iccntr  18883  icccmplem2  18885  reconnlem2  18889  metdcnlem  18898  metnrmlem3  18922  cnllycmp  19012  lebnumii  19022  tchcphlem1  19223  ipcnlem2  19229  ipcnlem1  19230  minveclem2  19358  minveclem3b  19360  minveclem4  19364  ivthlem2  19380  ovolgelb  19407  ovollb2lem  19415  ovolunlem1a  19423  ovolunlem1  19424  ovolfiniun  19428  ovoliunlem1  19429  ovoliunlem2  19430  ovolshftlem1  19436  ovolscalem1  19440  ovolicopnf  19451  ismbl2  19454  nulmbl2  19462  unmbl  19463  voliunlem2  19476  ioombl1lem2  19484  ioombl1lem4  19486  ioombl1  19487  ioorcl2  19495  uniioombllem1  19504  uniioombllem3  19508  uniioombllem4  19509  uniioombllem5  19510  uniioombl  19512  opnmbllem  19524  volcn  19529  itg1addlem4  19620  mbfi1fseqlem4  19639  mbfi1fseqlem6  19641  itg2splitlem  19669  itg2split  19670  itg2monolem3  19673  itg2addlem  19679  ibladdlem  19740  itgaddlem1  19743  itgaddlem2  19744  iblabslem  19748  iblabs  19749  dvferm1lem  19899  dvferm2lem  19901  dvlip2  19910  lhop1lem  19928  lhop1  19929  lhop  19931  dvcnvrelem1  19932  dvcnvrelem2  19933  dvcnvre  19934  dvcvx  19935  dvfsumlem3  19943  dvfsumlem4  19944  dvfsum2  19949  ftc1lem4  19954  coemullem  20199  ulmbdd  20345  ulmcn  20346  ulmdvlem1  20347  radcnvle  20367  pserdvlem1  20374  pserdv  20376  abelthlem7  20385  pilem2  20399  pilem3  20400  cosordlem  20464  abslogle  20544  logccv  20585  cxpaddle  20667  ang180lem2  20683  atanlogaddlem  20784  atans2  20802  cxp2limlem  20845  scvxcvx  20855  jensenlem2  20857  amgmlem  20859  logdiflbnd  20864  harmonicbnd4  20880  fsumharmonic  20881  ftalem5  20890  efnnfsumcl  20916  efchtdvds  20973  chtublem  21026  chtub  21027  logfaclbnd  21037  perfectlem2  21045  bcmono  21092  bposlem7  21105  bposlem9  21107  lgsdirprm  21144  2sqlem8  21187  vmadivsumb  21208  rplogsumlem1  21209  dchrisumlem2  21215  dchrvmasumlem2  21223  dchrvmasumiflem1  21226  dchrisum0re  21238  dchrisum0lem1b  21240  mulog2sumlem1  21259  mulog2sumlem2  21260  logsqvma2  21268  log2sumbnd  21269  selberglem2  21271  selbergb  21274  selberg2b  21277  chpdifbndlem1  21278  chpdifbndlem2  21279  selberg3lem2  21283  selberg3  21284  selberg4lem1  21285  selberg4  21286  pntrsumbnd2  21292  selberg3r  21294  selberg34r  21296  pntsf  21298  pntrlog2bndlem1  21302  pntrlog2bndlem2  21303  pntrlog2bndlem4  21305  pntrlog2bndlem5  21306  pntrlog2bndlem6  21308  pntrlog2bnd  21309  pntpbnd1a  21310  pntpbnd2  21312  pntibndlem2a  21315  pntibndlem2  21316  pntibndlem3  21317  pntlemg  21323  pntlemr  21327  pntlemk  21331  pntlemo  21332  pntlem3  21334  abvcxp  21340  padicabv  21355  ostth2lem2  21359  ostth3  21363  vacn  22221  smcnlem  22224  ubthlem2  22404  minvecolem2  22408  minvecolem3  22409  minvecolem4  22413  minvecolem5  22414  nmoptrii  23628  hstle  23764  staddi  23780  stadd3i  23782  lt2addrd  24146  fsumrp0cl  24248  sqsscirc1  24337  cnre2csqlem  24339  tpr2rico  24341  dya2iocress  24655  dya2iocbrsiga  24656  dya2icobrsiga  24657  dya2icoseg  24658  dya2iocucvr  24665  sxbrsigalem2  24667  ballotlemfc0  24781  ballotlemfcc  24782  ballotlemsgt1  24799  ballotlemsel1i  24801  lgamgulmlem3  24846  lgamgulmlem4  24847  lgamgulmlem5  24848  lgamgulmlem6  24849  lgambdd  24852  lgamucov  24853  regamcl  24876  rescon  24964  faclim  25396  brbtwn2  25875  axsegconlem8  25894  axsegconlem10  25896  axpaschlem  25910  axpasch  25911  axeuclidlem  25932  axcontlem2  25935  supaddc  26269  supadd  26270  heicant  26277  opnmbllem0  26278  mblfinlem3  26281  mblfinlem4  26282  ismblfin  26283  mbfposadd  26290  itg2addnclem  26294  itg2addnclem3  26296  itg2addnc  26297  itg2gt0cn  26298  ibladdnclem  26299  itgaddnclem1  26301  itgaddnclem2  26302  iblabsnclem  26306  iblabsnc  26307  iblmulc2nc  26308  ftc1cnnclem  26316  ftc1anclem4  26321  ftc1anclem7  26324  ftc1anclem8  26325  ftc1anc  26326  areacirclem5  26334  csbrn  26494  trirn  26495  mettrifi  26501  isbnd3  26531  ssbnd  26535  cntotbnd  26543  heibor1lem  26556  bfplem2  26570  rrnequiv  26582  iccbnd  26587  pellexlem2  26931  pell1qrge1  26971  pell14qrgapw  26977  pellqrexplicit  26978  pellqrex  26980  pellfundge  26983  pellfundgt1  26984  rmspecfund  27010  rmxycomplete  27018  ltrmynn0  27051  jm2.24nn  27062  jm2.24  27066  fzmaxdif  27084  jm2.26lem3  27110  jm3.1lem2  27127  climinf  27746  climsuselem1  27747  stoweidlem1  27764  stoweidlem11  27774  stoweidlem13  27776  stoweidlem14  27777  stoweidlem20  27783  stoweidlem21  27784  stoweidlem26  27789  stoweidlem44  27807  stoweidlem60  27823  wallispilem3  27830  wallispilem4  27831  wallispilem5  27832  wallispi  27833  wallispi2lem1  27834  wallispi2lem2  27835  stirlinglem1  27837  stirlinglem3  27839  stirlinglem5  27841  stirlinglem6  27842  stirlinglem7  27843  stirlinglem10  27846  stirlinglem11  27847  stirlinglem12  27848  cshwssizelem4a  28341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9082
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator