Theorem readdcld 11240

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7401  ℝcr 11105   + caddc 11109

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

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  ltadd2  11315  readdcan  11385  addrid  11391  leadd1  11679  le2add  11693  lesub2  11706  lesub3d  11829  supaddc  12178  supadd  12179  cju  12205  nnne0  12243  div4p1lem1div2  12464  difgtsumgt  12522  eluzmn  12826  rpnnen1lem5  12962  addlelt  13085  xralrple  13181  xov1plusxeqvd  13472  zltaddlt1le  13479  elincfzoext  13687  fladdz  13787  2tnp1ge0ge0  13791  flhalf  13792  fldiv  13822  modaddmodup  13896  modaddmodlo  13897  addmodlteq  13908  discr1  14199  discr  14200  ccatalpha  14540  2cshw  14760  remim  15061  remullem  15072  01sqrexlem7  15192  absrele  15252  abstri  15274  abs3lem  15282  amgm2  15313  bhmafibid1  15409  mulcn2  15537  o1add  15555  o1sub  15557  lo1add  15568  caucvgrlem  15616  iseraltlem2  15626  iseraltlem3  15627  fsumabs  15744  o1fsum  15756  climcndslem2  15793  tanhlt1  16100  eirrlem  16144  ruclem1  16171  ruclem2  16172  ruclem3  16173  ltoddhalfle  16301  bitscmp  16376  sadcaddlem  16395  sadasslem  16408  smuval2  16420  iserodd  16767  prmreclem4  16851  4sqlem5  16874  4sqlem6  16875  4sqlem12  16888  4sqlem15  16891  4sqlem16  16892  prmgaplem7  16989  prmgaplem8  16990  2expltfac  17025  cshwshashlem2  17029  chfacfscmul0  22682  chfacfscmulgsum  22684  chfacfpmmul0  22686  chfacfpmmulgsum  22688  prdsxmetlem  24196  xblss2ps  24229  metustexhalf  24387  nrmmetd  24405  ngptgp  24467  nlmvscnlem2  24524  nlmvscnlem1  24525  nmotri  24578  nghmplusg  24579  blcvx  24636  iccntr  24659  icccmplem2  24661  reconnlem2  24665  metdcnlem  24674  metnrmlem3  24699  cnllycmp  24804  lebnumii  24814  tcphcphlem1  25085  ipcnlem2  25094  ipcnlem1  25095  csbren  25249  trirn  25250  minveclem2  25276  minveclem3b  25278  minveclem4  25282  ivthlem2  25303  ovolgelb  25331  ovollb2lem  25339  ovolunlem1a  25347  ovolunlem1  25348  ovolfiniun  25352  ovoliunlem1  25353  ovoliunlem2  25354  ovolshftlem1  25360  ovolscalem1  25364  ovolicopnf  25375  ismbl2  25378  nulmbl2  25387  unmbl  25388  voliunlem2  25402  ioombl1lem2  25410  ioombl1lem4  25412  ioombl1  25413  ioorcl2  25423  uniioombllem1  25432  uniioombllem3  25436  uniioombllem4  25437  uniioombllem5  25438  uniioombl  25440  opnmbllem  25452  volcn  25457  itg1addlem4  25550  itg1addlem4OLD  25551  mbfi1fseqlem4  25570  mbfi1fseqlem6  25572  itg2splitlem  25600  itg2split  25601  itg2monolem3  25604  itg2addlem  25610  ibladdlem  25671  itgaddlem1  25674  itgaddlem2  25675  iblabslem  25679  iblabs  25680  dvferm1lem  25838  dvferm2lem  25840  dvlip2  25850  lhop1lem  25868  lhop1  25869  lhop  25871  dvcnvrelem1  25872  dvcnvrelem2  25873  dvcnvre  25874  dvcvx  25875  dvfsumlem3  25885  dvfsumlem4  25886  dvfsum2  25891  ftc1lem4  25896  coemullem  26104  ulmbdd  26251  ulmcn  26252  ulmdvlem1  26253  radcnvle  26273  pserdvlem1  26281  pserdv  26283  abelthlem7  26292  pilem2  26306  pilem3  26307  cosordlem  26381  abslogle  26468  logccv  26513  cxpaddle  26603  ang180lem2  26658  heron  26686  atanlogaddlem  26761  atans2  26779  cxp2limlem  26824  scvxcvx  26834  jensenlem2  26836  amgmlem  26838  logdiflbnd  26843  harmonicbnd4  26859  fsumharmonic  26860  lgamgulmlem3  26879  lgamgulmlem4  26880  lgamgulmlem5  26881  lgamgulmlem6  26882  lgambdd  26885  lgamucov  26886  regamcl  26909  ftalem5  26925  efnnfsumcl  26951  efchtdvds  27007  chtublem  27060  chtub  27061  logfaclbnd  27071  perfectlem2  27079  bposlem7  27139  bposlem9  27141  lgsdirprm  27180  gausslemma2dlem1a  27214  2sqlem8  27275  chpchtlim  27328  vmadivsumb  27332  rplogsumlem1  27333  dchrisumlem2  27339  dchrvmasumlem2  27347  dchrvmasumiflem1  27350  dchrisum0re  27362  dchrisum0lem1b  27364  mulog2sumlem1  27383  mulog2sumlem2  27384  logsqvma2  27392  log2sumbnd  27393  selberglem2  27395  selbergb  27398  selberg2b  27401  chpdifbndlem1  27402  chpdifbndlem2  27403  selberg3lem2  27407  selberg3  27408  selberg4lem1  27409  selberg4  27410  pntrsumbnd2  27416  selberg3r  27418  selberg34r  27420  pntsf  27422  pntrlog2bndlem1  27426  pntrlog2bndlem2  27427  pntrlog2bndlem4  27429  pntrlog2bndlem5  27430  pntrlog2bndlem6  27432  pntrlog2bnd  27433  pntpbnd1a  27434  pntpbnd2  27436  pntibndlem2a  27439  pntibndlem2  27440  pntibndlem3  27441  pntlemg  27447  pntlemr  27451  pntlemk  27455  pntlemo  27456  pntlem3  27458  abvcxp  27464  padicabv  27479  ostth2lem2  27483  ostth3  27487  brbtwn2  28632  axsegconlem8  28651  axsegconlem10  28653  axpaschlem  28667  axpasch  28668  axeuclidlem  28689  axcontlem2  28692  crctcshwlkn0lem3  29535  crctcshwlkn0lem5  29537  vacn  30416  smcnlem  30419  ubthlem2  30593  minvecolem2  30597  minvecolem3  30598  minvecolem4  30602  minvecolem5  30603  nmoptrii  31816  hstle  31952  staddi  31968  stadd3i  31970  lt2addrd  32433  nndiffz1  32466  wrdt2ind  32584  cshwrnid  32592  fsumrp0cl  32661  pmtrto1cl  32726  fzto1st  32730  psgnfzto1st  32732  1smat1  33273  sqsscirc1  33377  cnre2csqlem  33379  tpr2rico  33381  nexple  33496  dya2iocress  33762  dya2iocbrsiga  33763  dya2icobrsiga  33764  dya2icoseg  33765  dya2iocucvr  33772  sxbrsigalem2  33774  omssubaddlem  33787  fibp1  33889  ballotlemfc0  33980  ballotlemfcc  33981  ballotlemsgt1  33998  ballotlemsel1i  34000  plymulx0  34047  breprexplemc  34133  breprexp  34134  logdivsqrle  34151  resconn  34726  faclim  35211  dnizphlfeqhlf  35842  dnibndlem4  35847  dnibndlem6  35849  dnibndlem8  35851  dnibndlem9  35852  dnibndlem10  35853  dnibndlem11  35854  dnibndlem13  35856  dnibnd  35857  knoppcnlem4  35862  unblimceq0lem  35872  unblimceq0  35873  unbdqndv2lem1  35875  poimirlem29  37007  heicant  37013  opnmbllem0  37014  mblfinlem3  37017  mblfinlem4  37018  ismblfin  37019  mbfposadd  37025  itg2addnclem  37029  itg2addnclem3  37031  itg2addnc  37032  itg2gt0cn  37033  ibladdnclem  37034  itgaddnclem1  37036  itgaddnclem2  37037  iblabsnclem  37041  iblabsnc  37042  iblmulc2nc  37043  ftc1cnnclem  37049  ftc1anclem4  37054  ftc1anclem7  37057  ftc1anclem8  37058  ftc1anc  37059  areacirclem5  37070  mettrifi  37115  isbnd3  37142  ssbnd  37146  cntotbnd  37154  heibor1lem  37167  bfplem2  37181  rrnequiv  37193  iccbnd  37198  lcmineqlem18  41404  lcmineqlem20  41406  aks4d1p1p3  41427  aks4d1p1p2  41428  aks4d1p1p4  41429  aks4d1p1p6  41431  aks4d1p1p7  41432  aks4d1p1p5  41433  aks4d1p1  41434  2np3bcnp1  41453  2ap1caineq  41454  sticksstones6  41460  sticksstones7  41461  sticksstones10  41464  sticksstones12a  41466  sticksstones12  41467  sticksstones22  41477  metakunt29  41506  2xp3dxp2ge1d  41515  factwoffsmonot  41516  readdridaddlidd  41667  resubeulem1  41737  resubeulem2  41738  resubeu  41739  readdsub  41746  reladdrsub  41747  resubidaddlidlem  41756  renegid2  41775  sn-it0e0  41777  sn-0tie0  41801  sn-addlt0d  41808  sn-addgt0d  41809  cnreeu  41830  dffltz  41865  fltnltalem  41893  fltnlta  41894  3cubeslem1  41911  pellexlem2  42057  pell1qrge1  42097  pell14qrgapw  42103  pellqrexplicit  42104  pellqrex  42106  pellfundge  42109  pellfundgt1  42110  rmspecfund  42136  rmxycomplete  42145  ltrmynn0  42176  jm2.24nn  42187  jm2.24  42191  fzmaxdif  42209  jm2.26lem3  42229  jm3.1lem2  42246  areaquad  42454  sqrtcvallem4  42879  sqrtcvallem5  42880  sqrtcval  42881  imo72b2lem0  43406  hashnzfzclim  43570  binomcxplemnotnn0  43604  zltlesub  44480  lt3addmuld  44496  absnpncan2d  44497  fperiodmullem  44498  lt4addmuld  44501  absnpncan3d  44502  leadd12dd  44511  supxrgelem  44532  supxrge  44533  ltadd12dd  44538  xralrple2  44549  infxr  44562  infleinflem2  44566  xralrple4  44568  xralrple3  44569  xrralrecnnle  44578  eliooshift  44704  iccshift  44716  iooshift  44720  iooiinicc  44740  iooiinioc  44754  fsumnncl  44773  climinf  44807  climsuselem1  44808  sumnnodd  44831  lptre2pt  44841  addlimc  44849  0ellimcdiv  44850  limclner  44852  climleltrp  44877  liminfltlem  45005  fperdvper  45120  dvdivbd  45124  dvbdfbdioolem2  45130  dvbdfbdioo  45131  ioodvbdlimc1lem1  45132  ioodvbdlimc1lem2  45133  ioodvbdlimc2lem  45135  dvxpaek  45141  dvnmul  45144  iblsplit  45167  iblspltprt  45174  itgspltprt  45180  itgiccshift  45181  itgperiod  45182  itgsbtaddcnst  45183  stoweidlem1  45202  stoweidlem11  45212  stoweidlem13  45214  stoweidlem14  45215  stoweidlem20  45221  stoweidlem21  45222  stoweidlem26  45227  stoweidlem44  45245  stoweidlem60  45261  wallispilem3  45268  wallispilem4  45269  wallispilem5  45270  wallispi  45271  wallispi2lem1  45272  wallispi2lem2  45273  stirlinglem1  45275  stirlinglem3  45277  stirlinglem5  45279  stirlinglem6  45280  stirlinglem7  45281  stirlinglem10  45284  stirlinglem11  45285  stirlinglem12  45286  dirker2re  45293  dirkerval2  45295  dirkerre  45296  dirkerper  45297  dirkertrigeqlem1  45299  dirkertrigeqlem2  45300  dirkeritg  45303  dirkercncflem1  45304  dirkercncflem2  45305  dirkercncflem4  45307  fourierdlem4  45312  fourierdlem5  45313  fourierdlem6  45314  fourierdlem7  45315  fourierdlem9  45317  fourierdlem10  45318  fourierdlem18  45326  fourierdlem19  45327  fourierdlem20  45328  fourierdlem26  45334  fourierdlem28  45336  fourierdlem30  45338  fourierdlem35  45343  fourierdlem40  45348  fourierdlem41  45349  fourierdlem42  45350  fourierdlem47  45354  fourierdlem48  45355  fourierdlem49  45356  fourierdlem50  45357  fourierdlem51  45358  fourierdlem53  45360  fourierdlem57  45364  fourierdlem59  45366  fourierdlem60  45367  fourierdlem61  45368  fourierdlem63  45370  fourierdlem64  45371  fourierdlem65  45372  fourierdlem66  45373  fourierdlem68  45375  fourierdlem71  45378  fourierdlem72  45379  fourierdlem74  45381  fourierdlem75  45382  fourierdlem76  45383  fourierdlem78  45385  fourierdlem79  45386  fourierdlem80  45387  fourierdlem81  45388  fourierdlem82  45389  fourierdlem83  45390  fourierdlem84  45391  fourierdlem87  45394  fourierdlem88  45395  fourierdlem89  45396  fourierdlem90  45397  fourierdlem91  45398  fourierdlem92  45399  fourierdlem93  45400  fourierdlem94  45401  fourierdlem95  45402  fourierdlem97  45404  fourierdlem101  45408  fourierdlem103  45410  fourierdlem104  45411  fourierdlem111  45418  fourierdlem112  45419  fourierdlem113  45420  sqwvfoura  45429  sqwvfourb  45430  fouriersw  45432  qndenserrnbllem  45495  ioorrnopnlem  45505  ioorrnopnxrlem  45507  sge0xaddlem1  45634  sge0xaddlem2  45635  omeiunltfirp  45720  carageniuncllem2  45723  hoidmv1lelem1  45792  hoidmv1lelem2  45793  hoidmvlelem1  45796  hoidmvlelem2  45797  hoidmvlelem3  45798  hoidmvlelem4  45799  hoiqssbllem1  45823  hoiqssbllem2  45824  hoiqssbllem3  45825  hspmbllem2  45828  hspmbllem3  45829  ovolval5lem1  45853  iinhoiicclem  45874  iinhoiicc  45875  iunhoiioolem  45876  iccvonmbllem  45879  vonioolem1  45881  vonioolem2  45882  vonicclem1  45884  vonicclem2  45885  preimaleiinlt  45922  salpreimaltle  45927  smfaddlem1  45964  smfadd  45966  smflimlem3  45974  smflimlem4  45975  smflimlem6  45977  smfmullem1  45992  smfmullem2  45993  smfmullem3  45994  zm1nn  46495  requad01  46774  requad1  46775  requad2  46776  perfectALTVlem2  46875  nnsum4primesevenALTV  46954  bgoldbtbndlem2  46959  dignn0flhalflem1  47489  affinecomb1  47576  resum2sqcl  47580  2sphere  47623  line2  47626  itsclc0lem1  47630  itscnhlc0yqe  47633  itsclquadb  47650  2itscp  47655  itscnhlinecirc02plem1  47656  itscnhlinecirc02plem3  47658  itscnhlinecirc02p  47659  inlinecirc02plem  47660  amgmwlem  48037