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

Theorem readdcli 10266
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 10232 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3mp2an 710 1 (𝐴 + 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2140  (class class class)co 6815  cr 10148   + caddc 10152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10210
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  resubcli  10556  eqneg  10958  ledivp1i  11162  ltdivp1i  11163  2re  11303  3re  11307  4re  11310  5re  11312  6re  11314  7re  11316  8re  11318  9re  11320  10reOLD  11322  numltc  11741  nn0opthlem2  13271  hashunlei  13425  hashge2el2dif  13475  abs3lemi  14369  ef01bndlem  15134  divalglem6  15344  log2ub  24897  mumullem2  25127  bposlem8  25237  dchrvmasumlem2  25408  ex-fl  27637  norm-ii-i  28325  norm3lem  28337  nmoptrii  29284  bdophsi  29286  unierri  29294  staddi  29436  stadd3i  29438  dp2ltc  29925  dpmul4  29953  ballotlem2  30881  hgt750lem  31060  poimirlem16  33757  itg2addnclem3  33795  fdc  33873  pellqrex  37964  stirlinglem11  40823  fouriersw  40970  zm1nn  41845  evengpoap3  42216
  Copyright terms: Public domain W3C validator