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

Theorem readdcl 9006
Description: Alias for ax-addrcl 8984, for naming consistency with readdcli 9036. (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 8984 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 1717  (class class class)co 6020   RRcr 8922    + caddc 8926
This theorem is referenced by:  0re  9024  readdcli  9036  readdcld  9048  axltadd  9082  peano2re  9171  00id  9173  resubcl  9297  ltaddsub  9434  leaddsub  9436  ltleadd  9443  recex  9586  recp1lt1  9840  recreclt  9841  cju  9928  nnge1  9958  addltmul  10135  avglt1  10137  avglt2  10138  avgle1  10139  avgle2  10140  uzindOLD  10296  irradd  10530  rpnnen1lem5  10536  rpaddcl  10564  xaddf  10742  xaddnemnf  10752  xaddnepnf  10753  xnegdi  10759  xaddass  10760  xadddilem  10805  iooshf  10921  ge0addcl  10941  icoshft  10951  icoshftf1o  10952  iccshftr  10962  flbi2  11151  modcyc  11203  modadd1  11205  serfre  11279  sermono  11282  serge0  11304  serle  11305  bernneq  11432  faclbnd6  11517  hashfun  11627  readd  11858  imadd  11866  elicc4abs  12050  rddif  12071  absrdbnd  12072  caubnd2  12088  mulcn2  12316  o1add  12334  o1sub  12336  lo1add  12347  fsumrecl  12455  efgt1  12644  pythagtriplem12  13127  pythagtriplem14  13129  pythagtriplem16  13131  resubdrg  16673  prdsxmetlem  18306  xmeter  18353  bl2ioo  18694  ioo2bl  18695  ioo2blex  18696  blssioo  18697  reperf  18721  reconnlem2  18729  opnreen  18733  icopnfcnv  18838  pcoass  18920  pjthlem1  19205  ovolun  19262  shft2rab  19271  volun  19306  mbfaddlem  19419  i1fadd  19454  itg1addlem4  19458  itg2monolem1  19509  ply1divex  19926  psercnlem1  20208  reefgim  20233  tangtx  20280  efif1olem1  20311  efif1olem2  20312  efif1o  20315  relogmul  20353  argimgt0  20374  logimul  20376  ang180lem1  20518  atanlogaddlem  20620  atanlogsublem  20622  atantan  20630  ressatans  20641  emcllem6  20706  basellem9  20738  ppiub  20855  bposlem5  20939  bposlem6  20940  bposlem9  20943  chpchtlim  21040  mulog2sumlem1  21095  mulog2sumlem2  21096  selberglem2  21107  pntrmax  21125  pntpbnd1a  21146  pntpbnd2  21148  pntibndlem3  21153  pntlemb  21158  pntlemk  21167  readdsubgo  21789  pjhthlem1  22741  staddi  23597  stadd3i  23599  cdj1i  23784  cdj3lem2b  23788  cdj3i  23792  addltmulALT  23797  remulg  24086  raddcn  24119  subfacval3  24654  rerisefaccl  25101  rprisefaccl  25107  axsegconlem7  25576  axsegconlem9  25578  axsegconlem10  25579  supadd  25948  itgaddnclem2  25964  cntotbnd  26196  pellexlem5  26587  stoweidlem59  27476  stirlinglem10  27500  dp2cl  27858
This theorem was proved from axioms:  ax-addrcl 8984
  Copyright terms: Public domain W3C validator