Theorem readdcld 8362

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 8312	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6088  ℝcr 8185   + caddc 8189

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 8283

This theorem is used by:  ltadd2  8755  leadd1  8766  le2add  8780  lt2add  8781  lesub2  8793  ltsub2  8795  lesub3d  8899  gt0add  8910  reapadd1  8933  apadd1  8945  mulext1  8949  recexaplem2  8989  recp1lt1  9238  cju  9300  peano5nni  9317  peano2nn  9326  div4p1lem1div2  9571  peano2z  9692  difgtsumgt  9726  eluzmn  9945  irraddap  10064  addlelt  10187  xaddf  10264  xaddval  10265  xleaddadd  10307  lincmble  10424  zltaddlt1le  10428  elincfzoext  10629  zssinfcl  10683  exbtwnzlemstep  10700  exbtwnz  10703  rebtwn2zlemstep  10705  rebtwn2z  10707  qbtwnrelemcalc  10708  flqaddz  10754  btwnzge0  10757  2tnp1ge0ge0  10758  flhalf  10759  modqltm1p1mod  10835  expnbnd  11123  nn0opthlem2d  11182  ccatalpha  11404  remim  11648  remullem  11659  sq01  11683  caucvgrelemcau  11769  caucvgre  11770  cvg1nlemcxze  11771  cvg1nlemcau  11773  cvg1nlemres  11774  recvguniqlem  11783  resqrexlem1arp  11794  resqrexlemp1rp  11795  resqrexlemf1  11797  resqrexlemfp1  11798  resqrexlemover  11799  resqrexlemdec  11800  resqrexlemlo  11802  resqrexlemcalc1  11803  resqrexlemcalc2  11804  resqrexlemnm  11807  resqrexlemcvg  11808  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemga  11812  abs00ap  11851  absext  11852  absrele  11873  abstri  11894  abs3lem  11901  amgm2  11908  qdenre  11992  maxabsle  11994  maxabslemlub  11997  maxabslemval  11998  maxcl  12000  maxltsup  12008  bdtrilem  12031  bdtri  12032  xrbdtri  12068  mulcn2  12104  fsumabs  12258  cvgratnnlembern  12316  eirraplem  12570  ltoddhalfle  12686  divalglemnqt  12713  bitscmp  12751  4sqlem12  13211  4sqlem15  13214  4sqlem16  13215  2expltfac  13249  ballotfilemsgt1  13313  ballotfilemsel1i  13315  xblss2ps  15642  cnopnap  15849  maxcncf  15853  mincncf  15854  ivthinclemlopn  15874  ivthinclemuopn  15876  hoverb  15886  ivthdichlem  15889  limcimolemlt  15902  efltlemlt  16012  efap1p  16017  cosq23lt0  16072  cosordlem  16089  pellexlem2  16242  efnnfsumcl  16251  efchtqdvds  16277  chtublem  16307  chtqub  16308  bposlem7  16329  bposlem9  16331  lgsdirprm  16370  gausslemma2dlem1a  16394  2sqlem8  16459  qdencn  17290  repiecelem  17292  trilpolemeq1  17308