Theorem readdcld 10069

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 10019	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   RRcr 9935   + caddc 9939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9997

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  ltadd2  10141  readdcan  10210  addid1  10216  leadd1  10496  le2add  10510  lesub2  10523  lesub3d  10645  supaddc  10990  supadd  10991  cju  11016  div4p1lem1div2  11287  difgtsumgt  11346  eluzmn  11694  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  addlelt  11942  xralrple  12036  xov1plusxeqvd  12318  zltaddlt1le  12324  elincfzoext  12525  fladdz  12626  2tnp1ge0ge0  12630  flhalf  12631  fldiv  12659  modaddmodup  12733  modaddmodlo  12734  addmodlteq  12745  discr1  13000  discr  13001  ccatalpha  13375  2cshw  13559  remim  13857  remullem  13868  sqrlem7  13989  absrele  14048  abstri  14070  abs3lem  14078  amgm2  14109  mulcn2  14326  o1add  14344  o1sub  14346  lo1add  14357  caucvgrlem  14403  iseraltlem2  14413  iseraltlem3  14414  fsumabs  14533  o1fsum  14545  climcndslem2  14582  tanhlt1  14890  eirrlem  14932  ruclem1  14960  ruclem2  14961  ruclem3  14962  ltoddhalfle  15085  bitscmp  15160  sadcaddlem  15179  sadasslem  15192  smuval2  15204  prmreclem4  15623  4sqlem5  15646  4sqlem6  15647  4sqlem12  15660  4sqlem15  15663  4sqlem16  15664  prmgaplem7  15761  prmgaplem8  15762  2expltfac  15799  cshwshashlem2  15803  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  prdsxmetlem  22173  xblss2ps  22206  metustexhalf  22361  nrmmetd  22379  ngptgp  22440  nlmvscnlem2  22489  nlmvscnlem1  22490  nmotri  22543  nghmplusg  22544  blcvx  22601  iccntr  22624  icccmplem2  22626  reconnlem2  22630  metdcnlem  22639  metnrmlem3  22664  cnllycmp  22755  lebnumii  22765  tchcphlem1  23034  ipcnlem2  23043  ipcnlem1  23044  csbren  23182  trirn  23183  minveclem2  23197  minveclem3b  23199  minveclem4  23203  ivthlem2  23221  ovolgelb  23248  ovollb2lem  23256  ovolunlem1a  23264  ovolunlem1  23265  ovolfiniun  23269  ovoliunlem1  23270  ovoliunlem2  23271  ovolshftlem1  23277  ovolscalem1  23281  ovolicopnf  23292  ismbl2  23295  nulmbl2  23304  unmbl  23305  voliunlem2  23319  ioombl1lem2  23327  ioombl1lem4  23329  ioombl1  23330  ioorcl2  23340  uniioombllem1  23349  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  opnmbllem  23369  volcn  23374  itg1addlem4  23466  mbfi1fseqlem4  23485  mbfi1fseqlem6  23487  itg2splitlem  23515  itg2split  23516  itg2monolem3  23519  itg2addlem  23525  ibladdlem  23586  itgaddlem1  23589  itgaddlem2  23590  iblabslem  23594  iblabs  23595  dvferm1lem  23747  dvferm2lem  23749  dvlip2  23758  lhop1lem  23776  lhop1  23777  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvcvx  23783  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  ftc1lem4  23802  coemullem  24006  ulmbdd  24152  ulmcn  24153  ulmdvlem1  24154  radcnvle  24174  pserdvlem1  24181  pserdv  24183  abelthlem7  24192  pilem2  24206  pilem3  24207  cosordlem  24277  abslogle  24364  logccv  24409  cxpaddle  24493  ang180lem2  24540  heron  24565  atanlogaddlem  24640  atans2  24658  cxp2limlem  24702  scvxcvx  24712  jensenlem2  24714  amgmlem  24716  logdiflbnd  24721  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgambdd  24763  lgamucov  24764  regamcl  24787  ftalem5  24803  efnnfsumcl  24829  efchtdvds  24885  chtublem  24936  chtub  24937  logfaclbnd  24947  perfectlem2  24955  bcmono  25002  bposlem7  25015  bposlem9  25017  lgsdirprm  25056  gausslemma2dlem1a  25090  2sqlem8  25151  chpchtlim  25168  vmadivsumb  25172  rplogsumlem1  25173  dchrisumlem2  25179  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0re  25202  dchrisum0lem1b  25204  mulog2sumlem1  25223  mulog2sumlem2  25224  logsqvma2  25232  log2sumbnd  25233  selberglem2  25235  selbergb  25238  selberg2b  25241  chpdifbndlem1  25242  chpdifbndlem2  25243  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrsumbnd2  25256  selberg3r  25258  selberg34r  25260  pntsf  25262  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2a  25279  pntibndlem2  25280  pntibndlem3  25281  pntlemg  25287  pntlemr  25291  pntlemk  25295  pntlemo  25296  pntlem3  25298  abvcxp  25304  padicabv  25319  ostth2lem2  25323  ostth3  25327  brbtwn2  25785  axsegconlem8  25804  axsegconlem10  25806  axpaschlem  25820  axpasch  25821  axeuclidlem  25842  axcontlem2  25845  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  vacn  27549  smcnlem  27552  ubthlem2  27727  minvecolem2  27731  minvecolem3  27732  minvecolem4  27736  minvecolem5  27737  nmoptrii  28953  hstle  29089  staddi  29105  stadd3i  29107  lt2addrd  29516  nndiffz1  29548  bhmafibid1  29644  fsumrp0cl  29695  pmtrto1cl  29849  fzto1st  29853  psgnfzto1st  29855  1smat1  29870  sqsscirc1  29954  cnre2csqlem  29956  tpr2rico  29958  nexple  30071  dya2iocress  30336  dya2iocbrsiga  30337  dya2icobrsiga  30338  dya2icoseg  30339  dya2iocucvr  30346  sxbrsigalem2  30348  omssubaddlem  30361  fibp1  30463  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsgt1  30572  ballotlemsel1i  30574  plymulx0  30624  breprexplemc  30710  breprexp  30711  logdivsqrle  30728  resconn  31228  faclim  31632  dnizphlfeqhlf  32466  dnibndlem4  32471  dnibndlem6  32473  dnibndlem8  32475  dnibndlem9  32476  dnibndlem10  32477  dnibndlem11  32478  dnibndlem13  32480  dnibnd  32481  knoppcnlem4  32486  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2lem1  32500  poimirlem29  33438  heicant  33444  opnmbllem0  33445  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  mbfposadd  33457  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  itgaddnclem2  33469  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  ftc1cnnclem  33483  ftc1anclem4  33488  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem5  33504  mettrifi  33553  isbnd3  33583  ssbnd  33587  cntotbnd  33595  heibor1lem  33608  bfplem2  33622  rrnequiv  33634  iccbnd  33639  pellexlem2  37394  pell1qrge1  37434  pell14qrgapw  37440  pellqrexplicit  37441  pellqrex  37443  pellfundge  37446  pellfundgt1  37447  rmspecfund  37474  rmxycomplete  37482  ltrmynn0  37515  jm2.24nn  37526  jm2.24  37530  fzmaxdif  37548  jm2.26lem3  37568  jm3.1lem2  37585  areaquad  37802  imo72b2lem0  38465  hashnzfzclim  38521  binomcxplemnotnn0  38555  zltlesub  39497  lt3addmuld  39515  absnpncan2d  39516  fperiodmullem  39517  lt4addmuld  39520  absnpncan3d  39521  leadd12dd  39532  supxrgelem  39553  supxrge  39554  ltadd12dd  39559  xralrple2  39570  infxr  39583  infleinflem2  39587  xralrple4  39589  xralrple3  39590  xrralrecnnle  39602  eliooshift  39729  iccshift  39744  iooshift  39748  iooiinicc  39769  iooiinioc  39783  fsumnncl  39803  climinf  39838  climsuselem1  39839  sumnnodd  39862  lptre2pt  39872  addlimc  39880  0ellimcdiv  39881  limclner  39883  climleltrp  39908  liminfltlem  40036  fperdvper  40133  dvdivbd  40138  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvxpaek  40155  dvnmul  40158  iblsplit  40182  iblspltprt  40189  itgspltprt  40195  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  stoweidlem14  40231  stoweidlem20  40237  stoweidlem21  40238  stoweidlem26  40243  stoweidlem44  40261  stoweidlem60  40277  wallispilem3  40284  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem1  40291  stirlinglem3  40293  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  dirker2re  40309  dirkerval2  40311  dirkerre  40312  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem5  40329  fourierdlem6  40330  fourierdlem7  40331  fourierdlem9  40333  fourierdlem10  40334  fourierdlem18  40342  fourierdlem19  40343  fourierdlem20  40344  fourierdlem26  40350  fourierdlem28  40352  fourierdlem30  40354  fourierdlem35  40359  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem47  40370  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem53  40376  fourierdlem57  40380  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem66  40389  fourierdlem68  40391  fourierdlem71  40394  fourierdlem72  40395  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem87  40410  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem94  40417  fourierdlem95  40418  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  qndenserrnbllem  40514  ioorrnopnlem  40524  ioorrnopnxrlem  40526  sge0xaddlem1  40650  sge0xaddlem2  40651  omeiunltfirp  40733  carageniuncllem2  40736  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoiqssbllem1  40836  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem2  40841  hspmbllem3  40842  ovolval5lem1  40866  iinhoiicclem  40887  iinhoiicc  40888  iunhoiioolem  40889  iccvonmbllem  40892  vonioolem1  40894  vonioolem2  40895  vonicclem1  40897  vonicclem2  40898  preimaleiinlt  40931  salpreimaltle  40935  smfaddlem1  40971  smfadd  40973  smflimlem3  40981  smflimlem4  40982  smflimlem6  40984  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  zm1nn  41316  perfectALTVlem2  41631  nnsum4primesevenALTV  41689  bgoldbtbndlem2  41694  dignn0flhalflem1  42409  amgmwlem  42548