Theorem readdcld 11243

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109   + caddc 11113

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

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

This theorem is referenced by:  ltadd2  11318  readdcan  11388  addrid  11394  leadd1  11682  le2add  11696  lesub2  11709  lesub3d  11832  supaddc  12181  supadd  12182  cju  12208  nnne0  12246  div4p1lem1div2  12467  difgtsumgt  12525  eluzmn  12829  rpnnen1lem5  12965  addlelt  13088  xralrple  13184  xov1plusxeqvd  13475  zltaddlt1le  13482  elincfzoext  13690  fladdz  13790  2tnp1ge0ge0  13794  flhalf  13795  fldiv  13825  modaddmodup  13899  modaddmodlo  13900  addmodlteq  13911  discr1  14202  discr  14203  ccatalpha  14543  2cshw  14763  remim  15064  remullem  15075  01sqrexlem7  15195  absrele  15255  abstri  15277  abs3lem  15285  amgm2  15316  bhmafibid1  15412  mulcn2  15540  o1add  15558  o1sub  15560  lo1add  15571  caucvgrlem  15619  iseraltlem2  15629  iseraltlem3  15630  fsumabs  15747  o1fsum  15759  climcndslem2  15796  tanhlt1  16103  eirrlem  16147  ruclem1  16174  ruclem2  16175  ruclem3  16176  ltoddhalfle  16304  bitscmp  16379  sadcaddlem  16398  sadasslem  16411  smuval2  16423  iserodd  16768  prmreclem4  16852  4sqlem5  16875  4sqlem6  16876  4sqlem12  16889  4sqlem15  16892  4sqlem16  16893  prmgaplem7  16990  prmgaplem8  16991  2expltfac  17026  cshwshashlem2  17030  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  prdsxmetlem  23874  xblss2ps  23907  metustexhalf  24065  nrmmetd  24083  ngptgp  24145  nlmvscnlem2  24202  nlmvscnlem1  24203  nmotri  24256  nghmplusg  24257  blcvx  24314  iccntr  24337  icccmplem2  24339  reconnlem2  24343  metdcnlem  24352  metnrmlem3  24377  cnllycmp  24472  lebnumii  24482  tcphcphlem1  24752  ipcnlem2  24761  ipcnlem1  24762  csbren  24916  trirn  24917  minveclem2  24943  minveclem3b  24945  minveclem4  24949  ivthlem2  24969  ovolgelb  24997  ovollb2lem  25005  ovolunlem1a  25013  ovolunlem1  25014  ovolfiniun  25018  ovoliunlem1  25019  ovoliunlem2  25020  ovolshftlem1  25026  ovolscalem1  25030  ovolicopnf  25041  ismbl2  25044  nulmbl2  25053  unmbl  25054  voliunlem2  25068  ioombl1lem2  25076  ioombl1lem4  25078  ioombl1  25079  ioorcl2  25089  uniioombllem1  25098  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombl  25106  opnmbllem  25118  volcn  25123  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1fseqlem4  25236  mbfi1fseqlem6  25238  itg2splitlem  25266  itg2split  25267  itg2monolem3  25270  itg2addlem  25276  ibladdlem  25337  itgaddlem1  25340  itgaddlem2  25341  iblabslem  25345  iblabs  25346  dvferm1lem  25501  dvferm2lem  25503  dvlip2  25512  lhop1lem  25530  lhop1  25531  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcnvre  25536  dvcvx  25537  dvfsumlem3  25545  dvfsumlem4  25546  dvfsum2  25551  ftc1lem4  25556  coemullem  25764  ulmbdd  25910  ulmcn  25911  ulmdvlem1  25912  radcnvle  25932  pserdvlem1  25939  pserdv  25941  abelthlem7  25950  pilem2  25964  pilem3  25965  cosordlem  26039  abslogle  26126  logccv  26171  cxpaddle  26260  ang180lem2  26315  heron  26343  atanlogaddlem  26418  atans2  26436  cxp2limlem  26480  scvxcvx  26490  jensenlem2  26492  amgmlem  26494  logdiflbnd  26499  harmonicbnd4  26515  fsumharmonic  26516  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgambdd  26541  lgamucov  26542  regamcl  26565  ftalem5  26581  efnnfsumcl  26607  efchtdvds  26663  chtublem  26714  chtub  26715  logfaclbnd  26725  perfectlem2  26733  bposlem7  26793  bposlem9  26795  lgsdirprm  26834  gausslemma2dlem1a  26868  2sqlem8  26929  chpchtlim  26982  vmadivsumb  26986  rplogsumlem1  26987  dchrisumlem2  26993  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0re  27016  dchrisum0lem1b  27018  mulog2sumlem1  27037  mulog2sumlem2  27038  logsqvma2  27046  log2sumbnd  27047  selberglem2  27049  selbergb  27052  selberg2b  27055  chpdifbndlem1  27056  chpdifbndlem2  27057  selberg3lem2  27061  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrsumbnd2  27070  selberg3r  27072  selberg34r  27074  pntsf  27076  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2a  27093  pntibndlem2  27094  pntibndlem3  27095  pntlemg  27101  pntlemr  27105  pntlemk  27109  pntlemo  27110  pntlem3  27112  abvcxp  27118  padicabv  27133  ostth2lem2  27137  ostth3  27141  brbtwn2  28163  axsegconlem8  28182  axsegconlem10  28184  axpaschlem  28198  axpasch  28199  axeuclidlem  28220  axcontlem2  28223  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  vacn  29947  smcnlem  29950  ubthlem2  30124  minvecolem2  30128  minvecolem3  30129  minvecolem4  30133  minvecolem5  30134  nmoptrii  31347  hstle  31483  staddi  31499  stadd3i  31501  lt2addrd  31964  nndiffz1  31997  wrdt2ind  32117  cshwrnid  32125  fsumrp0cl  32196  pmtrto1cl  32258  fzto1st  32262  psgnfzto1st  32264  1smat1  32784  sqsscirc1  32888  cnre2csqlem  32890  tpr2rico  32892  nexple  33007  dya2iocress  33273  dya2iocbrsiga  33274  dya2icobrsiga  33275  dya2icoseg  33276  dya2iocucvr  33283  sxbrsigalem2  33285  omssubaddlem  33298  fibp1  33400  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemsgt1  33509  ballotlemsel1i  33511  plymulx0  33558  breprexplemc  33644  breprexp  33645  logdivsqrle  33662  resconn  34237  faclim  34716  dnizphlfeqhlf  35352  dnibndlem4  35357  dnibndlem6  35359  dnibndlem8  35361  dnibndlem9  35362  dnibndlem10  35363  dnibndlem11  35364  dnibndlem13  35366  dnibnd  35367  knoppcnlem4  35372  unblimceq0lem  35382  unblimceq0  35383  unbdqndv2lem1  35385  poimirlem29  36517  heicant  36523  opnmbllem0  36524  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  mbfposadd  36535  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem1  36546  itgaddnclem2  36547  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  ftc1cnnclem  36559  ftc1anclem4  36564  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  areacirclem5  36580  mettrifi  36625  isbnd3  36652  ssbnd  36656  cntotbnd  36664  heibor1lem  36677  bfplem2  36691  rrnequiv  36703  iccbnd  36708  lcmineqlem18  40911  lcmineqlem20  40913  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  2np3bcnp1  40960  2ap1caineq  40961  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  sticksstones22  40984  metakunt29  41013  2xp3dxp2ge1d  41022  factwoffsmonot  41023  readdridaddlidd  41178  resubeulem1  41248  resubeulem2  41249  resubeu  41250  readdsub  41257  reladdrsub  41258  resubidaddlidlem  41267  renegid2  41286  sn-it0e0  41288  sn-0tie0  41312  sn-addlt0d  41319  sn-addgt0d  41320  cnreeu  41341  dffltz  41376  fltnltalem  41404  fltnlta  41405  3cubeslem1  41422  pellexlem2  41568  pell1qrge1  41608  pell14qrgapw  41614  pellqrexplicit  41615  pellqrex  41617  pellfundge  41620  pellfundgt1  41621  rmspecfund  41647  rmxycomplete  41656  ltrmynn0  41687  jm2.24nn  41698  jm2.24  41702  fzmaxdif  41720  jm2.26lem3  41740  jm3.1lem2  41757  areaquad  41965  sqrtcvallem4  42390  sqrtcvallem5  42391  sqrtcval  42392  imo72b2lem0  42917  hashnzfzclim  43081  binomcxplemnotnn0  43115  zltlesub  43995  lt3addmuld  44011  absnpncan2d  44012  fperiodmullem  44013  lt4addmuld  44016  absnpncan3d  44017  leadd12dd  44026  supxrgelem  44047  supxrge  44048  ltadd12dd  44053  xralrple2  44064  infxr  44077  infleinflem2  44081  xralrple4  44083  xralrple3  44084  xrralrecnnle  44093  eliooshift  44219  iccshift  44231  iooshift  44235  iooiinicc  44255  iooiinioc  44269  fsumnncl  44288  climinf  44322  climsuselem1  44323  sumnnodd  44346  lptre2pt  44356  addlimc  44364  0ellimcdiv  44365  limclner  44367  climleltrp  44392  liminfltlem  44520  fperdvper  44635  dvdivbd  44639  dvbdfbdioolem2  44645  dvbdfbdioo  44646  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvxpaek  44656  dvnmul  44659  iblsplit  44682  iblspltprt  44689  itgspltprt  44695  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  stoweidlem1  44717  stoweidlem11  44727  stoweidlem13  44729  stoweidlem14  44730  stoweidlem20  44736  stoweidlem21  44737  stoweidlem26  44742  stoweidlem44  44760  stoweidlem60  44776  wallispilem3  44783  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  stirlinglem1  44790  stirlinglem3  44792  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  dirker2re  44808  dirkerval2  44810  dirkerre  44811  dirkerper  44812  dirkertrigeqlem1  44814  dirkertrigeqlem2  44815  dirkeritg  44818  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem4  44827  fourierdlem5  44828  fourierdlem6  44829  fourierdlem7  44830  fourierdlem9  44832  fourierdlem10  44833  fourierdlem18  44841  fourierdlem19  44842  fourierdlem20  44843  fourierdlem26  44849  fourierdlem28  44851  fourierdlem30  44853  fourierdlem35  44858  fourierdlem40  44863  fourierdlem41  44864  fourierdlem42  44865  fourierdlem47  44869  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem53  44875  fourierdlem57  44879  fourierdlem59  44881  fourierdlem60  44882  fourierdlem61  44883  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem66  44888  fourierdlem68  44890  fourierdlem71  44893  fourierdlem72  44894  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem79  44901  fourierdlem80  44902  fourierdlem81  44903  fourierdlem82  44904  fourierdlem83  44905  fourierdlem84  44906  fourierdlem87  44909  fourierdlem88  44910  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem92  44914  fourierdlem93  44915  fourierdlem94  44916  fourierdlem95  44917  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  sqwvfoura  44944  sqwvfourb  44945  fouriersw  44947  qndenserrnbllem  45010  ioorrnopnlem  45020  ioorrnopnxrlem  45022  sge0xaddlem1  45149  sge0xaddlem2  45150  omeiunltfirp  45235  carageniuncllem2  45238  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hoiqssbllem1  45338  hoiqssbllem2  45339  hoiqssbllem3  45340  hspmbllem2  45343  hspmbllem3  45344  ovolval5lem1  45368  iinhoiicclem  45389  iinhoiicc  45390  iunhoiioolem  45391  iccvonmbllem  45394  vonioolem1  45396  vonioolem2  45397  vonicclem1  45399  vonicclem2  45400  preimaleiinlt  45437  salpreimaltle  45442  smfaddlem1  45479  smfadd  45481  smflimlem3  45489  smflimlem4  45490  smflimlem6  45492  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  zm1nn  46010  requad01  46289  requad1  46290  requad2  46291  perfectALTVlem2  46390  nnsum4primesevenALTV  46469  bgoldbtbndlem2  46474  dignn0flhalflem1  47301  affinecomb1  47388  resum2sqcl  47392  2sphere  47435  line2  47438  itsclc0lem1  47442  itscnhlc0yqe  47445  itsclquadb  47462  2itscp  47467  itscnhlinecirc02plem1  47468  itscnhlinecirc02plem3  47470  itscnhlinecirc02p  47471  inlinecirc02plem  47472  amgmwlem  47849