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

Theorem readdcli 11177
Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
Hypotheses
Ref Expression
recni.1 𝐴 ∈ ℝ
axri.2 𝐵 ∈ ℝ
Assertion
Ref Expression
readdcli (𝐴 + 𝐵) ∈ ℝ

Proof of Theorem readdcli
StepHypRef Expression
1 recni.1 . 2 𝐴 ∈ ℝ
2 axri.2 . 2 𝐵 ∈ ℝ
3 readdcl 11141 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3mp2an 691 1 (𝐴 + 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7362  cr 11057   + caddc 11061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11119
This theorem depends on definitions:  df-bi 206  df-an 398
This theorem is referenced by:  resubcli  11470  eqneg  11882  ledivp1i  12087  ltdivp1i  12088  nnne0  12194  2re  12234  3re  12240  4re  12244  5re  12247  6re  12250  7re  12253  8re  12256  9re  12259  10re  12644  numltc  12651  nn0opthlem2  14176  hashunlei  14332  hashge2el2dif  14386  abs3lemi  15302  ef01bndlem  16073  divalglem6  16287  log2ub  26315  mumullem2  26545  bposlem8  26655  dchrvmasumlem2  26862  ex-fl  29433  norm-ii-i  30121  norm3lem  30133  nmoptrii  31078  bdophsi  31080  unierri  31088  staddi  31230  stadd3i  31232  dp2ltc  31785  dpmul4  31812  ballotlem2  33128  hgt750lem  33304  poimirlem16  36123  itg2addnclem3  36160  fdc  36233  remul02  40903  sn-0tie0  40937  pellqrex  41231  stirlinglem11  44399  fouriersw  44546  zm1nn  45608  evengpoap3  46065
  Copyright terms: Public domain W3C validator