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

Theorem readdcli 8850
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 8820 . 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 1684  (class class class)co 5858   RRcr 8736    + caddc 8740
This theorem is referenced by:  ltadd2i  8950  resubcli  9109  eqneg  9480  ledivp1i  9682  ltdivp1i  9683  2re  9815  3re  9817  4re  9819  5re  9821  6re  9822  7re  9823  8re  9824  9re  9825  10re  9826  numltc  10144  nn0opthlem2  11284  hashunlei  11377  abs3lemi  11893  ef01bndlem  12464  divalglem6  12597  log2ub  20245  mumullem2  20418  bposlem8  20530  dchrvmasumlem2  20647  ex-fl  20834  norm-ii-i  21716  norm3lem  21728  normpar2i  21735  nmoptrii  22674  bdophsi  22676  unierri  22684  staddi  22826  stadd3i  22828  ballotlem2  23047  fdc  26455  pellqrex  26964  stirlinglem11  27833
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 8798
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator