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  39117  factwoffsmonot  39118  readdid1addid2d  39177  resubeulem1  39225  resubeulem2  39226  resubeu  39227  readdsub  39234  reladdrsub  39235  resubidaddid1lem  39244  dffltz  39291  fltnltalem  39294  fltnlta  39295  3cubeslem1  39301  pellexlem2  39447  pell1qrge1  39487  pell14qrgapw  39493  pellqrexplicit  39494  pellqrex  39496  pellfundge  39499  pellfundgt1  39500  rmspecfund  39526  rmxycomplete  39534  ltrmynn0  39565  jm2.24nn  39576  jm2.24  39580  fzmaxdif  39598  jm2.26lem3  39618  jm3.1lem2  39635  areaquad  39843  imo72b2lem0  40536  hashnzfzclim  40674  binomcxplemnotnn0  40708  zltlesub  41571  lt3addmuld  41588  absnpncan2d  41589  fperiodmullem  41590  lt4addmuld  41593  absnpncan3d  41594  leadd12dd  41604  supxrgelem  41625  supxrge  41626  ltadd12dd  41631  xralrple2  41642  infxr  41655  infleinflem2  41659  xralrple4  41661  xralrple3  41662  xrralrecnnle  41673  eliooshift  41802  iccshift  41814  iooshift  41818  iooiinicc  41838  iooiinioc  41852  fsumnncl  41872  climinf  41907  climsuselem1  41908  sumnnodd  41931  lptre2pt  41941  addlimc  41949  0ellimcdiv  41950  limclner  41952  climleltrp  41977  liminfltlem  42105  fperdvper  42223  dvdivbd  42228  dvbdfbdioolem2  42234  dvbdfbdioo  42235  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvxpaek  42245  dvnmul  42248  iblsplit  42271  iblspltprt  42278  itgspltprt  42284  itgiccshift  42285  itgperiod  42286  itgsbtaddcnst  42287  stoweidlem1  42306  stoweidlem11  42316  stoweidlem13  42318  stoweidlem14  42319  stoweidlem20  42325  stoweidlem21  42326  stoweidlem26  42331  stoweidlem44  42349  stoweidlem60  42365  wallispilem3  42372  wallispilem4  42373  wallispilem5  42374  wallispi  42375  wallispi2lem1  42376  wallispi2lem2  42377  stirlinglem1  42379  stirlinglem3  42381  stirlinglem5  42383  stirlinglem6  42384  stirlinglem7  42385  stirlinglem10  42388  stirlinglem11  42389  stirlinglem12  42390  dirker2re  42397  dirkerval2  42399  dirkerre  42400  dirkerper  42401  dirkertrigeqlem1  42403  dirkertrigeqlem2  42404  dirkeritg  42407  dirkercncflem1  42408  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem4  42416  fourierdlem5  42417  fourierdlem6  42418  fourierdlem7  42419  fourierdlem9  42421  fourierdlem10  42422  fourierdlem18  42430  fourierdlem19  42431  fourierdlem20  42432  fourierdlem26  42438  fourierdlem28  42440  fourierdlem30  42442  fourierdlem35  42447  fourierdlem40  42452  fourierdlem41  42453  fourierdlem42  42454  fourierdlem47  42458  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem51  42462  fourierdlem53  42464  fourierdlem57  42468  fourierdlem59  42470  fourierdlem60  42471  fourierdlem61  42472  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem66  42477  fourierdlem68  42479  fourierdlem71  42482  fourierdlem72  42483  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem78  42489  fourierdlem79  42490  fourierdlem80  42491  fourierdlem81  42492  fourierdlem82  42493  fourierdlem83  42494  fourierdlem84  42495  fourierdlem87  42498  fourierdlem88  42499  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem92  42503  fourierdlem93  42504  fourierdlem94  42505  fourierdlem95  42506  fourierdlem97  42508  fourierdlem101  42512  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  fourierdlem112  42523  fourierdlem113  42524  sqwvfoura  42533  sqwvfourb  42534  fouriersw  42536  qndenserrnbllem  42599  ioorrnopnlem  42609  ioorrnopnxrlem  42611  sge0xaddlem1  42735  sge0xaddlem2  42736  omeiunltfirp  42821  carageniuncllem2  42824  hoidmv1lelem1  42893  hoidmv1lelem2  42894  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  hoidmvlelem4  42900  hoiqssbllem1  42924  hoiqssbllem2  42925  hoiqssbllem3  42926  hspmbllem2  42929  hspmbllem3  42930  ovolval5lem1  42954  iinhoiicclem  42975  iinhoiicc  42976  iunhoiioolem  42977  iccvonmbllem  42980  vonioolem1  42982  vonioolem2  42983  vonicclem1  42985  vonicclem2  42986  preimaleiinlt  43019  salpreimaltle  43023  smfaddlem1  43059  smfadd  43061  smflimlem3  43069  smflimlem4  43070  smflimlem6  43072  smfmullem1  43086  smfmullem2  43087  smfmullem3  43088  zm1nn  43522  requad01  43806  requad1  43807  requad2  43808  perfectALTVlem2  43907  nnsum4primesevenALTV  43986  bgoldbtbndlem2  43991  dignn0flhalflem1  44695  affinecomb1  44709  resum2sqcl  44713  2sphere  44756  line2  44759  itsclc0lem1  44763  itscnhlc0yqe  44766  itsclquadb  44783  2itscp  44788  itscnhlinecirc02plem1  44789  itscnhlinecirc02plem3  44791  itscnhlinecirc02p  44792  inlinecirc02plem  44793  amgmwlem  44923