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

Theorem readdcl 8820
Description: Alias for ax-addrcl 8798, for naming consistency with readdcli 8850. (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 8798 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 1684  (class class class)co 5858   RRcr 8736    + caddc 8740
This theorem is referenced by:  0re  8838  readdcli  8850  readdcld  8862  axltadd  8896  peano2re  8985  00id  8987  resubcl  9111  ltaddsub  9248  leaddsub  9250  ltleadd  9257  recex  9400  recp1lt1  9654  recreclt  9655  cju  9742  nnge1  9772  addltmul  9947  avglt1  9949  avglt2  9950  avgle1  9951  avgle2  9952  uzindOLD  10106  irradd  10340  rpnnen1lem5  10346  rpaddcl  10374  xaddf  10551  xaddnemnf  10561  xaddnepnf  10562  xnegdi  10568  xaddass  10569  xadddilem  10614  iooshf  10728  ge0addcl  10748  icoshft  10758  icoshftf1o  10759  iccshftr  10769  flbi2  10947  modcyc  10999  modadd1  11001  serfre  11075  sermono  11078  serge0  11100  serle  11101  bernneq  11227  faclbnd6  11312  hashfun  11389  readd  11611  imadd  11619  elicc4abs  11803  rddif  11824  absrdbnd  11825  caubnd2  11841  mulcn2  12069  o1add  12087  o1sub  12089  lo1add  12100  fsumrecl  12207  efgt1  12396  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem16  12883  resubdrg  16423  prdsxmetlem  17932  xmeter  17979  bl2ioo  18298  ioo2bl  18299  ioo2blex  18300  blssioo  18301  reperf  18324  reconnlem2  18332  opnreen  18336  icopnfcnv  18440  pcoass  18522  pjthlem1  18801  ovolun  18858  shft2rab  18867  volun  18902  mbfaddlem  19015  i1fadd  19050  itg1addlem4  19054  itg2monolem1  19105  ply1divex  19522  psercnlem1  19801  reefgim  19826  tangtx  19873  efif1olem1  19904  efif1olem2  19905  efif1o  19908  relogmul  19945  argimgt0  19966  logimul  19968  ang180lem1  20107  atanlogaddlem  20209  atanlogsublem  20211  atantan  20219  ressatans  20230  emcllem6  20294  basellem9  20326  ppiub  20443  bposlem5  20527  bposlem6  20528  bposlem9  20531  chpchtlim  20628  mulog2sumlem1  20683  mulog2sumlem2  20684  selberglem2  20695  pntrmax  20713  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem3  20741  pntlemb  20746  pntlemk  20755  readdsubgo  21020  pjhthlem1  21970  staddi  22826  stadd3i  22828  cdj1i  23013  cdj3lem2b  23017  cdj3i  23021  addltmulALT  23026  raddcn  23302  fsumrp0cl  23334  esumpcvgval  23446  subfacval3  23720  axsegconlem7  24551  axsegconlem9  24553  axsegconlem10  24554  truni1  25505  cbci  25508  msr4  25606  msra3  25609  iintlem1  25610  trdom  25613  trran  25614  trnij  25615  cnvtr  25616  claddrvr  25648  cntotbnd  26520  pellexlem5  26918  stoweidlem1  27750  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem26  27775  stoweidlem44  27793  stoweidlem59  27808  stoweidlem60  27809  stirlinglem10  27832  dp2cl  28239
This theorem was proved from axioms:  ax-addrcl 8798
  Copyright terms: Public domain W3C validator