Theorem readdcld 8355

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

Hypotheses

Ref	Expression
recnd.1	|- ( ph -> A e. RR )
readdcld.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
readdcld	|- ( ph -> ( A + B ) e. RR )

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		readdcld.2	. 2 |- ( ph -> B e. RR )
3		readdcl 8305	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A + B ) e. RR )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   RRcr 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  8748  leadd1  8759  le2add  8773  lt2add  8774  lesub2  8786  ltsub2  8788  lesub3d  8892  gt0add  8903  reapadd1  8926  apadd1  8938  mulext1  8942  recexaplem2  8982  recp1lt1  9231  cju  9293  peano5nni  9309  peano2nn  9318  div4p1lem1div2  9563  peano2z  9684  difgtsumgt  9718  eluzmn  9937  irraddap  10056  addlelt  10179  xaddf  10256  xaddval  10257  xleaddadd  10299  lincmble  10416  zltaddlt1le  10420  elincfzoext  10621  zssinfcl  10675  exbtwnzlemstep  10692  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnrelemcalc  10700  flqaddz  10745  btwnzge0  10748  2tnp1ge0ge0  10749  flhalf  10750  modqltm1p1mod  10826  expnbnd  11114  nn0opthlem2d  11173  ccatalpha  11395  remim  11639  remullem  11650  sq01  11674  caucvgrelemcau  11760  caucvgre  11761  cvg1nlemcxze  11762  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniqlem  11774  resqrexlem1arp  11785  resqrexlemp1rp  11786  resqrexlemf1  11788  resqrexlemfp1  11789  resqrexlemover  11790  resqrexlemdec  11791  resqrexlemlo  11793  resqrexlemcalc1  11794  resqrexlemcalc2  11795  resqrexlemnm  11798  resqrexlemcvg  11799  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemga  11803  abs00ap  11842  absext  11843  absrele  11864  abstri  11885  abs3lem  11892  amgm2  11899  qdenre  11983  maxabsle  11985  maxabslemlub  11988  maxabslemval  11989  maxcl  11991  maxltsup  11999  bdtrilem  12021  bdtri  12022  xrbdtri  12058  mulcn2  12094  fsumabs  12248  cvgratnnlembern  12306  eirraplem  12560  ltoddhalfle  12676  divalglemnqt  12703  bitscmp  12741  4sqlem12  13201  4sqlem15  13204  4sqlem16  13205  2expltfac  13239  ballotfilemsgt1  13303  ballotfilemsel1i  13305  xblss2ps  15554  cnopnap  15761  maxcncf  15765  mincncf  15766  ivthinclemlopn  15786  ivthinclemuopn  15788  hoverb  15798  ivthdichlem  15801  limcimolemlt  15814  efltlemlt  15924  efap1p  15929  cosq23lt0  15984  cosordlem  16000  pellexlem2  16149  lgsdirprm  16251  gausslemma2dlem1a  16275  2sqlem8  16340  qdencn  17170  repiecelem  17172  trilpolemeq1  17187