Theorem readdcld 7578

Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
readdcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		readdcl 7529	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 404	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1439  (class class class)co 5666  ℝcr 7410   + caddc 7414

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107  ax-addrcl 7503

This theorem is referenced by:  ltadd2  7958  leadd1  7969  le2add  7983  lt2add  7984  lesub2  7996  ltsub2  7998  gt0add  8111  reapadd1  8134  apadd1  8146  mulext1  8150  recexaplem2  8182  recp1lt1  8421  cju  8482  peano5nni  8486  peano2nn  8495  div4p1lem1div2  8730  peano2z  8847  addlelt  9300  zltaddlt1le  9484  exbtwnzlemstep  9720  exbtwnz  9723  rebtwn2zlemstep  9725  rebtwn2z  9727  qbtwnrelemcalc  9728  flqaddz  9765  btwnzge0  9768  2tnp1ge0ge0  9769  flhalf  9770  modqltm1p1mod  9844  expnbnd  10138  nn0opthlem2d  10190  remim  10355  remullem  10366  caucvgrelemcau  10474  caucvgre  10475  cvg1nlemcxze  10476  cvg1nlemcau  10478  cvg1nlemres  10479  recvguniqlem  10488  resqrexlem1arp  10499  resqrexlemp1rp  10500  resqrexlemf1  10502  resqrexlemfp1  10503  resqrexlemover  10504  resqrexlemdec  10505  resqrexlemlo  10507  resqrexlemcalc1  10508  resqrexlemcalc2  10509  resqrexlemnm  10512  resqrexlemcvg  10513  resqrexlemoverl  10515  resqrexlemglsq  10516  resqrexlemga  10517  abs00ap  10556  absext  10557  absrele  10577  abstri  10598  abs3lem  10605  amgm2  10612  qdenre  10696  maxabsle  10698  maxabslemlub  10701  maxabslemval  10702  maxcl  10704  maxltsup  10712  mulcn2  10762  fsumabs  10920  cvgratnnlembern  10978  eirraplem  11125  ltoddhalfle  11232  divalglemnqt  11259  zssinfcl  11283  qdencn  12187