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

Theorem readdcli 9598
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 9564 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3mp2an 672 1  |-  ( A  +  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762  (class class class)co 6275   RRcr 9480    + caddc 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9542
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ltadd2i  9704  resubcli  9870  eqneg  10253  ledivp1i  10460  ltdivp1i  10461  2re  10594  3re  10598  4re  10601  5re  10603  6re  10605  7re  10607  8re  10609  9re  10611  10re  10613  numltc  10985  nn0opthlem2  12304  hashunlei  12435  hashge2el2dif  12474  abs3lemi  13191  ef01bndlem  13769  divalglem6  13904  log2ub  23001  mumullem2  23175  bposlem8  23287  dchrvmasumlem2  23404  ex-fl  24831  norm-ii-i  25716  norm3lem  25728  normpar2i  25735  nmoptrii  26675  bdophsi  26677  unierri  26685  staddi  26827  stadd3i  26829  ballotlem2  28053  itg2addnclem3  29632  fdc  29828  pellqrex  30406  stirlinglem11  31339  fouriersw  31487  zm1nn  31749
  Copyright terms: Public domain W3C validator