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

Theorem readdcli 9658
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 9624 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3mp2an 677 1  |-  ( A  +  B )  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869  (class class class)co 6303   RRcr 9540    + caddc 9544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9602
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  ltadd2iOLD  9768  resubcli  9938  eqneg  10329  ledivp1i  10534  ltdivp1i  10535  2re  10681  3re  10685  4re  10688  5re  10690  6re  10692  7re  10694  8re  10696  9re  10698  10re  10700  numltc  11073  nn0opthlem2  12456  hashunlei  12596  hashge2el2dif  12635  abs3lemi  13466  ef01bndlem  14231  divalglem6  14371  log2ub  23867  mumullem2  24099  bposlem8  24211  dchrvmasumlem2  24328  ex-fl  25889  norm-ii-i  26782  norm3lem  26794  nmoptrii  27739  bdophsi  27741  unierri  27749  staddi  27891  stadd3i  27893  ballotlem2  29323  poimirlem16  31914  itg2addnclem3  31953  fdc  32032  pellqrex  35690  stirlinglem11  37810  fouriersw  37959  zm1nn  38782
  Copyright terms: Public domain W3C validator