Theorem readdcld 10659

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

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
readdcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		readdcl 10609	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7135  ℝcr 10525   + caddc 10529

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  ltadd2  10733  readdcan  10803  addid1  10809  leadd1  11097  le2add  11111  lesub2  11124  lesub3d  11247  supaddc  11595  supadd  11596  cju  11621  nnne0  11659  div4p1lem1div2  11880  difgtsumgt  11938  eluzmn  12238  rpnnen1lem5  12368  addlelt  12491  xralrple  12586  xov1plusxeqvd  12876  zltaddlt1le  12883  elincfzoext  13090  fladdz  13190  2tnp1ge0ge0  13194  flhalf  13195  fldiv  13223  modaddmodup  13297  modaddmodlo  13298  addmodlteq  13309  discr1  13596  discr  13597  ccatalpha  13938  2cshw  14166  remim  14468  remullem  14479  sqrlem7  14600  absrele  14660  abstri  14682  abs3lem  14690  amgm2  14721  bhmafibid1  14817  mulcn2  14944  o1add  14962  o1sub  14964  lo1add  14975  caucvgrlem  15021  iseraltlem2  15031  iseraltlem3  15032  fsumabs  15148  o1fsum  15160  climcndslem2  15197  tanhlt1  15505  eirrlem  15549  ruclem1  15576  ruclem2  15577  ruclem3  15578  ltoddhalfle  15702  bitscmp  15777  sadcaddlem  15796  sadasslem  15809  smuval2  15821  iserodd  16162  prmreclem4  16245  4sqlem5  16268  4sqlem6  16269  4sqlem12  16282  4sqlem15  16285  4sqlem16  16286  prmgaplem7  16383  prmgaplem8  16384  2expltfac  16418  cshwshashlem2  16422  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmul0  21467  chfacfpmmulgsum  21469  prdsxmetlem  22975  xblss2ps  23008  metustexhalf  23163  nrmmetd  23181  ngptgp  23242  nlmvscnlem2  23291  nlmvscnlem1  23292  nmotri  23345  nghmplusg  23346  blcvx  23403  iccntr  23426  icccmplem2  23428  reconnlem2  23432  metdcnlem  23441  metnrmlem3  23466  cnllycmp  23561  lebnumii  23571  tcphcphlem1  23839  ipcnlem2  23848  ipcnlem1  23849  csbren  24003  trirn  24004  minveclem2  24030  minveclem3b  24032  minveclem4  24036  ivthlem2  24056  ovolgelb  24084  ovollb2lem  24092  ovolunlem1a  24100  ovolunlem1  24101  ovolfiniun  24105  ovoliunlem1  24106  ovoliunlem2  24107  ovolshftlem1  24113  ovolscalem1  24117  ovolicopnf  24128  ismbl2  24131  nulmbl2  24140  unmbl  24141  voliunlem2  24155  ioombl1lem2  24163  ioombl1lem4  24165  ioombl1  24166  ioorcl2  24176  uniioombllem1  24185  uniioombllem3  24189  uniioombllem4  24190  uniioombllem5  24191  uniioombl  24193  opnmbllem  24205  volcn  24210  itg1addlem4  24303  mbfi1fseqlem4  24322  mbfi1fseqlem6  24324  itg2splitlem  24352  itg2split  24353  itg2monolem3  24356  itg2addlem  24362  ibladdlem  24423  itgaddlem1  24426  itgaddlem2  24427  iblabslem  24431  iblabs  24432  dvferm1lem  24587  dvferm2lem  24589  dvlip2  24598  lhop1lem  24616  lhop1  24617  lhop  24619  dvcnvrelem1  24620  dvcnvrelem2  24621  dvcnvre  24622  dvcvx  24623  dvfsumlem3  24631  dvfsumlem4  24632  dvfsum2  24637  ftc1lem4  24642  coemullem  24847  ulmbdd  24993  ulmcn  24994  ulmdvlem1  24995  radcnvle  25015  pserdvlem1  25022  pserdv  25024  abelthlem7  25033  pilem2  25047  pilem3  25048  cosordlem  25122  abslogle  25209  logccv  25254  cxpaddle  25341  ang180lem2  25396  heron  25424  atanlogaddlem  25499  atans2  25517  cxp2limlem  25561  scvxcvx  25571  jensenlem2  25573  amgmlem  25575  logdiflbnd  25580  harmonicbnd4  25596  fsumharmonic  25597  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  lgamgulmlem6  25619  lgambdd  25622  lgamucov  25623  regamcl  25646  ftalem5  25662  efnnfsumcl  25688  efchtdvds  25744  chtublem  25795  chtub  25796  logfaclbnd  25806  perfectlem2  25814  bposlem7  25874  bposlem9  25876  lgsdirprm  25915  gausslemma2dlem1a  25949  2sqlem8  26010  chpchtlim  26063  vmadivsumb  26067  rplogsumlem1  26068  dchrisumlem2  26074  dchrvmasumlem2  26082  dchrvmasumiflem1  26085  dchrisum0re  26097  dchrisum0lem1b  26099  mulog2sumlem1  26118  mulog2sumlem2  26119  logsqvma2  26127  log2sumbnd  26128  selberglem2  26130  selbergb  26133  selberg2b  26136  chpdifbndlem1  26137  chpdifbndlem2  26138  selberg3lem2  26142  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrsumbnd2  26151  selberg3r  26153  selberg34r  26155  pntsf  26157  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem2a  26174  pntibndlem2  26175  pntibndlem3  26176  pntlemg  26182  pntlemr  26186  pntlemk  26190  pntlemo  26191  pntlem3  26193  abvcxp  26199  padicabv  26214  ostth2lem2  26218  ostth3  26222  brbtwn2  26699  axsegconlem8  26718  axsegconlem10  26720  axpaschlem  26734  axpasch  26735  axeuclidlem  26756  axcontlem2  26759  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  vacn  28477  smcnlem  28480  ubthlem2  28654  minvecolem2  28658  minvecolem3  28659  minvecolem4  28663  minvecolem5  28664  nmoptrii  29877  hstle  30013  staddi  30029  stadd3i  30031  lt2addrd  30501  nndiffz1  30535  wrdt2ind  30653  cshwrnid  30661  fsumrp0cl  30729  pmtrto1cl  30791  fzto1st  30795  psgnfzto1st  30797  1smat1  31157  sqsscirc1  31261  cnre2csqlem  31263  tpr2rico  31265  nexple  31378  dya2iocress  31642  dya2iocbrsiga  31643  dya2icobrsiga  31644  dya2icoseg  31645  dya2iocucvr  31652  sxbrsigalem2  31654  omssubaddlem  31667  fibp1  31769  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemsgt1  31878  ballotlemsel1i  31880  plymulx0  31927  breprexplemc  32013  breprexp  32014  logdivsqrle  32031  resconn  32606  faclim  33091  dnizphlfeqhlf  33928  dnibndlem4  33933  dnibndlem6  33935  dnibndlem8  33937  dnibndlem9  33938  dnibndlem10  33939  dnibndlem11  33940  dnibndlem13  33942  dnibnd  33943  knoppcnlem4  33948  unblimceq0lem  33958  unblimceq0  33959  unbdqndv2lem1  33961  poimirlem29  35086  heicant  35092  opnmbllem0  35093  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  mbfposadd  35104  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ibladdnclem  35113  itgaddnclem1  35115  itgaddnclem2  35116  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  ftc1cnnclem  35128  ftc1anclem4  35133  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  areacirclem5  35149  mettrifi  35195  isbnd3  35222  ssbnd  35226  cntotbnd  35234  heibor1lem  35247  bfplem2  35261  rrnequiv  35273  iccbnd  35278  lcmineqlem18  39334  lcmineqlem20  39336  2np3bcnp1  39348  2ap1caineq  39349  metakunt29  39378  2xp3dxp2ge1d  39387  factwoffsmonot  39388  readdid1addid2d  39465  resubeulem1  39513  resubeulem2  39514  resubeu  39515  readdsub  39522  reladdrsub  39523  resubidaddid1lem  39532  renegid2  39551  sn-it0e0  39552  sn-0tie0  39576  cnreeu  39593  dffltz  39615  fltnltalem  39618  fltnlta  39619  3cubeslem1  39625  pellexlem2  39771  pell1qrge1  39811  pell14qrgapw  39817  pellqrexplicit  39818  pellqrex  39820  pellfundge  39823  pellfundgt1  39824  rmspecfund  39850  rmxycomplete  39858  ltrmynn0  39889  jm2.24nn  39900  jm2.24  39904  fzmaxdif  39922  jm2.26lem3  39942  jm3.1lem2  39959  areaquad  40166  sqrtcvallem4  40339  sqrtcvallem5  40340  sqrtcval  40341  imo72b2lem0  40869  hashnzfzclim  41026  binomcxplemnotnn0  41060  zltlesub  41916  lt3addmuld  41933  absnpncan2d  41934  fperiodmullem  41935  lt4addmuld  41938  absnpncan3d  41939  leadd12dd  41948  supxrgelem  41969  supxrge  41970  ltadd12dd  41975  xralrple2  41986  infxr  41999  infleinflem2  42003  xralrple4  42005  xralrple3  42006  xrralrecnnle  42017  eliooshift  42143  iccshift  42155  iooshift  42159  iooiinicc  42179  iooiinioc  42193  fsumnncl  42213  climinf  42248  climsuselem1  42249  sumnnodd  42272  lptre2pt  42282  addlimc  42290  0ellimcdiv  42291  limclner  42293  climleltrp  42318  liminfltlem  42446  fperdvper  42561  dvdivbd  42565  dvbdfbdioolem2  42571  dvbdfbdioo  42572  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvxpaek  42582  dvnmul  42585  iblsplit  42608  iblspltprt  42615  itgspltprt  42621  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stoweidlem1  42643  stoweidlem11  42653  stoweidlem13  42655  stoweidlem14  42656  stoweidlem20  42662  stoweidlem21  42663  stoweidlem26  42668  stoweidlem44  42686  stoweidlem60  42702  wallispilem3  42709  wallispilem4  42710  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem1  42716  stirlinglem3  42718  stirlinglem5  42720  stirlinglem6  42721  stirlinglem7  42722  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  dirker2re  42734  dirkerval2  42736  dirkerre  42737  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkeritg  42744  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem4  42753  fourierdlem5  42754  fourierdlem6  42755  fourierdlem7  42756  fourierdlem9  42758  fourierdlem10  42759  fourierdlem18  42767  fourierdlem19  42768  fourierdlem20  42769  fourierdlem26  42775  fourierdlem28  42777  fourierdlem30  42779  fourierdlem35  42784  fourierdlem40  42789  fourierdlem41  42790  fourierdlem42  42791  fourierdlem47  42795  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem53  42801  fourierdlem57  42805  fourierdlem59  42807  fourierdlem60  42808  fourierdlem61  42809  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem66  42814  fourierdlem68  42816  fourierdlem71  42819  fourierdlem72  42820  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem79  42827  fourierdlem80  42828  fourierdlem81  42829  fourierdlem82  42830  fourierdlem83  42831  fourierdlem84  42832  fourierdlem87  42835  fourierdlem88  42836  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem92  42840  fourierdlem93  42841  fourierdlem94  42842  fourierdlem95  42843  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  qndenserrnbllem  42936  ioorrnopnlem  42946  ioorrnopnxrlem  42948  sge0xaddlem1  43072  sge0xaddlem2  43073  omeiunltfirp  43158  carageniuncllem2  43161  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoiqssbllem1  43261  hoiqssbllem2  43262  hoiqssbllem3  43263  hspmbllem2  43266  hspmbllem3  43267  ovolval5lem1  43291  iinhoiicclem  43312  iinhoiicc  43313  iunhoiioolem  43314  iccvonmbllem  43317  vonioolem1  43319  vonioolem2  43320  vonicclem1  43322  vonicclem2  43323  preimaleiinlt  43356  salpreimaltle  43360  smfaddlem1  43396  smfadd  43398  smflimlem3  43406  smflimlem4  43407  smflimlem6  43409  smfmullem1  43423  smfmullem2  43424  smfmullem3  43425  zm1nn  43859  requad01  44139  requad1  44140  requad2  44141  perfectALTVlem2  44240  nnsum4primesevenALTV  44319  bgoldbtbndlem2  44324  dignn0flhalflem1  45029  affinecomb1  45116  resum2sqcl  45120  2sphere  45163  line2  45166  itsclc0lem1  45170  itscnhlc0yqe  45173  itsclquadb  45190  2itscp  45195  itscnhlinecirc02plem1  45196  itscnhlinecirc02plem3  45198  itscnhlinecirc02p  45199  inlinecirc02plem  45200  amgmwlem  45330