Theorem readdcld 11319

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183   + caddc 11187

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

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

This theorem is referenced by:  ltadd2  11394  readdcan  11464  addrid  11470  leadd1  11758  le2add  11772  lesub2  11785  lesub3d  11908  supaddc  12262  supadd  12263  cju  12289  nnne0  12327  div4p1lem1div2  12548  difgtsumgt  12606  eluzmn  12910  rpnnen1lem5  13046  addlelt  13171  xralrple  13267  xov1plusxeqvd  13558  zltaddlt1le  13565  elincfzoext  13774  fladdz  13876  2tnp1ge0ge0  13880  flhalf  13881  fldiv  13911  modaddmodup  13985  modaddmodlo  13986  addmodlteq  13997  discr1  14288  discr  14289  ccatalpha  14641  2cshw  14861  remim  15166  remullem  15177  01sqrexlem7  15297  absrele  15357  abstri  15379  abs3lem  15387  amgm2  15418  bhmafibid1  15514  mulcn2  15642  o1add  15660  o1sub  15662  lo1add  15673  caucvgrlem  15721  iseraltlem2  15731  iseraltlem3  15732  fsumabs  15849  o1fsum  15861  climcndslem2  15898  tanhlt1  16208  eirrlem  16252  ruclem1  16279  ruclem2  16280  ruclem3  16281  ltoddhalfle  16409  bitscmp  16484  sadcaddlem  16503  sadasslem  16516  smuval2  16528  iserodd  16882  prmreclem4  16966  4sqlem5  16989  4sqlem6  16990  4sqlem12  17003  4sqlem15  17006  4sqlem16  17007  prmgaplem7  17104  prmgaplem8  17105  2expltfac  17140  cshwshashlem2  17144  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  prdsxmetlem  24399  xblss2ps  24432  metustexhalf  24590  nrmmetd  24608  ngptgp  24670  nlmvscnlem2  24727  nlmvscnlem1  24728  nmotri  24781  nghmplusg  24782  blcvx  24839  iccntr  24862  icccmplem2  24864  reconnlem2  24868  metdcnlem  24877  metnrmlem3  24902  cnllycmp  25007  lebnumii  25017  tcphcphlem1  25288  ipcnlem2  25297  ipcnlem1  25298  csbren  25452  trirn  25453  minveclem2  25479  minveclem3b  25481  minveclem4  25485  ivthlem2  25506  ovolgelb  25534  ovollb2lem  25542  ovolunlem1a  25550  ovolunlem1  25551  ovolfiniun  25555  ovoliunlem1  25556  ovoliunlem2  25557  ovolshftlem1  25563  ovolscalem1  25567  ovolicopnf  25578  ismbl2  25581  nulmbl2  25590  unmbl  25591  voliunlem2  25605  ioombl1lem2  25613  ioombl1lem4  25615  ioombl1  25616  ioorcl2  25626  uniioombllem1  25635  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombl  25643  opnmbllem  25655  volcn  25660  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1fseqlem4  25773  mbfi1fseqlem6  25775  itg2splitlem  25803  itg2split  25804  itg2monolem3  25807  itg2addlem  25813  ibladdlem  25875  itgaddlem1  25878  itgaddlem2  25879  iblabslem  25883  iblabs  25884  dvferm1lem  26042  dvferm2lem  26044  dvlip2  26054  lhop1lem  26072  lhop1  26073  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvcvx  26079  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  ftc1lem4  26100  coemullem  26309  ulmbdd  26459  ulmcn  26460  ulmdvlem1  26461  radcnvle  26481  pserdvlem1  26489  pserdv  26491  abelthlem7  26500  pilem2  26514  pilem3  26515  cosordlem  26590  abslogle  26678  logccv  26723  cxpaddle  26813  ang180lem2  26871  heron  26899  atanlogaddlem  26974  atans2  26992  cxp2limlem  27037  scvxcvx  27047  jensenlem2  27049  amgmlem  27051  logdiflbnd  27056  harmonicbnd4  27072  fsumharmonic  27073  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  lgambdd  27098  lgamucov  27099  regamcl  27122  ftalem5  27138  efnnfsumcl  27164  efchtdvds  27220  chtublem  27273  chtub  27274  logfaclbnd  27284  perfectlem2  27292  bposlem7  27352  bposlem9  27354  lgsdirprm  27393  gausslemma2dlem1a  27427  2sqlem8  27488  chpchtlim  27541  vmadivsumb  27545  rplogsumlem1  27546  dchrisumlem2  27552  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0re  27575  dchrisum0lem1b  27577  mulog2sumlem1  27596  mulog2sumlem2  27597  logsqvma2  27605  log2sumbnd  27606  selberglem2  27608  selbergb  27611  selberg2b  27614  chpdifbndlem1  27615  chpdifbndlem2  27616  selberg3lem2  27620  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrsumbnd2  27629  selberg3r  27631  selberg34r  27633  pntsf  27635  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem2a  27652  pntibndlem2  27653  pntibndlem3  27654  pntlemg  27660  pntlemr  27664  pntlemk  27668  pntlemo  27669  pntlem3  27671  abvcxp  27677  padicabv  27692  ostth2lem2  27696  ostth3  27700  brbtwn2  28938  axsegconlem8  28957  axsegconlem10  28959  axpaschlem  28973  axpasch  28974  axeuclidlem  28995  axcontlem2  28998  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  vacn  30726  smcnlem  30729  ubthlem2  30903  minvecolem2  30907  minvecolem3  30908  minvecolem4  30912  minvecolem5  30913  nmoptrii  32126  hstle  32262  staddi  32278  stadd3i  32280  lt2addrd  32758  nndiffz1  32791  wrdt2ind  32920  cshwrnid  32928  fsumrp0cl  33007  pmtrto1cl  33092  fzto1st  33096  psgnfzto1st  33098  1smat1  33750  sqsscirc1  33854  cnre2csqlem  33856  tpr2rico  33858  nexple  33973  dya2iocress  34239  dya2iocbrsiga  34240  dya2icobrsiga  34241  dya2icoseg  34242  dya2iocucvr  34249  sxbrsigalem2  34251  omssubaddlem  34264  fibp1  34366  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsgt1  34475  ballotlemsel1i  34477  plymulx0  34524  breprexplemc  34609  breprexp  34610  logdivsqrle  34627  resconn  35214  faclim  35708  dnizphlfeqhlf  36442  dnibndlem4  36447  dnibndlem6  36449  dnibndlem8  36451  dnibndlem9  36452  dnibndlem10  36453  dnibndlem11  36454  dnibndlem13  36456  dnibnd  36457  knoppcnlem4  36462  unblimceq0lem  36472  unblimceq0  36473  unbdqndv2lem1  36475  poimirlem29  37609  heicant  37615  opnmbllem0  37616  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  mbfposadd  37627  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ibladdnclem  37636  itgaddnclem1  37638  itgaddnclem2  37639  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  ftc1cnnclem  37651  ftc1anclem4  37656  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirclem5  37672  mettrifi  37717  isbnd3  37744  ssbnd  37748  cntotbnd  37756  heibor1lem  37769  bfplem2  37783  rrnequiv  37795  iccbnd  37800  lcmineqlem18  42003  lcmineqlem20  42005  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  posbezout  42057  aks6d1c1  42073  aks6d1c2  42087  2np3bcnp1  42101  2ap1caineq  42102  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  bcle2d  42136  aks6d1c7lem1  42137  metakunt29  42190  2xp3dxp2ge1d  42198  factwoffsmonot  42199  readdridaddlidd  42253  resubeulem1  42351  resubeulem2  42352  resubeu  42353  readdsub  42360  reladdrsub  42361  resubidaddlidlem  42370  renegid2  42389  sn-it0e0  42391  sn-0tie0  42415  sn-addlt0d  42422  sn-addgt0d  42423  cnreeu  42446  dffltz  42589  fltnltalem  42617  fltnlta  42618  3cubeslem1  42640  pellexlem2  42786  pell1qrge1  42826  pell14qrgapw  42832  pellqrexplicit  42833  pellqrex  42835  pellfundge  42838  pellfundgt1  42839  rmspecfund  42865  rmxycomplete  42874  ltrmynn0  42905  jm2.24nn  42916  jm2.24  42920  fzmaxdif  42938  jm2.26lem3  42958  jm3.1lem2  42975  areaquad  43177  sqrtcvallem4  43601  sqrtcvallem5  43602  sqrtcval  43603  imo72b2lem0  44127  hashnzfzclim  44291  binomcxplemnotnn0  44325  zltlesub  45200  lt3addmuld  45216  absnpncan2d  45217  fperiodmullem  45218  lt4addmuld  45221  absnpncan3d  45222  leadd12dd  45231  supxrgelem  45252  supxrge  45253  ltadd12dd  45258  xralrple2  45269  infxr  45282  infleinflem2  45286  xralrple4  45288  xralrple3  45289  xrralrecnnle  45298  eliooshift  45424  iccshift  45436  iooshift  45440  iooiinicc  45460  iooiinioc  45474  fsumnncl  45493  climinf  45527  climsuselem1  45528  sumnnodd  45551  lptre2pt  45561  addlimc  45569  0ellimcdiv  45570  limclner  45572  climleltrp  45597  liminfltlem  45725  fperdvper  45840  dvdivbd  45844  dvbdfbdioolem2  45850  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvxpaek  45861  dvnmul  45864  iblsplit  45887  iblspltprt  45894  itgspltprt  45900  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem1  45922  stoweidlem11  45932  stoweidlem13  45934  stoweidlem14  45935  stoweidlem20  45941  stoweidlem21  45942  stoweidlem26  45947  stoweidlem44  45965  stoweidlem60  45981  wallispilem3  45988  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem1  45995  stirlinglem3  45997  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  dirker2re  46013  dirkerval2  46015  dirkerre  46016  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkeritg  46023  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem4  46032  fourierdlem5  46033  fourierdlem6  46034  fourierdlem7  46035  fourierdlem9  46037  fourierdlem10  46038  fourierdlem18  46046  fourierdlem19  46047  fourierdlem20  46048  fourierdlem26  46054  fourierdlem28  46056  fourierdlem30  46058  fourierdlem35  46063  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem47  46074  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem53  46080  fourierdlem57  46084  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem66  46093  fourierdlem68  46095  fourierdlem71  46098  fourierdlem72  46099  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem80  46107  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem87  46114  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem94  46121  fourierdlem95  46122  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fouriersw  46152  qndenserrnbllem  46215  ioorrnopnlem  46225  ioorrnopnxrlem  46227  sge0xaddlem1  46354  sge0xaddlem2  46355  omeiunltfirp  46440  carageniuncllem2  46443  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoiqssbllem1  46543  hoiqssbllem2  46544  hoiqssbllem3  46545  hspmbllem2  46548  hspmbllem3  46549  ovolval5lem1  46573  iinhoiicclem  46594  iinhoiicc  46595  iunhoiioolem  46596  iccvonmbllem  46599  vonioolem1  46601  vonioolem2  46602  vonicclem1  46604  vonicclem2  46605  preimaleiinlt  46642  salpreimaltle  46647  smfaddlem1  46684  smfadd  46686  smflimlem3  46694  smflimlem4  46695  smflimlem6  46697  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  zm1nn  47217  requad01  47495  requad1  47496  requad2  47497  perfectALTVlem2  47596  nnsum4primesevenALTV  47675  bgoldbtbndlem2  47680  dignn0flhalflem1  48349  affinecomb1  48436  resum2sqcl  48440  2sphere  48483  line2  48486  itsclc0lem1  48490  itscnhlc0yqe  48493  itsclquadb  48510  2itscp  48515  itscnhlinecirc02plem1  48516  itscnhlinecirc02plem3  48518  itscnhlinecirc02p  48519  inlinecirc02plem  48520  amgmwlem  48896