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

Theorem readdcl 9075
Description: Alias for ax-addrcl 9053, for naming consistency with readdcli 9105. (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 9053 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 6083   RRcr 8991    + caddc 8995
This theorem is referenced by:  0re  9093  readdcli  9105  readdcld  9117  axltadd  9151  peano2re  9241  00id  9243  resubcl  9367  ltaddsub  9504  leaddsub  9506  ltleadd  9513  recex  9656  recp1lt1  9910  recreclt  9911  cju  9998  nnge1  10028  addltmul  10205  avglt1  10207  avglt2  10208  avgle1  10209  avgle2  10210  uzindOLD  10366  irradd  10600  rpnnen1lem5  10606  rpaddcl  10634  xaddf  10812  xaddnemnf  10822  xaddnepnf  10823  xnegdi  10829  xaddass  10830  xadddilem  10875  iooshf  10991  ge0addcl  11011  icoshft  11021  icoshftf1o  11022  iccshftr  11032  flbi2  11226  modcyc  11278  modadd1  11280  serfre  11354  sermono  11357  serge0  11379  serle  11380  bernneq  11507  faclbnd6  11592  hashfun  11702  readd  11933  imadd  11941  elicc4abs  12125  rddif  12146  absrdbnd  12147  caubnd2  12163  mulcn2  12391  o1add  12409  o1sub  12411  lo1add  12422  fsumrecl  12530  efgt1  12719  pythagtriplem12  13202  pythagtriplem14  13204  pythagtriplem16  13206  resubdrg  16752  prdsxmetlem  18400  xmeter  18465  bl2ioo  18825  ioo2bl  18826  ioo2blex  18827  blssioo  18828  reperf  18852  reconnlem2  18860  opnreen  18864  icopnfcnv  18969  pcoass  19051  pjthlem1  19340  ovolun  19397  shft2rab  19406  volun  19441  mbfaddlem  19554  i1fadd  19589  itg1addlem4  19593  itg2monolem1  19644  ply1divex  20061  psercnlem1  20343  reefgim  20368  tangtx  20415  efif1olem1  20446  efif1olem2  20447  efif1o  20450  relogmul  20488  argimgt0  20509  logimul  20511  ang180lem1  20653  atanlogaddlem  20755  atanlogsublem  20757  atantan  20765  ressatans  20776  emcllem6  20841  basellem9  20873  ppiub  20990  bposlem5  21074  bposlem6  21075  bposlem9  21078  chpchtlim  21175  mulog2sumlem1  21230  mulog2sumlem2  21231  selberglem2  21242  pntrmax  21260  pntpbnd1a  21281  pntpbnd2  21283  pntibndlem3  21288  pntlemb  21293  pntlemk  21302  readdsubgo  21943  pjhthlem1  22895  staddi  23751  stadd3i  23753  cdj1i  23938  cdj3lem2b  23942  cdj3i  23946  addltmulALT  23951  remulg  24272  raddcn  24317  subfacval3  24877  rerisefaccl  25335  rprisefaccl  25341  axsegconlem7  25864  axsegconlem9  25866  axsegconlem10  25867  supadd  26240  mblfinlem2  26246  mblfinlem3  26247  ismblfin  26249  ftc1anclem3  26284  ftc1anclem4  26285  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  cntotbnd  26507  pellexlem5  26898  stoweidlem59  27786  stirlinglem10  27810  leaddsuble  28102  2leaddle2  28103  2elfz2melfz  28128  ccatsymb  28199  swrdswrdlem  28220  swrdccatin2  28232  2cshw2lem1  28274  2cshwmod  28279  cshweqrep  28296  dp2cl  28574
This theorem was proved from axioms:  ax-addrcl 9053
  Copyright terms: Public domain W3C validator