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  8747  leadd1  8758  le2add  8772  lt2add  8773  lesub2  8785  ltsub2  8787  gt0add  8901  reapadd1  8924  apadd1  8936  mulext1  8940  recexaplem2  8980  recp1lt1  9229  cju  9291  peano5nni  9307  peano2nn  9316  div4p1lem1div2  9559  peano2z  9680  difgtsumgt  9714  eluzmn  9928  addlelt  10169  xaddf  10246  xaddval  10247  xleaddadd  10289  lincmble  10406  zltaddlt1le  10410  elincfzoext  10611  zssinfcl  10665  exbtwnzlemstep  10682  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnrelemcalc  10690  flqaddz  10732  btwnzge0  10735  2tnp1ge0ge0  10736  flhalf  10737  modqltm1p1mod  10813  expnbnd  11101  nn0opthlem2d  11159  ccatalpha  11381  remim  11625  remullem  11636  sq01  11660  caucvgrelemcau  11746  caucvgre  11747  cvg1nlemcxze  11748  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniqlem  11760  resqrexlem1arp  11771  resqrexlemp1rp  11772  resqrexlemf1  11774  resqrexlemfp1  11775  resqrexlemover  11776  resqrexlemdec  11777  resqrexlemlo  11779  resqrexlemcalc1  11780  resqrexlemcalc2  11781  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  abs00ap  11828  absext  11829  absrele  11849  abstri  11870  abs3lem  11877  amgm2  11884  qdenre  11968  maxabsle  11970  maxabslemlub  11973  maxabslemval  11974  maxcl  11976  maxltsup  11984  bdtrilem  12005  bdtri  12006  xrbdtri  12042  mulcn2  12078  fsumabs  12232  cvgratnnlembern  12290  eirraplem  12544  ltoddhalfle  12660  divalglemnqt  12687  bitscmp  12725  4sqlem12  13181  4sqlem15  13184  4sqlem16  13185  2expltfac  13218  ballotfilemsgt1  13254  ballotfilemsel1i  13256  xblss2ps  15505  cnopnap  15712  maxcncf  15716  mincncf  15717  ivthinclemlopn  15737  ivthinclemuopn  15739  hoverb  15749  ivthdichlem  15752  limcimolemlt  15765  efltlemlt  15875  cosq23lt0  15934  cosordlem  15950  pellexlem2  16092  lgsdirprm  16153  gausslemma2dlem1a  16177  2sqlem8  16242  qdencn  17072  repiecelem  17074  trilpolemeq1  17089