Theorem readdcld 11341

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 11286	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  ℝcr 11202   + caddc 11206

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11264

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ltadd2  11417  readdcan  11487  addrid  11493  leadd1  11787  le2add  11801  lesub2  11814  lesub3d  11937  le2addd  11938  supaddc  12287  supadd  12288  cju  12319  nnne0  12375  div4p1lem1div2  12604  difgtsumgt  12662  eluzmn  12975  rpnnen1lem5  13112  addlelt  13239  xralrple  13338  xov1plusxeqvd  13632  zltaddlt1le  13639  elincfzoext  13861  fladdz  13968  2tnp1ge0ge0  13972  flhalf  13973  fldiv  14003  modaddb  14052  modaddmodup  14080  modaddmodlo  14081  addmodlteq  14092  discr1  14386  discr  14387  ccatalpha  14743  2cshw  14968  remim  15289  remullem  15300  01sqrexlem7  15420  absrele  15480  abstri  15503  abs3lem  15511  amgm2  15542  bhmafibid1  15640  mulcn2  15768  o1add  15786  o1sub  15788  lo1add  15799  caucvgrlem  15845  iseraltlem2  15855  iseraltlem3  15856  fsumabs  15973  o1fsum  15985  climcndslem2  16024  tanhlt1  16333  eirrlem  16377  ruclem1  16404  ruclem2  16405  ruclem3  16406  ltoddhalfle  16536  bitscmp  16613  sadcaddlem  16632  sadasslem  16645  smuval2  16657  iserodd  17018  prmreclem4  17102  4sqlem5  17125  4sqlem6  17126  4sqlem12  17139  4sqlem15  17142  4sqlem16  17143  prmgaplem7  17240  prmgaplem8  17241  2expltfac  17275  cshwshashlem2  17279  chfacfscmul0  23181  chfacfscmulgsum  23183  chfacfpmmul0  23185  chfacfpmmulgsum  23187  prdsxmetlem  24692  xblss2ps  24725  metustexhalf  24880  nrmmetd  24898  ngptgp  24960  nlmvscnlem2  25009  nlmvscnlem1  25010  nmotri  25063  nghmplusg  25064  blcvx  25122  iccntr  25146  icccmplem2  25148  reconnlem2  25152  metdcnlem  25161  metnrmlem3  25186  cnllycmp  25282  lebnumii  25292  tcphcphlem1  25561  ipcnlem2  25570  ipcnlem1  25571  csbren  25725  trirn  25726  minveclem2  25752  minveclem3b  25754  minveclem4  25758  ivthlem2  25778  ovolgelb  25806  ovollb2lem  25814  ovolunlem1a  25822  ovolunlem1  25823  ovolfiniun  25827  ovoliunlem1  25828  ovoliunlem2  25829  ovolshftlem1  25835  ovolscalem1  25839  ovolicopnf  25850  ismbl2  25853  nulmbl2  25862  unmbl  25863  voliunlem2  25877  ioombl1lem2  25885  ioombl1lem4  25887  ioombl1  25888  ioorcl2  25898  uniioombllem1  25907  uniioombllem3  25911  uniioombllem4  25912  uniioombllem5  25913  uniioombl  25915  opnmbllem  25927  volcn  25932  itg1addlem4  26025  mbfi1fseqlem4  26044  mbfi1fseqlem6  26046  itg2splitlem  26074  itg2split  26075  itg2monolem3  26078  itg2addlem  26084  ibladdlem  26145  itgaddlem1  26148  itgaddlem2  26149  iblabslem  26153  iblabs  26154  dvferm1lem  26309  dvferm2lem  26311  dvlip2  26320  lhop1lem  26338  lhop1  26339  lhop  26341  dvcnvrelem1  26342  dvcnvrelem2  26343  dvcnvre  26344  dvcvx  26345  dvfsumlem3  26353  dvfsumlem4  26354  dvfsum2  26359  ftc1lem4  26364  coemullem  26574  plyn0mulidp  26607  ulmbdd  26730  ulmcn  26731  ulmdvlem1  26732  radcnvle  26752  pserdvlem1  26759  pserdv  26761  abelthlem7  26770  pilem2  26784  pilem3  26785  cosordlem  26863  abslogle  26951  logccv  26996  cxpaddle  27085  ang180lem2  27143  heron  27171  atanlogaddlem  27246  atans2  27264  cxp2limlem  27308  scvxcvx  27318  jensenlem2  27320  amgmlem  27322  logdiflbnd  27327  harmonicbnd4  27343  fsumharmonic  27344  lgamgulmlem3  27363  lgamgulmlem4  27364  lgamgulmlem5  27365  lgamgulmlem6  27366  lgambdd  27369  lgamucov  27370  regamcl  27393  ftalem5  27409  efnnfsumcl  27435  efchtdvds  27491  chtublem  27543  chtub  27544  logfaclbnd  27554  perfectlem2  27562  bposlem7  27622  bposlem9  27624  lgsdirprm  27663  gausslemma2dlem1a  27697  2sqlem8  27758  chpchtlim  27811  vmadivsumb  27815  rplogsumlem1  27816  dchrisumlem2  27822  dchrvmasumlem2  27830  dchrvmasumiflem1  27833  dchrisum0re  27845  dchrisum0lem1b  27847  mulog2sumlem1  27866  mulog2sumlem2  27867  logsqvma2  27875  log2sumbnd  27876  selberglem2  27878  selbergb  27881  selberg2b  27884  chpdifbndlem1  27885  chpdifbndlem2  27886  selberg3lem2  27890  selberg3  27891  selberg4lem1  27892  selberg4  27893  pntrsumbnd2  27899  selberg3r  27901  selberg34r  27903  pntsf  27905  pntrlog2bndlem1  27909  pntrlog2bndlem2  27910  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntrlog2bndlem6  27915  pntrlog2bnd  27916  pntpbnd1a  27917  pntpbnd2  27919  pntibndlem2a  27922  pntibndlem2  27923  pntibndlem3  27924  pntlemg  27930  pntlemr  27934  pntlemk  27938  pntlemo  27939  pntlem3  27941  abvcxp  27947  padicabv  27962  ostth2lem2  27966  ostth3  27970  brbtwn2  29488  axsegconlem8  29507  axsegconlem10  29509  axpaschlem  29523  axpasch  29524  axeuclidlem  29545  axcontlem2  29548  crctcshwlkn0lem3  30406  crctcshwlkn0lem5  30408  vacn  31301  smcnlem  31304  ubthlem2  31478  minvecolem2  31482  minvecolem3  31483  minvecolem4  31487  minvecolem5  31488  nmoptrii  32701  hstle  32837  staddi  32853  stadd3i  32855  lt2addrd  33388  nndiffz1  33424  nexple  33470  wrdt2ind  33562  cshwrnid  33568  fsumrp0cl  33628  pmtrto1cl  33706  fzto1st  33710  psgnfzto1st  33712  constrresqrtcl  34455  cos9thpiminplylem1  34460  1smat1  34482  sqsscirc1  34586  cnre2csqlem  34588  tpr2rico  34590  dya2iocress  34952  dya2iocbrsiga  34953  dya2icobrsiga  34954  dya2icoseg  34955  dya2iocucvr  34962  sxbrsigalem2  34964  omssubaddlem  34977  fibp1  35079  ballotlemfc0  35171  ballotlemfcc  35172  ballotlemsgt1  35189  ballotlemsel1i  35191  breprexplemc  35307  breprexp  35308  logdivsqrle  35325  resconn  36097  faclim  36603  dnizphlfeqhlf  37434  dnibndlem4  37439  dnibndlem6  37441  dnibndlem8  37443  dnibndlem9  37444  dnibndlem10  37445  dnibndlem11  37446  dnibndlem13  37448  dnibnd  37449  knoppcnlem4  37454  unblimceq0lem  37464  unblimceq0  37465  unbdqndv2lem1  37467  poimirlem29  38660  heicant  38666  opnmbllem0  38667  mblfinlem3  38670  mblfinlem4  38671  ismblfin  38672  mbfposadd  38678  itg2addnclem  38682  itg2addnclem3  38684  itg2addnc  38685  itg2gt0cn  38686  ibladdnclem  38687  itgaddnclem1  38689  itgaddnclem2  38690  iblabsnclem  38694  iblabsnc  38695  iblmulc2nc  38696  ftc1cnnclem  38702  ftc1anclem4  38707  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  areacirclem5  38723  mettrifi  38784  isbnd3  38811  ssbnd  38815  cntotbnd  38823  heibor1lem  38836  bfplem2  38850  rrnequiv  38862  iccbnd  38867  lcmineqlem18  43189  lcmineqlem20  43191  aks4d1p1p3  43212  aks4d1p1p2  43213  aks4d1p1p4  43214  aks4d1p1p6  43216  aks4d1p1p7  43217  aks4d1p1p5  43218  aks4d1p1  43219  posbezout  43243  aks6d1c1  43259  aks6d1c2  43273  2np3bcnp1  43287  2ap1caineq  43288  sticksstones6  43294  sticksstones7  43295  sticksstones10  43298  sticksstones12a  43300  sticksstones12  43301  sticksstones22  43311  bcle2d  43322  aks6d1c7lem1  43323  readdridaddlidd  43401  resubeulem1  43519  resubeulem2  43520  resubeu  43521  readdsub  43528  reladdrsub  43529  resubidaddlidlem  43538  renegid2  43558  sn-it0e0  43560  redivdird  43606  sn-0tie0  43608  sn-addlt0d  43615  sn-addgt0d  43616  cnreeu  43647  dffltz  43763  fltnltalem  43766  fltnlta  43767  3cubeslem1  43787  pellexlem2  43930  pell1qrge1  43970  pell14qrgapw  43976  pellqrexplicit  43977  pellqrex  43979  pellfundge  43982  pellfundgt1  43983  rmspecfund  44009  rmxycomplete  44017  ltrmynn0  44048  jm2.24nn  44059  jm2.24  44063  fzmaxdif  44081  jm2.26lem3  44101  jm3.1lem2  44118  areaquad  44311  sqrtcvallem4  44732  sqrtcvallem5  44733  sqrtcval  44734  imo72b2lem0  45258  hashnzfzclim  45399  binomcxplemnotnn0  45433  zltlesub  46394  lt3addmuld  46410  absnpncan2d  46411  fperiodmullem  46412  lt4addmuld  46415  absnpncan3d  46416  supxrgelem  46442  supxrge  46443  ltadd12dd  46448  xralrple2  46459  infxr  46471  infleinflem2  46475  xralrple4  46477  xralrple3  46478  xrralrecnnle  46487  eliooshift  46611  iccshift  46623  iooshift  46627  iooiinicc  46647  iooiinioc  46661  fsumnncl  46677  climinf  46711  climsuselem1  46712  sumnnodd  46735  lptre2pt  46743  addlimc  46751  0ellimcdiv  46752  limclner  46754  climleltrp  46779  liminfltlem  46907  fperdvper  47022  dvdivbd  47026  dvbdfbdioolem2  47032  dvbdfbdioo  47033  ioodvbdlimc1lem1  47034  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvxpaek  47043  dvnmul  47046  iblsplit  47069  iblspltprt  47076  itgspltprt  47082  itgiccshift  47083  itgperiod  47084  itgsbtaddcnst  47085  stoweidlem1  47104  stoweidlem11  47114  stoweidlem13  47116  stoweidlem14  47117  stoweidlem20  47123  stoweidlem21  47124  stoweidlem26  47129  stoweidlem44  47147  stoweidlem60  47163  wallispilem3  47170  wallispilem4  47171  wallispilem5  47172  wallispi  47173  wallispi2lem1  47174  wallispi2lem2  47175  stirlinglem1  47177  stirlinglem3  47179  stirlinglem5  47181  stirlinglem6  47182  stirlinglem7  47183  stirlinglem10  47186  stirlinglem11  47187  stirlinglem12  47188  dirker2re  47195  dirkerval2  47197  dirkerre  47198  dirkerper  47199  dirkertrigeqlem1  47201  dirkertrigeqlem2  47202  dirkeritg  47205  dirkercncflem1  47206  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem4  47214  fourierdlem5  47215  fourierdlem6  47216  fourierdlem7  47217  fourierdlem9  47219  fourierdlem10  47220  fourierdlem18  47228  fourierdlem19  47229  fourierdlem20  47230  fourierdlem26  47236  fourierdlem28  47238  fourierdlem30  47240  fourierdlem35  47245  fourierdlem40  47250  fourierdlem41  47251  fourierdlem42  47252  fourierdlem47  47256  fourierdlem48  47257  fourierdlem49  47258  fourierdlem50  47259  fourierdlem51  47260  fourierdlem53  47262  fourierdlem57  47266  fourierdlem59  47268  fourierdlem60  47269  fourierdlem61  47270  fourierdlem63  47272  fourierdlem64  47273  fourierdlem65  47274  fourierdlem66  47275  fourierdlem68  47277  fourierdlem71  47280  fourierdlem72  47281  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem78  47287  fourierdlem79  47288  fourierdlem80  47289  fourierdlem81  47290  fourierdlem82  47291  fourierdlem83  47292  fourierdlem84  47293  fourierdlem87  47296  fourierdlem88  47297  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem92  47301  fourierdlem93  47302  fourierdlem94  47303  fourierdlem95  47304  fourierdlem97  47306  fourierdlem101  47310  fourierdlem103  47312  fourierdlem104  47313  fourierdlem111  47320  fourierdlem112  47321  fourierdlem113  47322  sqwvfoura  47331  sqwvfourb  47332  fouriersw  47334  qndenserrnbllem  47397  ioorrnopnlem  47407  ioorrnopnxrlem  47409  sge0xaddlem1  47536  sge0xaddlem2  47537  omeiunltfirp  47622  carageniuncllem2  47625  hoidmv1lelem1  47694  hoidmv1lelem2  47695  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  hoidmvlelem4  47701  hoiqssbllem1  47725  hoiqssbllem2  47726  hoiqssbllem3  47727  hspmbllem2  47730  hspmbllem3  47731  ovolval5lem1  47755  iinhoiicclem  47776  iinhoiicc  47777  iunhoiioolem  47778  iccvonmbllem  47781  vonioolem1  47783  vonioolem2  47784  vonicclem1  47786  vonicclem2  47787  preimaleiinlt  47824  salpreimaltle  47829  smfaddlem1  47866  smfadd  47868  smflimlem3  47876  smflimlem4  47877  smflimlem6  47879  smfmullem1  47894  smfmullem2  47895  smfmullem3  47896  ormkglobd  47980  zm1nn  48465  requad01  48812  requad1  48813  requad2  48814  perfectALTVlem2  48913  nnsum4primesevenALTV  48992  bgoldbtbndlem2  48997  gpgvtxedg0  49254  gpgvtxedg1  49255  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx13starlem2  49263  dignn0flhalflem1  49820  affinecomb1  49907  resum2sqcl  49911  2sphere  49954  line2  49957  itsclc0lem1  49961  itscnhlc0yqe  49964  itsclquadb  49981  2itscp  49986  itscnhlinecirc02plem1  49987  itscnhlinecirc02plem3  49989  itscnhlinecirc02p  49990  inlinecirc02plem  49991  crossp3d  51135  veronesefvcl  51140  veronesev1lem  51141  veronesev2lem  51142  veronesev3lem  51143  veronesev4lem  51144  veronesev5lem  51145  veronesev6lem  51146  amgmwlem  51155