Theorem readdcld 8361

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 8311	. 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 6088   RRcr 8184   + caddc 8188

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

This theorem is used by:  ltadd2  8754  leadd1  8765  le2add  8779  lt2add  8780  lesub2  8792  ltsub2  8794  lesub3d  8898  gt0add  8909  reapadd1  8932  apadd1  8944  mulext1  8948  recexaplem2  8988  recp1lt1  9237  cju  9299  peano5nni  9316  peano2nn  9325  div4p1lem1div2  9570  peano2z  9689  difgtsumgt  9723  eluzmn  9943  irraddap  10062  addlelt  10185  xaddf  10262  xaddval  10263  xleaddadd  10305  lincmble  10422  zltaddlt1le  10426  elincfzoext  10627  zssinfcl  10681  exbtwnzlemstep  10698  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnrelemcalc  10706  flqaddz  10752  btwnzge0  10755  2tnp1ge0ge0  10756  flhalf  10757  modqltm1p1mod  10833  expnbnd  11121  nn0opthlem2d  11180  ccatalpha  11402  remim  11646  remullem  11657  sq01  11681  caucvgrelemcau  11767  caucvgre  11768  cvg1nlemcxze  11769  cvg1nlemcau  11771  cvg1nlemres  11772  recvguniqlem  11781  resqrexlem1arp  11792  resqrexlemp1rp  11793  resqrexlemf1  11795  resqrexlemfp1  11796  resqrexlemover  11797  resqrexlemdec  11798  resqrexlemlo  11800  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  abs00ap  11849  absext  11850  absrele  11871  abstri  11892  abs3lem  11899  amgm2  11906  qdenre  11990  maxabsle  11992  maxabslemlub  11995  maxabslemval  11996  maxcl  11998  maxltsup  12006  bdtrilem  12029  bdtri  12030  xrbdtri  12066  mulcn2  12102  fsumabs  12256  cvgratnnlembern  12314  eirraplem  12568  ltoddhalfle  12684  divalglemnqt  12711  bitscmp  12749  4sqlem12  13209  4sqlem15  13212  4sqlem16  13213  2expltfac  13247  ballotfilemsgt1  13311  ballotfilemsel1i  13313  xblss2ps  15647  cnopnap  15854  maxcncf  15858  mincncf  15859  ivthinclemlopn  15879  ivthinclemuopn  15881  hoverb  15891  ivthdichlem  15894  limcimolemlt  15907  efltlemlt  16017  efap1p  16022  cosq23lt0  16077  cosordlem  16094  pellexlem2  16247  efnnfsumcl  16256  efchtqdvds  16282  chtublem  16312  chtqub  16313  bposlem7  16334  bposlem9  16336  lgsdirprm  16375  gausslemma2dlem1a  16399  2sqlem8  16464  qdencn  17295  repiecelem  17297  trilpolemeq1  17313