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

Theorem readdcli 10645
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 10609 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3mp2an 688 1 (𝐴 + 𝐵) ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7148  cr 10525   + caddc 10529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10587
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  resubcli  10937  eqneg  11349  ledivp1i  11554  ltdivp1i  11555  nnne0  11660  2re  11700  3re  11706  4re  11710  5re  11713  6re  11716  7re  11719  8re  11722  9re  11725  10re  12106  numltc  12113  nn0opthlem2  13619  hashunlei  13776  hashge2el2dif  13828  abs3lemi  14760  ef01bndlem  15527  divalglem6  15739  log2ub  25441  mumullem2  25671  bposlem8  25781  dchrvmasumlem2  25988  ex-fl  28140  norm-ii-i  28828  norm3lem  28840  nmoptrii  29785  bdophsi  29787  unierri  29795  staddi  29937  stadd3i  29939  dp2ltc  30477  dpmul4  30504  ballotlem2  31632  hgt750lem  31808  poimirlem16  34775  itg2addnclem3  34812  fdc  34888  remul02  39100  pellqrex  39341  stirlinglem11  42235  fouriersw  42382  zm1nn  43368  evengpoap3  43796
  Copyright terms: Public domain W3C validator