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

Theorem readdcl 9074
Description: Alias for ax-addrcl 9052, for naming consistency with readdcli 9104. (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 9052 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726  (class class class)co 6082   RRcr 8990    + caddc 8994
This theorem is referenced by:  0re  9092  readdcli  9104  readdcld  9116  axltadd  9150  peano2re  9240  00id  9242  resubcl  9366  ltaddsub  9503  leaddsub  9505  ltleadd  9512  recex  9655  recp1lt1  9909  recreclt  9910  cju  9997  nnge1  10027  addltmul  10204  avglt1  10206  avglt2  10207  avgle1  10208  avgle2  10209  uzindOLD  10365  irradd  10599  rpnnen1lem5  10605  rpaddcl  10633  xaddf  10811  xaddnemnf  10821  xaddnepnf  10822  xnegdi  10828  xaddass  10829  xadddilem  10874  iooshf  10990  ge0addcl  11010  icoshft  11020  icoshftf1o  11021  iccshftr  11031  flbi2  11225  modcyc  11277  modadd1  11279  serfre  11353  sermono  11356  serge0  11378  serle  11379  bernneq  11506  faclbnd6  11591  hashfun  11701  readd  11932  imadd  11940  elicc4abs  12124  rddif  12145  absrdbnd  12146  caubnd2  12162  mulcn2  12390  o1add  12408  o1sub  12410  lo1add  12421  fsumrecl  12529  efgt1  12718  pythagtriplem12  13201  pythagtriplem14  13203  pythagtriplem16  13205  resubdrg  16751  prdsxmetlem  18399  xmeter  18464  bl2ioo  18824  ioo2bl  18825  ioo2blex  18826  blssioo  18827  reperf  18851  reconnlem2  18859  opnreen  18863  icopnfcnv  18968  pcoass  19050  pjthlem1  19339  ovolun  19396  shft2rab  19405  volun  19440  mbfaddlem  19553  i1fadd  19588  itg1addlem4  19592  itg2monolem1  19643  ply1divex  20060  psercnlem1  20342  reefgim  20367  tangtx  20414  efif1olem1  20445  efif1olem2  20446  efif1o  20449  relogmul  20487  argimgt0  20508  logimul  20510  ang180lem1  20652  atanlogaddlem  20754  atanlogsublem  20756  atantan  20764  ressatans  20775  emcllem6  20840  basellem9  20872  ppiub  20989  bposlem5  21073  bposlem6  21074  bposlem9  21077  chpchtlim  21174  mulog2sumlem1  21229  mulog2sumlem2  21230  selberglem2  21241  pntrmax  21259  pntpbnd1a  21280  pntpbnd2  21282  pntibndlem3  21287  pntlemb  21292  pntlemk  21301  readdsubgo  21942  pjhthlem1  22894  staddi  23750  stadd3i  23752  cdj1i  23937  cdj3lem2b  23941  cdj3i  23945  addltmulALT  23950  remulg  24271  raddcn  24316  subfacval3  24876  rerisefaccl  25334  rprisefaccl  25340  axsegconlem7  25863  axsegconlem9  25865  axsegconlem10  25866  supadd  26239  mblfinlem2  26245  mblfinlem3  26246  ismblfin  26248  ftc1anclem3  26283  ftc1anclem4  26284  ftc1anclem6  26286  ftc1anclem7  26287  ftc1anclem8  26288  cntotbnd  26506  pellexlem5  26897  stoweidlem59  27785  stirlinglem10  27809  leaddsuble  28092  2leaddle2  28093  2elfz2melfz  28118  ccatsymb  28180  swrdswrdlem  28199  swrdccatin2  28211  2cshw2lem1  28253  2cshwmod  28258  cshweqrep  28275  dp2cl  28513
This theorem was proved from axioms:  ax-addrcl 9052
  Copyright terms: Public domain W3C validator