Theorem readdcld 11247

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

Syntax hints:   → wi 4   ∈ wcel 2104  (class class class)co 7411  ℝcr 11111   + caddc 11115

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

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

This theorem is referenced by:  ltadd2  11322  readdcan  11392  addrid  11398  leadd1  11686  le2add  11700  lesub2  11713  lesub3d  11836  supaddc  12185  supadd  12186  cju  12212  nnne0  12250  div4p1lem1div2  12471  difgtsumgt  12529  eluzmn  12833  rpnnen1lem5  12969  addlelt  13092  xralrple  13188  xov1plusxeqvd  13479  zltaddlt1le  13486  elincfzoext  13694  fladdz  13794  2tnp1ge0ge0  13798  flhalf  13799  fldiv  13829  modaddmodup  13903  modaddmodlo  13904  addmodlteq  13915  discr1  14206  discr  14207  ccatalpha  14547  2cshw  14767  remim  15068  remullem  15079  01sqrexlem7  15199  absrele  15259  abstri  15281  abs3lem  15289  amgm2  15320  bhmafibid1  15416  mulcn2  15544  o1add  15562  o1sub  15564  lo1add  15575  caucvgrlem  15623  iseraltlem2  15633  iseraltlem3  15634  fsumabs  15751  o1fsum  15763  climcndslem2  15800  tanhlt1  16107  eirrlem  16151  ruclem1  16178  ruclem2  16179  ruclem3  16180  ltoddhalfle  16308  bitscmp  16383  sadcaddlem  16402  sadasslem  16415  smuval2  16427  iserodd  16772  prmreclem4  16856  4sqlem5  16879  4sqlem6  16880  4sqlem12  16893  4sqlem15  16896  4sqlem16  16897  prmgaplem7  16994  prmgaplem8  16995  2expltfac  17030  cshwshashlem2  17034  chfacfscmul0  22580  chfacfscmulgsum  22582  chfacfpmmul0  22584  chfacfpmmulgsum  22586  prdsxmetlem  24094  xblss2ps  24127  metustexhalf  24285  nrmmetd  24303  ngptgp  24365  nlmvscnlem2  24422  nlmvscnlem1  24423  nmotri  24476  nghmplusg  24477  blcvx  24534  iccntr  24557  icccmplem2  24559  reconnlem2  24563  metdcnlem  24572  metnrmlem3  24597  cnllycmp  24702  lebnumii  24712  tcphcphlem1  24983  ipcnlem2  24992  ipcnlem1  24993  csbren  25147  trirn  25148  minveclem2  25174  minveclem3b  25176  minveclem4  25180  ivthlem2  25201  ovolgelb  25229  ovollb2lem  25237  ovolunlem1a  25245  ovolunlem1  25246  ovolfiniun  25250  ovoliunlem1  25251  ovoliunlem2  25252  ovolshftlem1  25258  ovolscalem1  25262  ovolicopnf  25273  ismbl2  25276  nulmbl2  25285  unmbl  25286  voliunlem2  25300  ioombl1lem2  25308  ioombl1lem4  25310  ioombl1  25311  ioorcl2  25321  uniioombllem1  25330  uniioombllem3  25334  uniioombllem4  25335  uniioombllem5  25336  uniioombl  25338  opnmbllem  25350  volcn  25355  itg1addlem4  25448  itg1addlem4OLD  25449  mbfi1fseqlem4  25468  mbfi1fseqlem6  25470  itg2splitlem  25498  itg2split  25499  itg2monolem3  25502  itg2addlem  25508  ibladdlem  25569  itgaddlem1  25572  itgaddlem2  25573  iblabslem  25577  iblabs  25578  dvferm1lem  25736  dvferm2lem  25738  dvlip2  25747  lhop1lem  25765  lhop1  25766  lhop  25768  dvcnvrelem1  25769  dvcnvrelem2  25770  dvcnvre  25771  dvcvx  25772  dvfsumlem3  25780  dvfsumlem4  25781  dvfsum2  25786  ftc1lem4  25791  coemullem  25999  ulmbdd  26146  ulmcn  26147  ulmdvlem1  26148  radcnvle  26168  pserdvlem1  26175  pserdv  26177  abelthlem7  26186  pilem2  26200  pilem3  26201  cosordlem  26275  abslogle  26362  logccv  26407  cxpaddle  26496  ang180lem2  26551  heron  26579  atanlogaddlem  26654  atans2  26672  cxp2limlem  26716  scvxcvx  26726  jensenlem2  26728  amgmlem  26730  logdiflbnd  26735  harmonicbnd4  26751  fsumharmonic  26752  lgamgulmlem3  26771  lgamgulmlem4  26772  lgamgulmlem5  26773  lgamgulmlem6  26774  lgambdd  26777  lgamucov  26778  regamcl  26801  ftalem5  26817  efnnfsumcl  26843  efchtdvds  26899  chtublem  26950  chtub  26951  logfaclbnd  26961  perfectlem2  26969  bposlem7  27029  bposlem9  27031  lgsdirprm  27070  gausslemma2dlem1a  27104  2sqlem8  27165  chpchtlim  27218  vmadivsumb  27222  rplogsumlem1  27223  dchrisumlem2  27229  dchrvmasumlem2  27237  dchrvmasumiflem1  27240  dchrisum0re  27252  dchrisum0lem1b  27254  mulog2sumlem1  27273  mulog2sumlem2  27274  logsqvma2  27282  log2sumbnd  27283  selberglem2  27285  selbergb  27288  selberg2b  27291  chpdifbndlem1  27292  chpdifbndlem2  27293  selberg3lem2  27297  selberg3  27298  selberg4lem1  27299  selberg4  27300  pntrsumbnd2  27306  selberg3r  27308  selberg34r  27310  pntsf  27312  pntrlog2bndlem1  27316  pntrlog2bndlem2  27317  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntrlog2bnd  27323  pntpbnd1a  27324  pntpbnd2  27326  pntibndlem2a  27329  pntibndlem2  27330  pntibndlem3  27331  pntlemg  27337  pntlemr  27341  pntlemk  27345  pntlemo  27346  pntlem3  27348  abvcxp  27354  padicabv  27369  ostth2lem2  27373  ostth3  27377  brbtwn2  28430  axsegconlem8  28449  axsegconlem10  28451  axpaschlem  28465  axpasch  28466  axeuclidlem  28487  axcontlem2  28490  crctcshwlkn0lem3  29333  crctcshwlkn0lem5  29335  vacn  30214  smcnlem  30217  ubthlem2  30391  minvecolem2  30395  minvecolem3  30396  minvecolem4  30400  minvecolem5  30401  nmoptrii  31614  hstle  31750  staddi  31766  stadd3i  31768  lt2addrd  32231  nndiffz1  32264  wrdt2ind  32384  cshwrnid  32392  fsumrp0cl  32463  pmtrto1cl  32528  fzto1st  32532  psgnfzto1st  32534  1smat1  33082  sqsscirc1  33186  cnre2csqlem  33188  tpr2rico  33190  nexple  33305  dya2iocress  33571  dya2iocbrsiga  33572  dya2icobrsiga  33573  dya2icoseg  33574  dya2iocucvr  33581  sxbrsigalem2  33583  omssubaddlem  33596  fibp1  33698  ballotlemfc0  33789  ballotlemfcc  33790  ballotlemsgt1  33807  ballotlemsel1i  33809  plymulx0  33856  breprexplemc  33942  breprexp  33943  logdivsqrle  33960  resconn  34535  faclim  35020  dnizphlfeqhlf  35655  dnibndlem4  35660  dnibndlem6  35662  dnibndlem8  35664  dnibndlem9  35665  dnibndlem10  35666  dnibndlem11  35667  dnibndlem13  35669  dnibnd  35670  knoppcnlem4  35675  unblimceq0lem  35685  unblimceq0  35686  unbdqndv2lem1  35688  poimirlem29  36820  heicant  36826  opnmbllem0  36827  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  mbfposadd  36838  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  ibladdnclem  36847  itgaddnclem1  36849  itgaddnclem2  36850  iblabsnclem  36854  iblabsnc  36855  iblmulc2nc  36856  ftc1cnnclem  36862  ftc1anclem4  36867  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  areacirclem5  36883  mettrifi  36928  isbnd3  36955  ssbnd  36959  cntotbnd  36967  heibor1lem  36980  bfplem2  36994  rrnequiv  37006  iccbnd  37011  lcmineqlem18  41217  lcmineqlem20  41219  aks4d1p1p3  41240  aks4d1p1p2  41241  aks4d1p1p4  41242  aks4d1p1p6  41244  aks4d1p1p7  41245  aks4d1p1p5  41246  aks4d1p1  41247  2np3bcnp1  41266  2ap1caineq  41267  sticksstones6  41273  sticksstones7  41274  sticksstones10  41277  sticksstones12a  41279  sticksstones12  41280  sticksstones22  41290  metakunt29  41319  2xp3dxp2ge1d  41328  factwoffsmonot  41329  readdridaddlidd  41480  resubeulem1  41550  resubeulem2  41551  resubeu  41552  readdsub  41559  reladdrsub  41560  resubidaddlidlem  41569  renegid2  41588  sn-it0e0  41590  sn-0tie0  41614  sn-addlt0d  41621  sn-addgt0d  41622  cnreeu  41643  dffltz  41678  fltnltalem  41706  fltnlta  41707  3cubeslem1  41724  pellexlem2  41870  pell1qrge1  41910  pell14qrgapw  41916  pellqrexplicit  41917  pellqrex  41919  pellfundge  41922  pellfundgt1  41923  rmspecfund  41949  rmxycomplete  41958  ltrmynn0  41989  jm2.24nn  42000  jm2.24  42004  fzmaxdif  42022  jm2.26lem3  42042  jm3.1lem2  42059  areaquad  42267  sqrtcvallem4  42692  sqrtcvallem5  42693  sqrtcval  42694  imo72b2lem0  43219  hashnzfzclim  43383  binomcxplemnotnn0  43417  zltlesub  44293  lt3addmuld  44309  absnpncan2d  44310  fperiodmullem  44311  lt4addmuld  44314  absnpncan3d  44315  leadd12dd  44324  supxrgelem  44345  supxrge  44346  ltadd12dd  44351  xralrple2  44362  infxr  44375  infleinflem2  44379  xralrple4  44381  xralrple3  44382  xrralrecnnle  44391  eliooshift  44517  iccshift  44529  iooshift  44533  iooiinicc  44553  iooiinioc  44567  fsumnncl  44586  climinf  44620  climsuselem1  44621  sumnnodd  44644  lptre2pt  44654  addlimc  44662  0ellimcdiv  44663  limclner  44665  climleltrp  44690  liminfltlem  44818  fperdvper  44933  dvdivbd  44937  dvbdfbdioolem2  44943  dvbdfbdioo  44944  ioodvbdlimc1lem1  44945  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvxpaek  44954  dvnmul  44957  iblsplit  44980  iblspltprt  44987  itgspltprt  44993  itgiccshift  44994  itgperiod  44995  itgsbtaddcnst  44996  stoweidlem1  45015  stoweidlem11  45025  stoweidlem13  45027  stoweidlem14  45028  stoweidlem20  45034  stoweidlem21  45035  stoweidlem26  45040  stoweidlem44  45058  stoweidlem60  45074  wallispilem3  45081  wallispilem4  45082  wallispilem5  45083  wallispi  45084  wallispi2lem1  45085  wallispi2lem2  45086  stirlinglem1  45088  stirlinglem3  45090  stirlinglem5  45092  stirlinglem6  45093  stirlinglem7  45094  stirlinglem10  45097  stirlinglem11  45098  stirlinglem12  45099  dirker2re  45106  dirkerval2  45108  dirkerre  45109  dirkerper  45110  dirkertrigeqlem1  45112  dirkertrigeqlem2  45113  dirkeritg  45116  dirkercncflem1  45117  dirkercncflem2  45118  dirkercncflem4  45120  fourierdlem4  45125  fourierdlem5  45126  fourierdlem6  45127  fourierdlem7  45128  fourierdlem9  45130  fourierdlem10  45131  fourierdlem18  45139  fourierdlem19  45140  fourierdlem20  45141  fourierdlem26  45147  fourierdlem28  45149  fourierdlem30  45151  fourierdlem35  45156  fourierdlem40  45161  fourierdlem41  45162  fourierdlem42  45163  fourierdlem47  45167  fourierdlem48  45168  fourierdlem49  45169  fourierdlem50  45170  fourierdlem51  45171  fourierdlem53  45173  fourierdlem57  45177  fourierdlem59  45179  fourierdlem60  45180  fourierdlem61  45181  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem66  45186  fourierdlem68  45188  fourierdlem71  45191  fourierdlem72  45192  fourierdlem74  45194  fourierdlem75  45195  fourierdlem76  45196  fourierdlem78  45198  fourierdlem79  45199  fourierdlem80  45200  fourierdlem81  45201  fourierdlem82  45202  fourierdlem83  45203  fourierdlem84  45204  fourierdlem87  45207  fourierdlem88  45208  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  fourierdlem92  45212  fourierdlem93  45213  fourierdlem94  45214  fourierdlem95  45215  fourierdlem97  45217  fourierdlem101  45221  fourierdlem103  45223  fourierdlem104  45224  fourierdlem111  45231  fourierdlem112  45232  fourierdlem113  45233  sqwvfoura  45242  sqwvfourb  45243  fouriersw  45245  qndenserrnbllem  45308  ioorrnopnlem  45318  ioorrnopnxrlem  45320  sge0xaddlem1  45447  sge0xaddlem2  45448  omeiunltfirp  45533  carageniuncllem2  45536  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  hoidmvlelem4  45612  hoiqssbllem1  45636  hoiqssbllem2  45637  hoiqssbllem3  45638  hspmbllem2  45641  hspmbllem3  45642  ovolval5lem1  45666  iinhoiicclem  45687  iinhoiicc  45688  iunhoiioolem  45689  iccvonmbllem  45692  vonioolem1  45694  vonioolem2  45695  vonicclem1  45697  vonicclem2  45698  preimaleiinlt  45735  salpreimaltle  45740  smfaddlem1  45777  smfadd  45779  smflimlem3  45787  smflimlem4  45788  smflimlem6  45790  smfmullem1  45805  smfmullem2  45806  smfmullem3  45807  zm1nn  46308  requad01  46587  requad1  46588  requad2  46589  perfectALTVlem2  46688  nnsum4primesevenALTV  46767  bgoldbtbndlem2  46772  dignn0flhalflem1  47388  affinecomb1  47475  resum2sqcl  47479  2sphere  47522  line2  47525  itsclc0lem1  47529  itscnhlc0yqe  47532  itsclquadb  47549  2itscp  47554  itscnhlinecirc02plem1  47555  itscnhlinecirc02plem3  47557  itscnhlinecirc02p  47558  inlinecirc02plem  47559  amgmwlem  47936