Theorem readdcld 10988

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7268  ℝcr 10854   + caddc 10858

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

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

This theorem is referenced by:  ltadd2  11062  readdcan  11132  addid1  11138  leadd1  11426  le2add  11440  lesub2  11453  lesub3d  11576  supaddc  11925  supadd  11926  cju  11952  nnne0  11990  div4p1lem1div2  12211  difgtsumgt  12269  eluzmn  12571  rpnnen1lem5  12703  addlelt  12826  xralrple  12921  xov1plusxeqvd  13212  zltaddlt1le  13219  elincfzoext  13426  fladdz  13526  2tnp1ge0ge0  13530  flhalf  13531  fldiv  13561  modaddmodup  13635  modaddmodlo  13636  addmodlteq  13647  discr1  13935  discr  13936  ccatalpha  14279  2cshw  14507  remim  14809  remullem  14820  sqrlem7  14941  absrele  15001  abstri  15023  abs3lem  15031  amgm2  15062  bhmafibid1  15158  mulcn2  15286  o1add  15304  o1sub  15306  lo1add  15317  caucvgrlem  15365  iseraltlem2  15375  iseraltlem3  15376  fsumabs  15494  o1fsum  15506  climcndslem2  15543  tanhlt1  15850  eirrlem  15894  ruclem1  15921  ruclem2  15922  ruclem3  15923  ltoddhalfle  16051  bitscmp  16126  sadcaddlem  16145  sadasslem  16158  smuval2  16170  iserodd  16517  prmreclem4  16601  4sqlem5  16624  4sqlem6  16625  4sqlem12  16638  4sqlem15  16641  4sqlem16  16642  prmgaplem7  16739  prmgaplem8  16740  2expltfac  16775  cshwshashlem2  16779  chfacfscmul0  21988  chfacfscmulgsum  21990  chfacfpmmul0  21992  chfacfpmmulgsum  21994  prdsxmetlem  23502  xblss2ps  23535  metustexhalf  23693  nrmmetd  23711  ngptgp  23773  nlmvscnlem2  23830  nlmvscnlem1  23831  nmotri  23884  nghmplusg  23885  blcvx  23942  iccntr  23965  icccmplem2  23967  reconnlem2  23971  metdcnlem  23980  metnrmlem3  24005  cnllycmp  24100  lebnumii  24110  tcphcphlem1  24380  ipcnlem2  24389  ipcnlem1  24390  csbren  24544  trirn  24545  minveclem2  24571  minveclem3b  24573  minveclem4  24577  ivthlem2  24597  ovolgelb  24625  ovollb2lem  24633  ovolunlem1a  24641  ovolunlem1  24642  ovolfiniun  24646  ovoliunlem1  24647  ovoliunlem2  24648  ovolshftlem1  24654  ovolscalem1  24658  ovolicopnf  24669  ismbl2  24672  nulmbl2  24681  unmbl  24682  voliunlem2  24696  ioombl1lem2  24704  ioombl1lem4  24706  ioombl1  24707  ioorcl2  24717  uniioombllem1  24726  uniioombllem3  24730  uniioombllem4  24731  uniioombllem5  24732  uniioombl  24734  opnmbllem  24746  volcn  24751  itg1addlem4  24844  itg1addlem4OLD  24845  mbfi1fseqlem4  24864  mbfi1fseqlem6  24866  itg2splitlem  24894  itg2split  24895  itg2monolem3  24898  itg2addlem  24904  ibladdlem  24965  itgaddlem1  24968  itgaddlem2  24969  iblabslem  24973  iblabs  24974  dvferm1lem  25129  dvferm2lem  25131  dvlip2  25140  lhop1lem  25158  lhop1  25159  lhop  25161  dvcnvrelem1  25162  dvcnvrelem2  25163  dvcnvre  25164  dvcvx  25165  dvfsumlem3  25173  dvfsumlem4  25174  dvfsum2  25179  ftc1lem4  25184  coemullem  25392  ulmbdd  25538  ulmcn  25539  ulmdvlem1  25540  radcnvle  25560  pserdvlem1  25567  pserdv  25569  abelthlem7  25578  pilem2  25592  pilem3  25593  cosordlem  25667  abslogle  25754  logccv  25799  cxpaddle  25886  ang180lem2  25941  heron  25969  atanlogaddlem  26044  atans2  26062  cxp2limlem  26106  scvxcvx  26116  jensenlem2  26118  amgmlem  26120  logdiflbnd  26125  harmonicbnd4  26141  fsumharmonic  26142  lgamgulmlem3  26161  lgamgulmlem4  26162  lgamgulmlem5  26163  lgamgulmlem6  26164  lgambdd  26167  lgamucov  26168  regamcl  26191  ftalem5  26207  efnnfsumcl  26233  efchtdvds  26289  chtublem  26340  chtub  26341  logfaclbnd  26351  perfectlem2  26359  bposlem7  26419  bposlem9  26421  lgsdirprm  26460  gausslemma2dlem1a  26494  2sqlem8  26555  chpchtlim  26608  vmadivsumb  26612  rplogsumlem1  26613  dchrisumlem2  26619  dchrvmasumlem2  26627  dchrvmasumiflem1  26630  dchrisum0re  26642  dchrisum0lem1b  26644  mulog2sumlem1  26663  mulog2sumlem2  26664  logsqvma2  26672  log2sumbnd  26673  selberglem2  26675  selbergb  26678  selberg2b  26681  chpdifbndlem1  26682  chpdifbndlem2  26683  selberg3lem2  26687  selberg3  26688  selberg4lem1  26689  selberg4  26690  pntrsumbnd2  26696  selberg3r  26698  selberg34r  26700  pntsf  26702  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntrlog2bnd  26713  pntpbnd1a  26714  pntpbnd2  26716  pntibndlem2a  26719  pntibndlem2  26720  pntibndlem3  26721  pntlemg  26727  pntlemr  26731  pntlemk  26735  pntlemo  26736  pntlem3  26738  abvcxp  26744  padicabv  26759  ostth2lem2  26763  ostth3  26767  brbtwn2  27254  axsegconlem8  27273  axsegconlem10  27275  axpaschlem  27289  axpasch  27290  axeuclidlem  27311  axcontlem2  27314  crctcshwlkn0lem3  28156  crctcshwlkn0lem5  28158  vacn  29035  smcnlem  29038  ubthlem2  29212  minvecolem2  29216  minvecolem3  29217  minvecolem4  29221  minvecolem5  29222  nmoptrii  30435  hstle  30571  staddi  30587  stadd3i  30589  lt2addrd  31053  nndiffz1  31086  wrdt2ind  31204  cshwrnid  31212  fsumrp0cl  31283  pmtrto1cl  31345  fzto1st  31349  psgnfzto1st  31351  1smat1  31733  sqsscirc1  31837  cnre2csqlem  31839  tpr2rico  31841  nexple  31956  dya2iocress  32220  dya2iocbrsiga  32221  dya2icobrsiga  32222  dya2icoseg  32223  dya2iocucvr  32230  sxbrsigalem2  32232  omssubaddlem  32245  fibp1  32347  ballotlemfc0  32438  ballotlemfcc  32439  ballotlemsgt1  32456  ballotlemsel1i  32458  plymulx0  32505  breprexplemc  32591  breprexp  32592  logdivsqrle  32609  resconn  33187  faclim  33691  dnizphlfeqhlf  34635  dnibndlem4  34640  dnibndlem6  34642  dnibndlem8  34644  dnibndlem9  34645  dnibndlem10  34646  dnibndlem11  34647  dnibndlem13  34649  dnibnd  34650  knoppcnlem4  34655  unblimceq0lem  34665  unblimceq0  34666  unbdqndv2lem1  34668  poimirlem29  35785  heicant  35791  opnmbllem0  35792  mblfinlem3  35795  mblfinlem4  35796  ismblfin  35797  mbfposadd  35803  itg2addnclem  35807  itg2addnclem3  35809  itg2addnc  35810  itg2gt0cn  35811  ibladdnclem  35812  itgaddnclem1  35814  itgaddnclem2  35815  iblabsnclem  35819  iblabsnc  35820  iblmulc2nc  35821  ftc1cnnclem  35827  ftc1anclem4  35832  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837  areacirclem5  35848  mettrifi  35894  isbnd3  35921  ssbnd  35925  cntotbnd  35933  heibor1lem  35946  bfplem2  35960  rrnequiv  35972  iccbnd  35977  lcmineqlem18  40034  lcmineqlem20  40036  aks4d1p1p3  40057  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  2np3bcnp1  40080  2ap1caineq  40081  sticksstones6  40087  sticksstones7  40088  sticksstones10  40091  sticksstones12a  40093  sticksstones12  40094  sticksstones22  40104  metakunt29  40133  2xp3dxp2ge1d  40142  factwoffsmonot  40143  readdid1addid2d  40274  resubeulem1  40338  resubeulem2  40339  resubeu  40340  readdsub  40347  reladdrsub  40348  resubidaddid1lem  40357  renegid2  40376  sn-it0e0  40377  sn-0tie0  40401  cnreeu  40418  dffltz  40451  fltnltalem  40479  fltnlta  40480  3cubeslem1  40486  pellexlem2  40632  pell1qrge1  40672  pell14qrgapw  40678  pellqrexplicit  40679  pellqrex  40681  pellfundge  40684  pellfundgt1  40685  rmspecfund  40711  rmxycomplete  40719  ltrmynn0  40750  jm2.24nn  40761  jm2.24  40765  fzmaxdif  40783  jm2.26lem3  40803  jm3.1lem2  40820  areaquad  41027  sqrtcvallem4  41200  sqrtcvallem5  41201  sqrtcval  41202  imo72b2lem0  41729  hashnzfzclim  41893  binomcxplemnotnn0  41927  zltlesub  42777  lt3addmuld  42794  absnpncan2d  42795  fperiodmullem  42796  lt4addmuld  42799  absnpncan3d  42800  leadd12dd  42809  supxrgelem  42830  supxrge  42831  ltadd12dd  42836  xralrple2  42847  infxr  42860  infleinflem2  42864  xralrple4  42866  xralrple3  42867  xrralrecnnle  42876  eliooshift  42998  iccshift  43010  iooshift  43014  iooiinicc  43034  iooiinioc  43048  fsumnncl  43067  climinf  43101  climsuselem1  43102  sumnnodd  43125  lptre2pt  43135  addlimc  43143  0ellimcdiv  43144  limclner  43146  climleltrp  43171  liminfltlem  43299  fperdvper  43414  dvdivbd  43418  dvbdfbdioolem2  43424  dvbdfbdioo  43425  ioodvbdlimc1lem1  43426  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvxpaek  43435  dvnmul  43438  iblsplit  43461  iblspltprt  43468  itgspltprt  43474  itgiccshift  43475  itgperiod  43476  itgsbtaddcnst  43477  stoweidlem1  43496  stoweidlem11  43506  stoweidlem13  43508  stoweidlem14  43509  stoweidlem20  43515  stoweidlem21  43516  stoweidlem26  43521  stoweidlem44  43539  stoweidlem60  43555  wallispilem3  43562  wallispilem4  43563  wallispilem5  43564  wallispi  43565  wallispi2lem1  43566  wallispi2lem2  43567  stirlinglem1  43569  stirlinglem3  43571  stirlinglem5  43573  stirlinglem6  43574  stirlinglem7  43575  stirlinglem10  43578  stirlinglem11  43579  stirlinglem12  43580  dirker2re  43587  dirkerval2  43589  dirkerre  43590  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem2  43594  dirkeritg  43597  dirkercncflem1  43598  dirkercncflem2  43599  dirkercncflem4  43601  fourierdlem4  43606  fourierdlem5  43607  fourierdlem6  43608  fourierdlem7  43609  fourierdlem9  43611  fourierdlem10  43612  fourierdlem18  43620  fourierdlem19  43621  fourierdlem20  43622  fourierdlem26  43628  fourierdlem28  43630  fourierdlem30  43632  fourierdlem35  43637  fourierdlem40  43642  fourierdlem41  43643  fourierdlem42  43644  fourierdlem47  43648  fourierdlem48  43649  fourierdlem49  43650  fourierdlem50  43651  fourierdlem51  43652  fourierdlem53  43654  fourierdlem57  43658  fourierdlem59  43660  fourierdlem60  43661  fourierdlem61  43662  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  fourierdlem66  43667  fourierdlem68  43669  fourierdlem71  43672  fourierdlem72  43673  fourierdlem74  43675  fourierdlem75  43676  fourierdlem76  43677  fourierdlem78  43679  fourierdlem79  43680  fourierdlem80  43681  fourierdlem81  43682  fourierdlem82  43683  fourierdlem83  43684  fourierdlem84  43685  fourierdlem87  43688  fourierdlem88  43689  fourierdlem89  43690  fourierdlem90  43691  fourierdlem91  43692  fourierdlem92  43693  fourierdlem93  43694  fourierdlem94  43695  fourierdlem95  43696  fourierdlem97  43698  fourierdlem101  43702  fourierdlem103  43704  fourierdlem104  43705  fourierdlem111  43712  fourierdlem112  43713  fourierdlem113  43714  sqwvfoura  43723  sqwvfourb  43724  fouriersw  43726  qndenserrnbllem  43789  ioorrnopnlem  43799  ioorrnopnxrlem  43801  sge0xaddlem1  43925  sge0xaddlem2  43926  omeiunltfirp  44011  carageniuncllem2  44014  hoidmv1lelem1  44083  hoidmv1lelem2  44084  hoidmvlelem1  44087  hoidmvlelem2  44088  hoidmvlelem3  44089  hoidmvlelem4  44090  hoiqssbllem1  44114  hoiqssbllem2  44115  hoiqssbllem3  44116  hspmbllem2  44119  hspmbllem3  44120  ovolval5lem1  44144  iinhoiicclem  44165  iinhoiicc  44166  iunhoiioolem  44167  iccvonmbllem  44170  vonioolem1  44172  vonioolem2  44173  vonicclem1  44175  vonicclem2  44176  preimaleiinlt  44209  salpreimaltle  44213  smfaddlem1  44249  smfadd  44251  smflimlem3  44259  smflimlem4  44260  smflimlem6  44262  smfmullem1  44276  smfmullem2  44277  smfmullem3  44278  zm1nn  44746  requad01  45025  requad1  45026  requad2  45027  perfectALTVlem2  45126  nnsum4primesevenALTV  45205  bgoldbtbndlem2  45210  dignn0flhalflem1  45913  affinecomb1  46000  resum2sqcl  46004  2sphere  46047  line2  46050  itsclc0lem1  46054  itscnhlc0yqe  46057  itsclquadb  46074  2itscp  46079  itscnhlinecirc02plem1  46080  itscnhlinecirc02plem3  46082  itscnhlinecirc02p  46083  inlinecirc02plem  46084  amgmwlem  46458