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

Theorem readdcli 10309
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 10272 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3mp2an 683 1 (𝐴 + 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  (class class class)co 6842  cr 10188   + caddc 10192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10250
This theorem depends on definitions:  df-bi 198  df-an 385
This theorem is referenced by:  resubcli  10597  eqneg  10999  ledivp1i  11203  ltdivp1i  11204  2re  11346  3re  11352  4re  11357  5re  11361  6re  11365  7re  11369  8re  11373  9re  11377  10re  11759  numltc  11767  nn0opthlem2  13260  hashunlei  13413  hashge2el2dif  13463  abs3lemi  14434  ef01bndlem  15196  divalglem6  15403  log2ub  24967  mumullem2  25197  bposlem8  25307  dchrvmasumlem2  25478  ex-fl  27763  norm-ii-i  28450  norm3lem  28462  nmoptrii  29409  bdophsi  29411  unierri  29419  staddi  29561  stadd3i  29563  dp2ltc  30042  dpmul4  30069  ballotlem2  30998  hgt750lem  31180  poimirlem16  33849  itg2addnclem3  33886  fdc  33963  pellqrex  38121  stirlinglem11  40938  fouriersw  41085  zm1nn  42051  evengpoap3  42363
  Copyright terms: Public domain W3C validator