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

Theorem readdcli 9105
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 9075 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3mp2an 655 1  |-  ( A  +  B )  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1726  (class class class)co 6083   RRcr 8991    + caddc 8995
This theorem is referenced by:  ltadd2i  9206  resubcli  9365  eqneg  9736  ledivp1i  9938  ltdivp1i  9939  2re  10071  3re  10073  4re  10075  5re  10077  6re  10078  7re  10079  8re  10080  9re  10081  10re  10082  numltc  10404  nn0opthlem2  11564  hashunlei  11686  abs3lemi  12215  ef01bndlem  12787  divalglem6  12920  log2ub  20791  mumullem2  20965  bposlem8  21077  dchrvmasumlem2  21194  ex-fl  21757  norm-ii-i  22641  norm3lem  22653  normpar2i  22660  nmoptrii  23599  bdophsi  23601  unierri  23609  staddi  23751  stadd3i  23753  ballotlem2  24748  itg2addnclem3  26260  fdc  26451  pellqrex  26944  stirlinglem11  27811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 9053
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator