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

Theorem readdcld 9107
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 9065 . 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 1725  (class class class)co 6073   RRcr 8981    + caddc 8985
This theorem is referenced by:  ltadd2  9169  readdcan  9232  addid1  9238  leadd1  9488  le2add  9502  lesub2  9515  cju  9988  rpnnen1lem5  10596  xralrple  10783  xov1plusxeqvd  11033  fladdz  11219  flhalf  11223  fldiv  11233  discr1  11507  discr  11508  remim  11914  remullem  11925  sqrlem7  12046  absrele  12105  abstri  12126  abs3lem  12134  amgm2  12165  mulcn2  12381  o1add  12399  o1sub  12401  lo1add  12412  caucvgrlem  12458  iseraltlem2  12468  iseraltlem3  12469  fsumabs  12572  o1fsum  12584  climcndslem2  12622  tanhlt1  12753  eirrlem  12795  ruclem1  12822  ruclem2  12823  ruclem3  12824  bitscmp  12942  sadcaddlem  12961  sadasslem  12974  smuval2  12986  prmreclem4  13279  4sqlem5  13302  4sqlem6  13303  4sqlem12  13316  4sqlem15  13319  4sqlem16  13320  2expltfac  13418  prdsxmetlem  18390  xblss2ps  18423  metustexhalfOLD  18585  metustexhalf  18586  nrmmetd  18614  ngptgp  18669  nlmvscnlem2  18713  nlmvscnlem1  18714  nmotri  18765  nghmplusg  18766  blcvx  18821  iccntr  18844  icccmplem2  18846  reconnlem2  18850  metdcnlem  18859  metnrmlem3  18883  cnllycmp  18973  lebnumii  18983  tchcphlem1  19184  ipcnlem2  19190  ipcnlem1  19191  minveclem2  19319  minveclem3b  19321  minveclem4  19325  ivthlem2  19341  ovolgelb  19368  ovollb2lem  19376  ovolunlem1a  19384  ovolunlem1  19385  ovolfiniun  19389  ovoliunlem1  19390  ovoliunlem2  19391  ovolshftlem1  19397  ovolscalem1  19401  ovolicopnf  19412  ismbl2  19415  nulmbl2  19423  unmbl  19424  voliunlem2  19437  ioombl1lem2  19445  ioombl1lem4  19447  ioombl1  19448  ioorcl2  19456  uniioombllem1  19465  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  uniioombl  19473  opnmbllem  19485  volcn  19490  itg1addlem4  19583  mbfi1fseqlem4  19602  mbfi1fseqlem6  19604  itg2splitlem  19632  itg2split  19633  itg2monolem3  19636  itg2addlem  19642  ibladdlem  19703  itgaddlem1  19706  itgaddlem2  19707  iblabslem  19711  iblabs  19712  dvferm1lem  19860  dvferm2lem  19862  dvlip2  19871  lhop1lem  19889  lhop1  19890  lhop  19892  dvcnvrelem1  19893  dvcnvrelem2  19894  dvcnvre  19895  dvcvx  19896  dvfsumlem3  19904  dvfsumlem4  19905  dvfsum2  19910  ftc1lem4  19915  coemullem  20160  ulmbdd  20306  ulmcn  20307  ulmdvlem1  20308  radcnvle  20328  pserdvlem1  20335  pserdv  20337  abelthlem7  20346  pilem2  20360  pilem3  20361  cosordlem  20425  abslogle  20505  logccv  20546  cxpaddle  20628  ang180lem2  20644  atanlogaddlem  20745  atans2  20763  cxp2limlem  20806  scvxcvx  20816  jensenlem2  20818  amgmlem  20820  logdiflbnd  20825  harmonicbnd4  20841  fsumharmonic  20842  ftalem5  20851  efnnfsumcl  20877  efchtdvds  20934  chtublem  20987  chtub  20988  logfaclbnd  20998  perfectlem2  21006  bcmono  21053  bposlem7  21066  bposlem9  21068  lgsdirprm  21105  2sqlem8  21148  vmadivsumb  21169  rplogsumlem1  21170  dchrisumlem2  21176  dchrvmasumlem2  21184  dchrvmasumiflem1  21187  dchrisum0re  21199  dchrisum0lem1b  21201  mulog2sumlem1  21220  mulog2sumlem2  21221  logsqvma2  21229  log2sumbnd  21230  selberglem2  21232  selbergb  21235  selberg2b  21238  chpdifbndlem1  21239  chpdifbndlem2  21240  selberg3lem2  21244  selberg3  21245  selberg4lem1  21246  selberg4  21247  pntrsumbnd2  21253  selberg3r  21255  selberg34r  21257  pntsf  21259  pntrlog2bndlem1  21263  pntrlog2bndlem2  21264  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntrlog2bnd  21270  pntpbnd1a  21271  pntpbnd2  21273  pntibndlem2a  21276  pntibndlem2  21277  pntibndlem3  21278  pntlemg  21284  pntlemr  21288  pntlemk  21292  pntlemo  21293  pntlem3  21295  abvcxp  21301  padicabv  21316  ostth2lem2  21320  ostth3  21324  vacn  22182  smcnlem  22185  ubthlem2  22365  minvecolem2  22369  minvecolem3  22370  minvecolem4  22374  minvecolem5  22375  nmoptrii  23589  hstle  23725  staddi  23741  stadd3i  23743  lt2addrd  24107  fsumrp0cl  24209  sqsscirc1  24298  cnre2csqlem  24300  tpr2rico  24302  dya2iocress  24616  dya2iocbrsiga  24617  dya2icobrsiga  24618  dya2icoseg  24619  dya2iocucvr  24626  sxbrsigalem2  24628  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemsgt1  24760  ballotlemsel1i  24762  lgamgulmlem3  24807  lgamgulmlem4  24808  lgamgulmlem5  24809  lgamgulmlem6  24810  lgambdd  24813  lgamucov  24814  regamcl  24837  rescon  24925  faclim  25357  brbtwn2  25836  axsegconlem8  25855  axsegconlem10  25857  axpaschlem  25871  axpasch  25872  axeuclidlem  25893  axcontlem2  25896  supaddc  26228  supadd  26229  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  mbfposadd  26244  itg2addnclem  26246  itg2addnclem3  26248  itg2addnc  26249  itg2gt0cn  26250  ibladdnclem  26251  itgaddnclem1  26253  itgaddnclem2  26254  iblabsnclem  26258  iblabsnc  26259  iblmulc2nc  26260  ftc1cnnclem  26268  ftc1anclem4  26273  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  areacirclem6  26287  csbrn  26447  trirn  26448  mettrifi  26454  isbnd3  26484  ssbnd  26488  cntotbnd  26496  heibor1lem  26509  bfplem2  26523  rrnequiv  26535  iccbnd  26540  pellexlem2  26884  pell1qrge1  26924  pell14qrgapw  26930  pellqrexplicit  26931  pellqrex  26933  pellfundge  26936  pellfundgt1  26937  rmspecfund  26963  rmxycomplete  26971  ltrmynn0  27004  jm2.24nn  27015  jm2.24  27019  fzmaxdif  27037  jm2.26lem3  27063  jm3.1lem2  27080  climinf  27699  climsuselem1  27700  stoweidlem1  27717  stoweidlem11  27727  stoweidlem13  27729  stoweidlem14  27730  stoweidlem20  27736  stoweidlem21  27737  stoweidlem26  27742  stoweidlem44  27760  stoweidlem60  27776  wallispilem3  27783  wallispilem4  27784  wallispilem5  27785  wallispi  27786  wallispi2lem1  27787  wallispi2lem2  27788  stirlinglem1  27790  stirlinglem3  27792  stirlinglem5  27794  stirlinglem6  27795  stirlinglem7  27796  stirlinglem10  27799  stirlinglem11  27800  stirlinglem12  27801  cshwssizelem4a  28246
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 9043
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator