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  9691  difgtsumgt  9725  eluzmn  9944  irraddap  10063  addlelt  10186  xaddf  10263  xaddval  10264  xleaddadd  10306  lincmble  10423  zltaddlt1le  10427  elincfzoext  10628  zssinfcl  10682  exbtwnzlemstep  10699  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnrelemcalc  10707  flqaddz  10753  btwnzge0  10756  2tnp1ge0ge0  10757  flhalf  10758  modqltm1p1mod  10834  expnbnd  11122  nn0opthlem2d  11181  ccatalpha  11403  remim  11647  remullem  11658  sq01  11682  caucvgrelemcau  11768  caucvgre  11769  cvg1nlemcxze  11770  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniqlem  11782  resqrexlem1arp  11793  resqrexlemp1rp  11794  resqrexlemf1  11796  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  abs00ap  11850  absext  11851  absrele  11872  abstri  11893  abs3lem  11900  amgm2  11907  qdenre  11991  maxabsle  11993  maxabslemlub  11996  maxabslemval  11997  maxcl  11999  maxltsup  12007  bdtrilem  12030  bdtri  12031  xrbdtri  12067  mulcn2  12103  fsumabs  12257  cvgratnnlembern  12315  eirraplem  12569  ltoddhalfle  12685  divalglemnqt  12712  bitscmp  12750  4sqlem12  13210  4sqlem15  13213  4sqlem16  13214  2expltfac  13248  ballotfilemsgt1  13312  ballotfilemsel1i  13314  xblss2ps  15630  cnopnap  15837  maxcncf  15841  mincncf  15842  ivthinclemlopn  15862  ivthinclemuopn  15864  hoverb  15874  ivthdichlem  15877  limcimolemlt  15890  efltlemlt  16000  efap1p  16005  cosq23lt0  16060  cosordlem  16077  pellexlem2  16230  efnnfsumcl  16239  efchtqdvds  16265  chtublem  16295  chtqub  16296  bposlem7  16317  bposlem9  16319  lgsdirprm  16358  gausslemma2dlem1a  16382  2sqlem8  16447  qdencn  17278  repiecelem  17280  trilpolemeq1  17296