Theorem readdcld 8355

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178   + caddc 8182

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

This theorem is used by:  ltadd2  8747  leadd1  8758  le2add  8772  lt2add  8773  lesub2  8785  ltsub2  8787  lesub3d  8891  gt0add  8902  reapadd1  8925  apadd1  8937  mulext1  8941  recexaplem2  8981  recp1lt1  9230  cju  9292  peano5nni  9308  peano2nn  9317  div4p1lem1div2  9561  peano2z  9682  difgtsumgt  9716  eluzmn  9930  addlelt  10171  xaddf  10248  xaddval  10249  xleaddadd  10291  lincmble  10408  zltaddlt1le  10412  elincfzoext  10613  zssinfcl  10667  exbtwnzlemstep  10684  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2z  10691  qbtwnrelemcalc  10692  flqaddz  10734  btwnzge0  10737  2tnp1ge0ge0  10738  flhalf  10739  modqltm1p1mod  10815  expnbnd  11103  nn0opthlem2d  11161  ccatalpha  11383  remim  11627  remullem  11638  sq01  11662  caucvgrelemcau  11748  caucvgre  11749  cvg1nlemcxze  11750  cvg1nlemcau  11752  cvg1nlemres  11753  recvguniqlem  11762  resqrexlem1arp  11773  resqrexlemp1rp  11774  resqrexlemf1  11776  resqrexlemfp1  11777  resqrexlemover  11778  resqrexlemdec  11779  resqrexlemlo  11781  resqrexlemcalc1  11782  resqrexlemcalc2  11783  resqrexlemnm  11786  resqrexlemcvg  11787  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemga  11791  abs00ap  11830  absext  11831  absrele  11851  abstri  11872  abs3lem  11879  amgm2  11886  qdenre  11970  maxabsle  11972  maxabslemlub  11975  maxabslemval  11976  maxcl  11978  maxltsup  11986  bdtrilem  12007  bdtri  12008  xrbdtri  12044  mulcn2  12080  fsumabs  12234  cvgratnnlembern  12292  eirraplem  12546  ltoddhalfle  12662  divalglemnqt  12689  bitscmp  12727  4sqlem12  13183  4sqlem15  13186  4sqlem16  13187  2expltfac  13220  ballotfilemsgt1  13256  ballotfilemsel1i  13258  xblss2ps  15507  cnopnap  15714  maxcncf  15718  mincncf  15719  ivthinclemlopn  15739  ivthinclemuopn  15741  hoverb  15751  ivthdichlem  15754  limcimolemlt  15767  efltlemlt  15877  efap1p  15882  cosq23lt0  15937  cosordlem  15953  pellexlem2  16098  lgsdirprm  16165  gausslemma2dlem1a  16189  2sqlem8  16254  qdencn  17084  repiecelem  17086  trilpolemeq1  17101