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

Theorem readdcli 11225
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 11189 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3mp2an 690 1 (𝐴 + 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  (class class class)co 7405  cr 11105   + caddc 11109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11167
This theorem depends on definitions:  df-bi 206  df-an 397
This theorem is referenced by:  resubcli  11518  eqneg  11930  ledivp1i  12135  ltdivp1i  12136  nnne0  12242  2re  12282  3re  12288  4re  12292  5re  12295  6re  12298  7re  12301  8re  12304  9re  12307  10re  12692  numltc  12699  nn0opthlem2  14225  hashunlei  14381  hashge2el2dif  14437  abs3lemi  15353  ef01bndlem  16123  divalglem6  16337  log2ub  26443  mumullem2  26673  bposlem8  26783  dchrvmasumlem2  26990  ex-fl  29689  norm-ii-i  30377  norm3lem  30389  nmoptrii  31334  bdophsi  31336  unierri  31344  staddi  31486  stadd3i  31488  dp2ltc  32040  dpmul4  32067  ballotlem2  33475  hgt750lem  33651  poimirlem16  36492  itg2addnclem3  36529  fdc  36601  remul02  41274  sn-0tie0  41308  pellqrex  41602  stirlinglem11  44786  fouriersw  44933  zm1nn  45996  evengpoap3  46453
  Copyright terms: Public domain W3C validator