Theorem readdcld 11173

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037   + caddc 11041

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

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

This theorem is referenced by:  ltadd2  11249  readdcan  11319  addrid  11325  leadd1  11617  le2add  11631  lesub2  11644  lesub3d  11767  le2addd  11768  supaddc  12121  supadd  12122  cju  12153  nnne0  12191  div4p1lem1div2  12408  difgtsumgt  12466  eluzmn  12770  rpnnen1lem5  12906  addlelt  13033  xralrple  13132  xov1plusxeqvd  13426  zltaddlt1le  13433  elincfzoext  13651  fladdz  13757  2tnp1ge0ge0  13761  flhalf  13762  fldiv  13792  modaddb  13841  modaddmodup  13869  modaddmodlo  13870  addmodlteq  13881  discr1  14174  discr  14175  ccatalpha  14529  2cshw  14748  remim  15052  remullem  15063  01sqrexlem7  15183  absrele  15243  abstri  15266  abs3lem  15274  amgm2  15305  bhmafibid1  15403  mulcn2  15531  o1add  15549  o1sub  15551  lo1add  15562  caucvgrlem  15608  iseraltlem2  15618  iseraltlem3  15619  fsumabs  15736  o1fsum  15748  climcndslem2  15785  tanhlt1  16097  eirrlem  16141  ruclem1  16168  ruclem2  16169  ruclem3  16170  ltoddhalfle  16300  bitscmp  16377  sadcaddlem  16396  sadasslem  16409  smuval2  16421  iserodd  16775  prmreclem4  16859  4sqlem5  16882  4sqlem6  16883  4sqlem12  16896  4sqlem15  16899  4sqlem16  16900  prmgaplem7  16997  prmgaplem8  16998  2expltfac  17032  cshwshashlem2  17036  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  prdsxmetlem  24324  xblss2ps  24357  metustexhalf  24512  nrmmetd  24530  ngptgp  24592  nlmvscnlem2  24641  nlmvscnlem1  24642  nmotri  24695  nghmplusg  24696  blcvx  24754  iccntr  24778  icccmplem2  24780  reconnlem2  24784  metdcnlem  24793  metnrmlem3  24818  cnllycmp  24923  lebnumii  24933  tcphcphlem1  25203  ipcnlem2  25212  ipcnlem1  25213  csbren  25367  trirn  25368  minveclem2  25394  minveclem3b  25396  minveclem4  25400  ivthlem2  25421  ovolgelb  25449  ovollb2lem  25457  ovolunlem1a  25465  ovolunlem1  25466  ovolfiniun  25470  ovoliunlem1  25471  ovoliunlem2  25472  ovolshftlem1  25478  ovolscalem1  25482  ovolicopnf  25493  ismbl2  25496  nulmbl2  25505  unmbl  25506  voliunlem2  25520  ioombl1lem2  25528  ioombl1lem4  25530  ioombl1  25531  ioorcl2  25541  uniioombllem1  25550  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombl  25558  opnmbllem  25570  volcn  25575  itg1addlem4  25668  mbfi1fseqlem4  25687  mbfi1fseqlem6  25689  itg2splitlem  25717  itg2split  25718  itg2monolem3  25721  itg2addlem  25727  ibladdlem  25789  itgaddlem1  25792  itgaddlem2  25793  iblabslem  25797  iblabs  25798  dvferm1lem  25956  dvferm2lem  25958  dvlip2  25968  lhop1lem  25986  lhop1  25987  lhop  25989  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcnvre  25992  dvcvx  25993  dvfsumlem3  26003  dvfsumlem4  26004  dvfsum2  26009  ftc1lem4  26014  coemullem  26223  ulmbdd  26375  ulmcn  26376  ulmdvlem1  26377  radcnvle  26397  pserdvlem1  26405  pserdv  26407  abelthlem7  26416  pilem2  26430  pilem3  26431  cosordlem  26507  abslogle  26595  logccv  26640  cxpaddle  26730  ang180lem2  26788  heron  26816  atanlogaddlem  26891  atans2  26909  cxp2limlem  26954  scvxcvx  26964  jensenlem2  26966  amgmlem  26968  logdiflbnd  26973  harmonicbnd4  26989  fsumharmonic  26990  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgambdd  27015  lgamucov  27016  regamcl  27039  ftalem5  27055  efnnfsumcl  27081  efchtdvds  27137  chtublem  27190  chtub  27191  logfaclbnd  27201  perfectlem2  27209  bposlem7  27269  bposlem9  27271  lgsdirprm  27310  gausslemma2dlem1a  27344  2sqlem8  27405  chpchtlim  27458  vmadivsumb  27462  rplogsumlem1  27463  dchrisumlem2  27469  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0re  27492  dchrisum0lem1b  27494  mulog2sumlem1  27513  mulog2sumlem2  27514  logsqvma2  27522  log2sumbnd  27523  selberglem2  27525  selbergb  27528  selberg2b  27531  chpdifbndlem1  27532  chpdifbndlem2  27533  selberg3lem2  27537  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrsumbnd2  27546  selberg3r  27548  selberg34r  27550  pntsf  27552  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem2a  27569  pntibndlem2  27570  pntibndlem3  27571  pntlemg  27577  pntlemr  27581  pntlemk  27585  pntlemo  27586  pntlem3  27588  abvcxp  27594  padicabv  27609  ostth2lem2  27613  ostth3  27617  brbtwn2  28990  axsegconlem8  29009  axsegconlem10  29011  axpaschlem  29025  axpasch  29026  axeuclidlem  29047  axcontlem2  29050  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  vacn  30781  smcnlem  30784  ubthlem2  30958  minvecolem2  30962  minvecolem3  30963  minvecolem4  30967  minvecolem5  30968  nmoptrii  32181  hstle  32317  staddi  32333  stadd3i  32335  lt2addrd  32840  nndiffz1  32876  nexple  32935  wrdt2ind  33045  cshwrnid  33053  fsumrp0cl  33113  pmtrto1cl  33192  fzto1st  33196  psgnfzto1st  33198  constrresqrtcl  33954  cos9thpiminplylem1  33959  1smat1  33981  sqsscirc1  34085  cnre2csqlem  34087  tpr2rico  34089  dya2iocress  34451  dya2iocbrsiga  34452  dya2icobrsiga  34453  dya2icoseg  34454  dya2iocucvr  34461  sxbrsigalem2  34463  omssubaddlem  34476  fibp1  34578  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemsgt1  34688  ballotlemsel1i  34690  plymulx0  34724  breprexplemc  34809  breprexp  34810  logdivsqrle  34827  resconn  35459  faclim  35959  dnizphlfeqhlf  36695  dnibndlem4  36700  dnibndlem6  36702  dnibndlem8  36704  dnibndlem9  36705  dnibndlem10  36706  dnibndlem11  36707  dnibndlem13  36709  dnibnd  36710  knoppcnlem4  36715  unblimceq0lem  36725  unblimceq0  36726  unbdqndv2lem1  36728  poimirlem29  37894  heicant  37900  opnmbllem0  37901  mblfinlem3  37904  mblfinlem4  37905  ismblfin  37906  mbfposadd  37912  itg2addnclem  37916  itg2addnclem3  37918  itg2addnc  37919  itg2gt0cn  37920  ibladdnclem  37921  itgaddnclem1  37923  itgaddnclem2  37924  iblabsnclem  37928  iblabsnc  37929  iblmulc2nc  37930  ftc1cnnclem  37936  ftc1anclem4  37941  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  areacirclem5  37957  mettrifi  38002  isbnd3  38029  ssbnd  38033  cntotbnd  38041  heibor1lem  38054  bfplem2  38068  rrnequiv  38080  iccbnd  38085  lcmineqlem18  42410  lcmineqlem20  42412  aks4d1p1p3  42433  aks4d1p1p2  42434  aks4d1p1p4  42435  aks4d1p1p6  42437  aks4d1p1p7  42438  aks4d1p1p5  42439  aks4d1p1  42440  posbezout  42464  aks6d1c1  42480  aks6d1c2  42494  2np3bcnp1  42508  2ap1caineq  42509  sticksstones6  42515  sticksstones7  42516  sticksstones10  42519  sticksstones12a  42521  sticksstones12  42522  sticksstones22  42532  bcle2d  42543  aks6d1c7lem1  42544  readdridaddlidd  42622  resubeulem1  42739  resubeulem2  42740  resubeu  42741  readdsub  42748  reladdrsub  42749  resubidaddlidlem  42758  renegid2  42778  sn-it0e0  42780  sn-0tie0  42815  sn-addlt0d  42822  sn-addgt0d  42823  cnreeu  42854  dffltz  42986  fltnltalem  43014  fltnlta  43015  3cubeslem1  43035  pellexlem2  43181  pell1qrge1  43221  pell14qrgapw  43227  pellqrexplicit  43228  pellqrex  43230  pellfundge  43233  pellfundgt1  43234  rmspecfund  43260  rmxycomplete  43268  ltrmynn0  43299  jm2.24nn  43310  jm2.24  43314  fzmaxdif  43332  jm2.26lem3  43352  jm3.1lem2  43369  areaquad  43567  sqrtcvallem4  43989  sqrtcvallem5  43990  sqrtcval  43991  imo72b2lem0  44515  hashnzfzclim  44672  binomcxplemnotnn0  44706  zltlesub  45641  lt3addmuld  45657  absnpncan2d  45658  fperiodmullem  45659  lt4addmuld  45662  absnpncan3d  45663  supxrgelem  45690  supxrge  45691  ltadd12dd  45696  xralrple2  45707  infxr  45719  infleinflem2  45723  xralrple4  45725  xralrple3  45726  xrralrecnnle  45735  eliooshift  45860  iccshift  45872  iooshift  45876  iooiinicc  45896  iooiinioc  45910  fsumnncl  45926  climinf  45960  climsuselem1  45961  sumnnodd  45984  lptre2pt  45992  addlimc  46000  0ellimcdiv  46001  limclner  46003  climleltrp  46028  liminfltlem  46156  fperdvper  46271  dvdivbd  46275  dvbdfbdioolem2  46281  dvbdfbdioo  46282  ioodvbdlimc1lem1  46283  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvxpaek  46292  dvnmul  46295  iblsplit  46318  iblspltprt  46325  itgspltprt  46331  itgiccshift  46332  itgperiod  46333  itgsbtaddcnst  46334  stoweidlem1  46353  stoweidlem11  46363  stoweidlem13  46365  stoweidlem14  46366  stoweidlem20  46372  stoweidlem21  46373  stoweidlem26  46378  stoweidlem44  46396  stoweidlem60  46412  wallispilem3  46419  wallispilem4  46420  wallispilem5  46421  wallispi  46422  wallispi2lem1  46423  wallispi2lem2  46424  stirlinglem1  46426  stirlinglem3  46428  stirlinglem5  46430  stirlinglem6  46431  stirlinglem7  46432  stirlinglem10  46435  stirlinglem11  46436  stirlinglem12  46437  dirker2re  46444  dirkerval2  46446  dirkerre  46447  dirkerper  46448  dirkertrigeqlem1  46450  dirkertrigeqlem2  46451  dirkeritg  46454  dirkercncflem1  46455  dirkercncflem2  46456  dirkercncflem4  46458  fourierdlem4  46463  fourierdlem5  46464  fourierdlem6  46465  fourierdlem7  46466  fourierdlem9  46468  fourierdlem10  46469  fourierdlem18  46477  fourierdlem19  46478  fourierdlem20  46479  fourierdlem26  46485  fourierdlem28  46487  fourierdlem30  46489  fourierdlem35  46494  fourierdlem40  46499  fourierdlem41  46500  fourierdlem42  46501  fourierdlem47  46505  fourierdlem48  46506  fourierdlem49  46507  fourierdlem50  46508  fourierdlem51  46509  fourierdlem53  46511  fourierdlem57  46515  fourierdlem59  46517  fourierdlem60  46518  fourierdlem61  46519  fourierdlem63  46521  fourierdlem64  46522  fourierdlem65  46523  fourierdlem66  46524  fourierdlem68  46526  fourierdlem71  46529  fourierdlem72  46530  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem78  46536  fourierdlem79  46537  fourierdlem80  46538  fourierdlem81  46539  fourierdlem82  46540  fourierdlem83  46541  fourierdlem84  46542  fourierdlem87  46545  fourierdlem88  46546  fourierdlem89  46547  fourierdlem90  46548  fourierdlem91  46549  fourierdlem92  46550  fourierdlem93  46551  fourierdlem94  46552  fourierdlem95  46553  fourierdlem97  46555  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fourierdlem112  46570  fourierdlem113  46571  sqwvfoura  46580  sqwvfourb  46581  fouriersw  46583  qndenserrnbllem  46646  ioorrnopnlem  46656  ioorrnopnxrlem  46658  sge0xaddlem1  46785  sge0xaddlem2  46786  omeiunltfirp  46871  carageniuncllem2  46874  hoidmv1lelem1  46943  hoidmv1lelem2  46944  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hoiqssbllem1  46974  hoiqssbllem2  46975  hoiqssbllem3  46976  hspmbllem2  46979  hspmbllem3  46980  ovolval5lem1  47004  iinhoiicclem  47025  iinhoiicc  47026  iunhoiioolem  47027  iccvonmbllem  47030  vonioolem1  47032  vonioolem2  47033  vonicclem1  47035  vonicclem2  47036  preimaleiinlt  47073  salpreimaltle  47078  smfaddlem1  47115  smfadd  47117  smflimlem3  47125  smflimlem4  47126  smflimlem6  47128  smfmullem1  47143  smfmullem2  47144  smfmullem3  47145  ormkglobd  47227  zm1nn  47656  requad01  47975  requad1  47976  requad2  47977  perfectALTVlem2  48076  nnsum4primesevenALTV  48155  bgoldbtbndlem2  48160  gpgvtxedg0  48417  gpgvtxedg1  48418  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx13starlem2  48426  dignn0flhalflem1  48969  affinecomb1  49056  resum2sqcl  49060  2sphere  49103  line2  49106  itsclc0lem1  49110  itscnhlc0yqe  49113  itsclquadb  49130  2itscp  49135  itscnhlinecirc02plem1  49136  itscnhlinecirc02plem3  49138  itscnhlinecirc02p  49139  inlinecirc02plem  49140  amgmwlem  50155