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

Theorem readdcl 9029
Description: Alias for ax-addrcl 9007, for naming consistency with readdcli 9059. (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 9007 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 6040   RRcr 8945    + caddc 8949
This theorem is referenced by:  0re  9047  readdcli  9059  readdcld  9071  axltadd  9105  peano2re  9195  00id  9197  resubcl  9321  ltaddsub  9458  leaddsub  9460  ltleadd  9467  recex  9610  recp1lt1  9864  recreclt  9865  cju  9952  nnge1  9982  addltmul  10159  avglt1  10161  avglt2  10162  avgle1  10163  avgle2  10164  uzindOLD  10320  irradd  10554  rpnnen1lem5  10560  rpaddcl  10588  xaddf  10766  xaddnemnf  10776  xaddnepnf  10777  xnegdi  10783  xaddass  10784  xadddilem  10829  iooshf  10945  ge0addcl  10965  icoshft  10975  icoshftf1o  10976  iccshftr  10986  flbi2  11179  modcyc  11231  modadd1  11233  serfre  11307  sermono  11310  serge0  11332  serle  11333  bernneq  11460  faclbnd6  11545  hashfun  11655  readd  11886  imadd  11894  elicc4abs  12078  rddif  12099  absrdbnd  12100  caubnd2  12116  mulcn2  12344  o1add  12362  o1sub  12364  lo1add  12375  fsumrecl  12483  efgt1  12672  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem16  13159  resubdrg  16705  prdsxmetlem  18351  xmeter  18416  bl2ioo  18776  ioo2bl  18777  ioo2blex  18778  blssioo  18779  reperf  18803  reconnlem2  18811  opnreen  18815  icopnfcnv  18920  pcoass  19002  pjthlem1  19291  ovolun  19348  shft2rab  19357  volun  19392  mbfaddlem  19505  i1fadd  19540  itg1addlem4  19544  itg2monolem1  19595  ply1divex  20012  psercnlem1  20294  reefgim  20319  tangtx  20366  efif1olem1  20397  efif1olem2  20398  efif1o  20401  relogmul  20439  argimgt0  20460  logimul  20462  ang180lem1  20604  atanlogaddlem  20706  atanlogsublem  20708  atantan  20716  ressatans  20727  emcllem6  20792  basellem9  20824  ppiub  20941  bposlem5  21025  bposlem6  21026  bposlem9  21029  chpchtlim  21126  mulog2sumlem1  21181  mulog2sumlem2  21182  selberglem2  21193  pntrmax  21211  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem3  21239  pntlemb  21244  pntlemk  21253  readdsubgo  21894  pjhthlem1  22846  staddi  23702  stadd3i  23704  cdj1i  23889  cdj3lem2b  23893  cdj3i  23897  addltmulALT  23902  remulg  24223  raddcn  24268  subfacval3  24828  rerisefaccl  25285  rprisefaccl  25291  axsegconlem7  25766  axsegconlem9  25768  axsegconlem10  25769  supadd  26138  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  cntotbnd  26395  pellexlem5  26786  stoweidlem59  27675  stirlinglem10  27699  leaddsuble  27970  swrdswrdlem  28010  dp2cl  28226
This theorem was proved from axioms:  ax-addrcl 9007
  Copyright terms: Public domain W3C validator