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

Theorem readdcli 8866
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 8836 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3mp2an 653 1  |-  ( A  +  B )  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1696  (class class class)co 5874   RRcr 8752    + caddc 8756
This theorem is referenced by:  ltadd2i  8966  resubcli  9125  eqneg  9496  ledivp1i  9698  ltdivp1i  9699  2re  9831  3re  9833  4re  9835  5re  9837  6re  9838  7re  9839  8re  9840  9re  9841  10re  9842  numltc  10160  nn0opthlem2  11300  hashunlei  11393  abs3lemi  11909  ef01bndlem  12480  divalglem6  12613  log2ub  20261  mumullem2  20434  bposlem8  20546  dchrvmasumlem2  20663  ex-fl  20850  norm-ii-i  21732  norm3lem  21744  normpar2i  21751  nmoptrii  22690  bdophsi  22692  unierri  22700  staddi  22842  stadd3i  22844  ballotlem2  23063  faclimlem8  24124  itg2addnc  25005  fdc  26558  pellqrex  27067  stirlinglem11  27936
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 8814
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator