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

Theorem readdcl 9037
Description: Alias for ax-addrcl 9015, for naming consistency with readdcli 9067. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 9015 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721  (class class class)co 6048   RRcr 8953    + caddc 8957
This theorem is referenced by:  0re  9055  readdcli  9067  readdcld  9079  axltadd  9113  peano2re  9203  00id  9205  resubcl  9329  ltaddsub  9466  leaddsub  9468  ltleadd  9475  recex  9618  recp1lt1  9872  recreclt  9873  cju  9960  nnge1  9990  addltmul  10167  avglt1  10169  avglt2  10170  avgle1  10171  avgle2  10172  uzindOLD  10328  irradd  10562  rpnnen1lem5  10568  rpaddcl  10596  xaddf  10774  xaddnemnf  10784  xaddnepnf  10785  xnegdi  10791  xaddass  10792  xadddilem  10837  iooshf  10953  ge0addcl  10973  icoshft  10983  icoshftf1o  10984  iccshftr  10994  flbi2  11187  modcyc  11239  modadd1  11241  serfre  11315  sermono  11318  serge0  11340  serle  11341  bernneq  11468  faclbnd6  11553  hashfun  11663  readd  11894  imadd  11902  elicc4abs  12086  rddif  12107  absrdbnd  12108  caubnd2  12124  mulcn2  12352  o1add  12370  o1sub  12372  lo1add  12383  fsumrecl  12491  efgt1  12680  pythagtriplem12  13163  pythagtriplem14  13165  pythagtriplem16  13167  resubdrg  16713  prdsxmetlem  18359  xmeter  18424  bl2ioo  18784  ioo2bl  18785  ioo2blex  18786  blssioo  18787  reperf  18811  reconnlem2  18819  opnreen  18823  icopnfcnv  18928  pcoass  19010  pjthlem1  19299  ovolun  19356  shft2rab  19365  volun  19400  mbfaddlem  19513  i1fadd  19548  itg1addlem4  19552  itg2monolem1  19603  ply1divex  20020  psercnlem1  20302  reefgim  20327  tangtx  20374  efif1olem1  20405  efif1olem2  20406  efif1o  20409  relogmul  20447  argimgt0  20468  logimul  20470  ang180lem1  20612  atanlogaddlem  20714  atanlogsublem  20716  atantan  20724  ressatans  20735  emcllem6  20800  basellem9  20832  ppiub  20949  bposlem5  21033  bposlem6  21034  bposlem9  21037  chpchtlim  21134  mulog2sumlem1  21189  mulog2sumlem2  21190  selberglem2  21201  pntrmax  21219  pntpbnd1a  21240  pntpbnd2  21242  pntibndlem3  21247  pntlemb  21252  pntlemk  21261  readdsubgo  21902  pjhthlem1  22854  staddi  23710  stadd3i  23712  cdj1i  23897  cdj3lem2b  23901  cdj3i  23905  addltmulALT  23910  remulg  24231  raddcn  24276  subfacval3  24836  rerisefaccl  25293  rprisefaccl  25299  axsegconlem7  25774  axsegconlem9  25776  axsegconlem10  25777  supadd  26146  mblfinlem  26151  mblfinlem2  26152  ismblfin  26154  cntotbnd  26403  pellexlem5  26794  stoweidlem59  27683  stirlinglem10  27707  leaddsuble  27978  swrdswrdlem  28018  dp2cl  28234
This theorem was proved from axioms:  ax-addrcl 9015
  Copyright terms: Public domain W3C validator