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

Theorem readdcli 9639
Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
Hypotheses
Ref Expression
recni.1  |-  A  e.  RR
axri.2  |-  B  e.  RR
Assertion
Ref Expression
readdcli  |-  ( A  +  B )  e.  RR

Proof of Theorem readdcli
StepHypRef Expression
1 recni.1 . 2  |-  A  e.  RR
2 axri.2 . 2  |-  B  e.  RR
3 readdcl 9605 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3mp2an 670 1  |-  ( A  +  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842  (class class class)co 6278   RRcr 9521    + caddc 9525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9583
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  ltadd2iOLD  9748  resubcli  9917  eqneg  10305  ledivp1i  10511  ltdivp1i  10512  2re  10646  3re  10650  4re  10653  5re  10655  6re  10657  7re  10659  8re  10661  9re  10663  10re  10665  numltc  11039  nn0opthlem2  12393  hashunlei  12532  hashge2el2dif  12570  abs3lemi  13391  ef01bndlem  14128  divalglem6  14265  log2ub  23605  mumullem2  23835  bposlem8  23947  dchrvmasumlem2  24064  ex-fl  25585  norm-ii-i  26468  norm3lem  26480  nmoptrii  27426  bdophsi  27428  unierri  27436  staddi  27578  stadd3i  27580  ballotlem2  28933  itg2addnclem3  31441  fdc  31520  pellqrex  35176  stirlinglem11  37234  fouriersw  37382  zm1nn  37957
  Copyright terms: Public domain W3C validator