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

Theorem readdcl 8836
Description: Alias for ax-addrcl 8814, for naming consistency with readdcli 8866. (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 8814 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696  (class class class)co 5874   RRcr 8752    + caddc 8756
This theorem is referenced by:  0re  8854  readdcli  8866  readdcld  8878  axltadd  8912  peano2re  9001  00id  9003  resubcl  9127  ltaddsub  9264  leaddsub  9266  ltleadd  9273  recex  9416  recp1lt1  9670  recreclt  9671  cju  9758  nnge1  9788  addltmul  9963  avglt1  9965  avglt2  9966  avgle1  9967  avgle2  9968  uzindOLD  10122  irradd  10356  rpnnen1lem5  10362  rpaddcl  10390  xaddf  10567  xaddnemnf  10577  xaddnepnf  10578  xnegdi  10584  xaddass  10585  xadddilem  10630  iooshf  10744  ge0addcl  10764  icoshft  10774  icoshftf1o  10775  iccshftr  10785  flbi2  10963  modcyc  11015  modadd1  11017  serfre  11091  sermono  11094  serge0  11116  serle  11117  bernneq  11243  faclbnd6  11328  hashfun  11405  readd  11627  imadd  11635  elicc4abs  11819  rddif  11840  absrdbnd  11841  caubnd2  11857  mulcn2  12085  o1add  12103  o1sub  12105  lo1add  12116  fsumrecl  12223  efgt1  12412  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem16  12899  resubdrg  16439  prdsxmetlem  17948  xmeter  17995  bl2ioo  18314  ioo2bl  18315  ioo2blex  18316  blssioo  18317  reperf  18340  reconnlem2  18348  opnreen  18352  icopnfcnv  18456  pcoass  18538  pjthlem1  18817  ovolun  18874  shft2rab  18883  volun  18918  mbfaddlem  19031  i1fadd  19066  itg1addlem4  19070  itg2monolem1  19121  ply1divex  19538  psercnlem1  19817  reefgim  19842  tangtx  19889  efif1olem1  19920  efif1olem2  19921  efif1o  19924  relogmul  19961  argimgt0  19982  logimul  19984  ang180lem1  20123  atanlogaddlem  20225  atanlogsublem  20227  atantan  20235  ressatans  20246  emcllem6  20310  basellem9  20342  ppiub  20459  bposlem5  20543  bposlem6  20544  bposlem9  20547  chpchtlim  20644  mulog2sumlem1  20699  mulog2sumlem2  20700  selberglem2  20711  pntrmax  20729  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem3  20757  pntlemb  20762  pntlemk  20771  readdsubgo  21036  pjhthlem1  21986  staddi  22842  stadd3i  22844  cdj1i  23029  cdj3lem2b  23033  cdj3i  23037  addltmulALT  23042  raddcn  23317  fsumrp0cl  23349  esumpcvgval  23461  subfacval3  23735  axsegconlem7  24623  axsegconlem9  24625  axsegconlem10  24626  supadd  24996  itgaddnclem2  25010  truni1  25608  cbci  25611  msr4  25709  msra3  25712  iintlem1  25713  trdom  25716  trran  25717  trnij  25718  cnvtr  25719  claddrvr  25751  cntotbnd  26623  pellexlem5  27021  stoweidlem1  27853  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem26  27878  stoweidlem44  27896  stoweidlem59  27911  stoweidlem60  27912  stirlinglem10  27935  dp2cl  28493
This theorem was proved from axioms:  ax-addrcl 8814
  Copyright terms: Public domain W3C validator