Theorem readdcld 10406

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 6922  ℝcr 10271   + caddc 10275

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

This theorem depends on definitions:  df-bi 199  df-an 387

This theorem is referenced by:  ltadd2  10480  readdcan  10550  addid1  10556  leadd1  10843  le2add  10857  lesub2  10870  lesub3d  10993  supaddc  11344  supadd  11345  cju  11370  nnne0  11410  div4p1lem1div2  11637  difgtsumgt  11697  eluzmn  11999  rpnnen1lem5  12128  addlelt  12253  xralrple  12348  xov1plusxeqvd  12635  zltaddlt1le  12641  elincfzoext  12845  fladdz  12945  2tnp1ge0ge0  12949  flhalf  12950  fldiv  12978  modaddmodup  13052  modaddmodlo  13053  addmodlteq  13064  discr1  13319  discr  13320  ccatalpha  13683  2cshw  13964  remim  14264  remullem  14275  sqrlem7  14396  absrele  14455  abstri  14477  abs3lem  14485  amgm2  14516  mulcn2  14734  o1add  14752  o1sub  14754  lo1add  14765  caucvgrlem  14811  iseraltlem2  14821  iseraltlem3  14822  fsumabs  14937  o1fsum  14949  climcndslem2  14986  tanhlt1  15292  eirrlem  15336  ruclem1  15364  ruclem2  15365  ruclem3  15366  ltoddhalfle  15489  bitscmp  15566  sadcaddlem  15585  sadasslem  15598  smuval2  15610  iserodd  15944  prmreclem4  16027  4sqlem5  16050  4sqlem6  16051  4sqlem12  16064  4sqlem15  16067  4sqlem16  16068  prmgaplem7  16165  prmgaplem8  16166  2expltfac  16198  cshwshashlem2  16202  chfacfscmul0  21070  chfacfscmulgsum  21072  chfacfpmmul0  21074  chfacfpmmulgsum  21076  prdsxmetlem  22581  xblss2ps  22614  metustexhalf  22769  nrmmetd  22787  ngptgp  22848  nlmvscnlem2  22897  nlmvscnlem1  22898  nmotri  22951  nghmplusg  22952  blcvx  23009  iccntr  23032  icccmplem2  23034  reconnlem2  23038  metdcnlem  23047  metnrmlem3  23072  cnllycmp  23163  lebnumii  23173  tcphcphlem1  23441  ipcnlem2  23450  ipcnlem1  23451  csbren  23605  trirn  23606  minveclem2  23632  minveclem3b  23634  minveclem4  23638  ivthlem2  23656  ovolgelb  23684  ovollb2lem  23692  ovolunlem1a  23700  ovolunlem1  23701  ovolfiniun  23705  ovoliunlem1  23706  ovoliunlem2  23707  ovolshftlem1  23713  ovolscalem1  23717  ovolicopnf  23728  ismbl2  23731  nulmbl2  23740  unmbl  23741  voliunlem2  23755  ioombl1lem2  23763  ioombl1lem4  23765  ioombl1  23766  ioorcl2  23776  uniioombllem1  23785  uniioombllem3  23789  uniioombllem4  23790  uniioombllem5  23791  uniioombl  23793  opnmbllem  23805  volcn  23810  itg1addlem4  23903  mbfi1fseqlem4  23922  mbfi1fseqlem6  23924  itg2splitlem  23952  itg2split  23953  itg2monolem3  23956  itg2addlem  23962  ibladdlem  24023  itgaddlem1  24026  itgaddlem2  24027  iblabslem  24031  iblabs  24032  dvferm1lem  24184  dvferm2lem  24186  dvlip2  24195  lhop1lem  24213  lhop1  24214  lhop  24216  dvcnvrelem1  24217  dvcnvrelem2  24218  dvcnvre  24219  dvcvx  24220  dvfsumlem3  24228  dvfsumlem4  24229  dvfsum2  24234  ftc1lem4  24239  coemullem  24443  ulmbdd  24589  ulmcn  24590  ulmdvlem1  24591  radcnvle  24611  pserdvlem1  24618  pserdv  24620  abelthlem7  24629  pilem2  24643  pilem3  24644  pilem3OLD  24645  cosordlem  24715  abslogle  24801  logccv  24846  cxpaddle  24933  ang180lem2  24988  heron  25016  atanlogaddlem  25091  atans2  25109  cxp2limlem  25154  scvxcvx  25164  jensenlem2  25166  amgmlem  25168  logdiflbnd  25173  harmonicbnd4  25189  fsumharmonic  25190  lgamgulmlem3  25209  lgamgulmlem4  25210  lgamgulmlem5  25211  lgamgulmlem6  25212  lgambdd  25215  lgamucov  25216  regamcl  25239  ftalem5  25255  efnnfsumcl  25281  efchtdvds  25337  chtublem  25388  chtub  25389  logfaclbnd  25399  perfectlem2  25407  bcmono  25454  bposlem7  25467  bposlem9  25469  lgsdirprm  25508  gausslemma2dlem1a  25542  2sqlem8  25603  chpchtlim  25620  vmadivsumb  25624  rplogsumlem1  25625  dchrisumlem2  25631  dchrvmasumlem2  25639  dchrvmasumiflem1  25642  dchrisum0re  25654  dchrisum0lem1b  25656  mulog2sumlem1  25675  mulog2sumlem2  25676  logsqvma2  25684  log2sumbnd  25685  selberglem2  25687  selbergb  25690  selberg2b  25693  chpdifbndlem1  25694  chpdifbndlem2  25695  selberg3lem2  25699  selberg3  25700  selberg4lem1  25701  selberg4  25702  pntrsumbnd2  25708  selberg3r  25710  selberg34r  25712  pntsf  25714  pntrlog2bndlem1  25718  pntrlog2bndlem2  25719  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  pntrlog2bndlem6  25724  pntrlog2bnd  25725  pntpbnd1a  25726  pntpbnd2  25728  pntibndlem2a  25731  pntibndlem2  25732  pntibndlem3  25733  pntlemg  25739  pntlemr  25743  pntlemk  25747  pntlemo  25748  pntlem3  25750  abvcxp  25756  padicabv  25771  ostth2lem2  25775  ostth3  25779  brbtwn2  26254  axsegconlem8  26273  axsegconlem10  26275  axpaschlem  26289  axpasch  26290  axeuclidlem  26311  axcontlem2  26314  crctcshwlkn0lem3  27161  crctcshwlkn0lem5  27163  vacn  28121  smcnlem  28124  ubthlem2  28299  minvecolem2  28303  minvecolem3  28304  minvecolem4  28308  minvecolem5  28309  nmoptrii  29525  hstle  29661  staddi  29677  stadd3i  29679  lt2addrd  30081  nndiffz1  30112  bhmafibid1  30206  fsumrp0cl  30257  pmtrto1cl  30447  fzto1st  30451  psgnfzto1st  30453  1smat1  30468  sqsscirc1  30552  cnre2csqlem  30554  tpr2rico  30556  nexple  30669  dya2iocress  30934  dya2iocbrsiga  30935  dya2icobrsiga  30936  dya2icoseg  30937  dya2iocucvr  30944  sxbrsigalem2  30946  omssubaddlem  30959  fibp1  31062  ballotlemfc0  31153  ballotlemfcc  31154  ballotlemsgt1  31171  ballotlemsel1i  31173  plymulx0  31224  breprexplemc  31312  breprexp  31313  logdivsqrle  31330  resconn  31827  faclim  32226  dnizphlfeqhlf  33049  dnibndlem4  33054  dnibndlem6  33056  dnibndlem8  33058  dnibndlem9  33059  dnibndlem10  33060  dnibndlem11  33061  dnibndlem13  33063  dnibnd  33064  knoppcnlem4  33069  unblimceq0lem  33079  unblimceq0  33080  unbdqndv2lem1  33082  poimirlem29  34066  heicant  34072  opnmbllem0  34073  mblfinlem3  34076  mblfinlem4  34077  ismblfin  34078  mbfposadd  34084  itg2addnclem  34088  itg2addnclem3  34090  itg2addnc  34091  itg2gt0cn  34092  ibladdnclem  34093  itgaddnclem1  34095  itgaddnclem2  34096  iblabsnclem  34100  iblabsnc  34101  iblmulc2nc  34102  ftc1cnnclem  34110  ftc1anclem4  34115  ftc1anclem7  34118  ftc1anclem8  34119  ftc1anc  34120  areacirclem5  34131  mettrifi  34179  isbnd3  34209  ssbnd  34213  cntotbnd  34221  heibor1lem  34234  bfplem2  34248  rrnequiv  34260  iccbnd  34265  readdid2addid1d  38184  resubeulem1  38186  resubeulem2  38187  resubeu  38188  readdsub  38195  reladdrsub  38196  resubidaddid1lem  38202  dffltz  38217  pellexlem2  38358  pell1qrge1  38398  pell14qrgapw  38404  pellqrexplicit  38405  pellqrex  38407  pellfundge  38410  pellfundgt1  38411  rmspecfund  38437  rmxycomplete  38445  ltrmynn0  38478  jm2.24nn  38489  jm2.24  38493  fzmaxdif  38511  jm2.26lem3  38531  jm3.1lem2  38548  areaquad  38764  imo72b2lem0  39425  hashnzfzclim  39481  binomcxplemnotnn0  39515  zltlesub  40411  lt3addmuld  40428  absnpncan2d  40429  fperiodmullem  40430  lt4addmuld  40433  absnpncan3d  40434  leadd12dd  40444  supxrgelem  40465  supxrge  40466  ltadd12dd  40471  xralrple2  40482  infxr  40495  infleinflem2  40499  xralrple4  40501  xralrple3  40502  xrralrecnnle  40514  eliooshift  40645  iccshift  40657  iooshift  40661  iooiinicc  40681  iooiinioc  40695  fsumnncl  40715  climinf  40750  climsuselem1  40751  sumnnodd  40774  lptre2pt  40784  addlimc  40792  0ellimcdiv  40793  limclner  40795  climleltrp  40820  liminfltlem  40948  fperdvper  41065  dvdivbd  41070  dvbdfbdioolem2  41076  dvbdfbdioo  41077  ioodvbdlimc1lem1  41078  ioodvbdlimc1lem2  41079  ioodvbdlimc2lem  41081  dvxpaek  41087  dvnmul  41090  iblsplit  41113  iblspltprt  41120  itgspltprt  41126  itgiccshift  41127  itgperiod  41128  itgsbtaddcnst  41129  stoweidlem1  41149  stoweidlem11  41159  stoweidlem13  41161  stoweidlem14  41162  stoweidlem20  41168  stoweidlem21  41169  stoweidlem26  41174  stoweidlem44  41192  stoweidlem60  41208  wallispilem3  41215  wallispilem4  41216  wallispilem5  41217  wallispi  41218  wallispi2lem1  41219  wallispi2lem2  41220  stirlinglem1  41222  stirlinglem3  41224  stirlinglem5  41226  stirlinglem6  41227  stirlinglem7  41228  stirlinglem10  41231  stirlinglem11  41232  stirlinglem12  41233  dirker2re  41240  dirkerval2  41242  dirkerre  41243  dirkerper  41244  dirkertrigeqlem1  41246  dirkertrigeqlem2  41247  dirkeritg  41250  dirkercncflem1  41251  dirkercncflem2  41252  dirkercncflem4  41254  fourierdlem4  41259  fourierdlem5  41260  fourierdlem6  41261  fourierdlem7  41262  fourierdlem9  41264  fourierdlem10  41265  fourierdlem18  41273  fourierdlem19  41274  fourierdlem20  41275  fourierdlem26  41281  fourierdlem28  41283  fourierdlem30  41285  fourierdlem35  41290  fourierdlem40  41295  fourierdlem41  41296  fourierdlem42  41297  fourierdlem47  41301  fourierdlem48  41302  fourierdlem49  41303  fourierdlem50  41304  fourierdlem51  41305  fourierdlem53  41307  fourierdlem57  41311  fourierdlem59  41313  fourierdlem60  41314  fourierdlem61  41315  fourierdlem63  41317  fourierdlem64  41318  fourierdlem65  41319  fourierdlem66  41320  fourierdlem68  41322  fourierdlem71  41325  fourierdlem72  41326  fourierdlem74  41328  fourierdlem75  41329  fourierdlem76  41330  fourierdlem78  41332  fourierdlem79  41333  fourierdlem80  41334  fourierdlem81  41335  fourierdlem82  41336  fourierdlem83  41337  fourierdlem84  41338  fourierdlem87  41341  fourierdlem88  41342  fourierdlem89  41343  fourierdlem90  41344  fourierdlem91  41345  fourierdlem92  41346  fourierdlem93  41347  fourierdlem94  41348  fourierdlem95  41349  fourierdlem97  41351  fourierdlem101  41355  fourierdlem103  41357  fourierdlem104  41358  fourierdlem111  41365  fourierdlem112  41366  fourierdlem113  41367  sqwvfoura  41376  sqwvfourb  41377  fouriersw  41379  qndenserrnbllem  41442  ioorrnopnlem  41452  ioorrnopnxrlem  41454  sge0xaddlem1  41578  sge0xaddlem2  41579  omeiunltfirp  41664  carageniuncllem2  41667  hoidmv1lelem1  41736  hoidmv1lelem2  41737  hoidmvlelem1  41740  hoidmvlelem2  41741  hoidmvlelem3  41742  hoidmvlelem4  41743  hoiqssbllem1  41767  hoiqssbllem2  41768  hoiqssbllem3  41769  hspmbllem2  41772  hspmbllem3  41773  ovolval5lem1  41797  iinhoiicclem  41818  iinhoiicc  41819  iunhoiioolem  41820  iccvonmbllem  41823  vonioolem1  41825  vonioolem2  41826  vonicclem1  41828  vonicclem2  41829  preimaleiinlt  41862  salpreimaltle  41866  smfaddlem1  41902  smfadd  41904  smflimlem3  41912  smflimlem4  41913  smflimlem6  41915  smfmullem1  41929  smfmullem2  41930  smfmullem3  41931  zm1nn  42348  requad01  42563  requad1  42564  requad2  42565  perfectALTVlem2  42660  nnsum4primesevenALTV  42718  bgoldbtbndlem2  42723  dignn0flhalflem1  43428  affinecomb1  43442  resum2sqcl  43446  2sphere  43489  line2  43492  itsclc0lem1  43496  itscnhlc0yqe  43499  itsclquadb  43516  2itscp  43521  itscnhlinecirc02plem1  43522  itscnhlinecirc02plem3  43524  itscnhlinecirc02p  43525  inlinecirc02plem  43526  amgmwlem  43658