Theorem readdcld 10670

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536   + caddc 10540

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  ltadd2  10744  readdcan  10814  addid1  10820  leadd1  11108  le2add  11122  lesub2  11135  lesub3d  11258  supaddc  11608  supadd  11609  cju  11634  nnne0  11672  div4p1lem1div2  11893  difgtsumgt  11951  eluzmn  12251  rpnnen1lem5  12381  addlelt  12504  xralrple  12599  xov1plusxeqvd  12885  zltaddlt1le  12891  elincfzoext  13096  fladdz  13196  2tnp1ge0ge0  13200  flhalf  13201  fldiv  13229  modaddmodup  13303  modaddmodlo  13304  addmodlteq  13315  discr1  13601  discr  13602  ccatalpha  13947  2cshw  14175  remim  14476  remullem  14487  sqrlem7  14608  absrele  14668  abstri  14690  abs3lem  14698  amgm2  14729  bhmafibid1  14825  mulcn2  14952  o1add  14970  o1sub  14972  lo1add  14983  caucvgrlem  15029  iseraltlem2  15039  iseraltlem3  15040  fsumabs  15156  o1fsum  15168  climcndslem2  15205  tanhlt1  15513  eirrlem  15557  ruclem1  15584  ruclem2  15585  ruclem3  15586  ltoddhalfle  15710  bitscmp  15787  sadcaddlem  15806  sadasslem  15819  smuval2  15831  iserodd  16172  prmreclem4  16255  4sqlem5  16278  4sqlem6  16279  4sqlem12  16292  4sqlem15  16295  4sqlem16  16296  prmgaplem7  16393  prmgaplem8  16394  2expltfac  16426  cshwshashlem2  16430  chfacfscmul0  21466  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulgsum  21472  prdsxmetlem  22978  xblss2ps  23011  metustexhalf  23166  nrmmetd  23184  ngptgp  23245  nlmvscnlem2  23294  nlmvscnlem1  23295  nmotri  23348  nghmplusg  23349  blcvx  23406  iccntr  23429  icccmplem2  23431  reconnlem2  23435  metdcnlem  23444  metnrmlem3  23469  cnllycmp  23560  lebnumii  23570  tcphcphlem1  23838  ipcnlem2  23847  ipcnlem1  23848  csbren  24002  trirn  24003  minveclem2  24029  minveclem3b  24031  minveclem4  24035  ivthlem2  24053  ovolgelb  24081  ovollb2lem  24089  ovolunlem1a  24097  ovolunlem1  24098  ovolfiniun  24102  ovoliunlem1  24103  ovoliunlem2  24104  ovolshftlem1  24110  ovolscalem1  24114  ovolicopnf  24125  ismbl2  24128  nulmbl2  24137  unmbl  24138  voliunlem2  24152  ioombl1lem2  24160  ioombl1lem4  24162  ioombl1  24163  ioorcl2  24173  uniioombllem1  24182  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombl  24190  opnmbllem  24202  volcn  24207  itg1addlem4  24300  mbfi1fseqlem4  24319  mbfi1fseqlem6  24321  itg2splitlem  24349  itg2split  24350  itg2monolem3  24353  itg2addlem  24359  ibladdlem  24420  itgaddlem1  24423  itgaddlem2  24424  iblabslem  24428  iblabs  24429  dvferm1lem  24581  dvferm2lem  24583  dvlip2  24592  lhop1lem  24610  lhop1  24611  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvcvx  24617  dvfsumlem3  24625  dvfsumlem4  24626  dvfsum2  24631  ftc1lem4  24636  coemullem  24840  ulmbdd  24986  ulmcn  24987  ulmdvlem1  24988  radcnvle  25008  pserdvlem1  25015  pserdv  25017  abelthlem7  25026  pilem2  25040  pilem3  25041  cosordlem  25115  abslogle  25201  logccv  25246  cxpaddle  25333  ang180lem2  25388  heron  25416  atanlogaddlem  25491  atans2  25509  cxp2limlem  25553  scvxcvx  25563  jensenlem2  25565  amgmlem  25567  logdiflbnd  25572  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem3  25608  lgamgulmlem4  25609  lgamgulmlem5  25610  lgamgulmlem6  25611  lgambdd  25614  lgamucov  25615  regamcl  25638  ftalem5  25654  efnnfsumcl  25680  efchtdvds  25736  chtublem  25787  chtub  25788  logfaclbnd  25798  perfectlem2  25806  bposlem7  25866  bposlem9  25868  lgsdirprm  25907  gausslemma2dlem1a  25941  2sqlem8  26002  chpchtlim  26055  vmadivsumb  26059  rplogsumlem1  26060  dchrisumlem2  26066  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0re  26089  dchrisum0lem1b  26091  mulog2sumlem1  26110  mulog2sumlem2  26111  logsqvma2  26119  log2sumbnd  26120  selberglem2  26122  selbergb  26125  selberg2b  26128  chpdifbndlem1  26129  chpdifbndlem2  26130  selberg3lem2  26134  selberg3  26135  selberg4lem1  26136  selberg4  26137  pntrsumbnd2  26143  selberg3r  26145  selberg34r  26147  pntsf  26149  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2a  26166  pntibndlem2  26167  pntibndlem3  26168  pntlemg  26174  pntlemr  26178  pntlemk  26182  pntlemo  26183  pntlem3  26185  abvcxp  26191  padicabv  26206  ostth2lem2  26210  ostth3  26214  brbtwn2  26691  axsegconlem8  26710  axsegconlem10  26712  axpaschlem  26726  axpasch  26727  axeuclidlem  26748  axcontlem2  26751  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  vacn  28471  smcnlem  28474  ubthlem2  28648  minvecolem2  28652  minvecolem3  28653  minvecolem4  28657  minvecolem5  28658  nmoptrii  29871  hstle  30007  staddi  30023  stadd3i  30025  lt2addrd  30475  nndiffz1  30509  wrdt2ind  30627  cshwrnid  30635  fsumrp0cl  30682  pmtrto1cl  30741  fzto1st  30745  psgnfzto1st  30747  1smat1  31069  sqsscirc1  31151  cnre2csqlem  31153  tpr2rico  31155  nexple  31268  dya2iocress  31532  dya2iocbrsiga  31533  dya2icobrsiga  31534  dya2icoseg  31535  dya2iocucvr  31542  sxbrsigalem2  31544  omssubaddlem  31557  fibp1  31659  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemsgt1  31768  ballotlemsel1i  31770  plymulx0  31817  breprexplemc  31903  breprexp  31904  logdivsqrle  31921  resconn  32493  faclim  32978  dnizphlfeqhlf  33815  dnibndlem4  33820  dnibndlem6  33822  dnibndlem8  33824  dnibndlem9  33825  dnibndlem10  33826  dnibndlem11  33827  dnibndlem13  33829  dnibnd  33830  knoppcnlem4  33835  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2lem1  33848  poimirlem29  34936  heicant  34942  opnmbllem0  34943  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  mbfposadd  34954  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  itg2gt0cn  34962  ibladdnclem  34963  itgaddnclem1  34965  itgaddnclem2  34966  iblabsnclem  34970  iblabsnc  34971  iblmulc2nc  34972  ftc1cnnclem  34980  ftc1anclem4  34985  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  areacirclem5  35001  mettrifi  35047  isbnd3  35077  ssbnd  35081  cntotbnd  35089  heibor1lem  35102  bfplem2  35116  rrnequiv  35128  iccbnd  35133  2xp3dxp2ge1d  39146  factwoffsmonot  39147  readdid1addid2d  39206  resubeulem1  39254  resubeulem2  39255  resubeu  39256  readdsub  39263  reladdrsub  39264  resubidaddid1lem  39273  dffltz  39320  fltnltalem  39323  fltnlta  39324  3cubeslem1  39330  pellexlem2  39476  pell1qrge1  39516  pell14qrgapw  39522  pellqrexplicit  39523  pellqrex  39525  pellfundge  39528  pellfundgt1  39529  rmspecfund  39555  rmxycomplete  39563  ltrmynn0  39594  jm2.24nn  39605  jm2.24  39609  fzmaxdif  39627  jm2.26lem3  39647  jm3.1lem2  39664  areaquad  39872  imo72b2lem0  40565  hashnzfzclim  40703  binomcxplemnotnn0  40737  zltlesub  41600  lt3addmuld  41617  absnpncan2d  41618  fperiodmullem  41619  lt4addmuld  41622  absnpncan3d  41623  leadd12dd  41633  supxrgelem  41654  supxrge  41655  ltadd12dd  41660  xralrple2  41671  infxr  41684  infleinflem2  41688  xralrple4  41690  xralrple3  41691  xrralrecnnle  41702  eliooshift  41831  iccshift  41843  iooshift  41847  iooiinicc  41867  iooiinioc  41881  fsumnncl  41901  climinf  41936  climsuselem1  41937  sumnnodd  41960  lptre2pt  41970  addlimc  41978  0ellimcdiv  41979  limclner  41981  climleltrp  42006  liminfltlem  42134  fperdvper  42252  dvdivbd  42257  dvbdfbdioolem2  42263  dvbdfbdioo  42264  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvxpaek  42274  dvnmul  42277  iblsplit  42300  iblspltprt  42307  itgspltprt  42313  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  stoweidlem1  42335  stoweidlem11  42345  stoweidlem13  42347  stoweidlem14  42348  stoweidlem20  42354  stoweidlem21  42355  stoweidlem26  42360  stoweidlem44  42378  stoweidlem60  42394  wallispilem3  42401  wallispilem4  42402  wallispilem5  42403  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem1  42408  stirlinglem3  42410  stirlinglem5  42412  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem11  42418  stirlinglem12  42419  dirker2re  42426  dirkerval2  42428  dirkerre  42429  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem2  42433  dirkeritg  42436  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem4  42445  fourierdlem5  42446  fourierdlem6  42447  fourierdlem7  42448  fourierdlem9  42450  fourierdlem10  42451  fourierdlem18  42459  fourierdlem19  42460  fourierdlem20  42461  fourierdlem26  42467  fourierdlem28  42469  fourierdlem30  42471  fourierdlem35  42476  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem47  42487  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem53  42493  fourierdlem57  42497  fourierdlem59  42499  fourierdlem60  42500  fourierdlem61  42501  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem66  42506  fourierdlem68  42508  fourierdlem71  42511  fourierdlem72  42512  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem79  42519  fourierdlem80  42520  fourierdlem81  42521  fourierdlem82  42522  fourierdlem83  42523  fourierdlem84  42524  fourierdlem87  42527  fourierdlem88  42528  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem92  42532  fourierdlem93  42533  fourierdlem94  42534  fourierdlem95  42535  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  qndenserrnbllem  42628  ioorrnopnlem  42638  ioorrnopnxrlem  42640  sge0xaddlem1  42764  sge0xaddlem2  42765  omeiunltfirp  42850  carageniuncllem2  42853  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoiqssbllem1  42953  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem2  42958  hspmbllem3  42959  ovolval5lem1  42983  iinhoiicclem  43004  iinhoiicc  43005  iunhoiioolem  43006  iccvonmbllem  43009  vonioolem1  43011  vonioolem2  43012  vonicclem1  43014  vonicclem2  43015  preimaleiinlt  43048  salpreimaltle  43052  smfaddlem1  43088  smfadd  43090  smflimlem3  43098  smflimlem4  43099  smflimlem6  43101  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  zm1nn  43551  requad01  43835  requad1  43836  requad2  43837  perfectALTVlem2  43936  nnsum4primesevenALTV  44015  bgoldbtbndlem2  44020  dignn0flhalflem1  44724  affinecomb1  44738  resum2sqcl  44742  2sphere  44785  line2  44788  itsclc0lem1  44792  itscnhlc0yqe  44795  itsclquadb  44812  2itscp  44817  itscnhlinecirc02plem1  44818  itscnhlinecirc02plem3  44820  itscnhlinecirc02p  44821  inlinecirc02plem  44822  amgmwlem  44952