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

Theorem readdcli 9909
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 9875 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3mp2an 703 1 (𝐴 + 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  (class class class)co 6527  cr 9791   + caddc 9795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9853
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  resubcli  10194  eqneg  10594  ledivp1i  10798  ltdivp1i  10799  2re  10937  3re  10941  4re  10944  5re  10946  6re  10948  7re  10950  8re  10952  9re  10954  10reOLD  10956  numltc  11360  nn0opthlem2  12873  hashunlei  13024  hashge2el2dif  13067  abs3lemi  13943  ef01bndlem  14699  divalglem6  14905  log2ub  24393  mumullem2  24623  bposlem8  24733  dchrvmasumlem2  24904  ex-fl  26462  norm-ii-i  27184  norm3lem  27196  nmoptrii  28143  bdophsi  28145  unierri  28153  staddi  28295  stadd3i  28297  ballotlem2  29683  poimirlem16  32391  itg2addnclem3  32429  fdc  32507  pellqrex  36257  stirlinglem11  38774  fouriersw  38921  evengpoap3  40013  zm1nn  40168
  Copyright terms: Public domain W3C validator