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

Theorem readdcli 9503
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 9469 . 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 1758  (class class class)co 6193   RRcr 9385    + caddc 9389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9447
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ltadd2i  9609  resubcli  9775  eqneg  10155  ledivp1i  10362  ltdivp1i  10363  2re  10495  3re  10499  4re  10502  5re  10504  6re  10506  7re  10508  8re  10510  9re  10512  10re  10514  numltc  10879  nn0opthlem2  12157  hashunlei  12286  hashge2el2dif  12295  abs3lemi  13008  ef01bndlem  13579  divalglem6  13713  log2ub  22470  mumullem2  22644  bposlem8  22756  dchrvmasumlem2  22873  ex-fl  23799  norm-ii-i  24684  norm3lem  24696  normpar2i  24703  nmoptrii  25643  bdophsi  25645  unierri  25653  staddi  25795  stadd3i  25797  ballotlem2  27008  itg2addnclem3  28586  fdc  28782  pellqrex  29361  stirlinglem11  30020  zm1nn  30609
  Copyright terms: Public domain W3C validator