Theorem readdcld 11161

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025   + caddc 11029

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

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

This theorem is referenced by:  ltadd2  11237  readdcan  11307  addrid  11313  leadd1  11605  le2add  11619  lesub2  11632  lesub3d  11755  le2addd  11756  supaddc  12109  supadd  12110  cju  12141  nnne0  12179  div4p1lem1div2  12396  difgtsumgt  12454  eluzmn  12758  rpnnen1lem5  12894  addlelt  13021  xralrple  13120  xov1plusxeqvd  13414  zltaddlt1le  13421  elincfzoext  13639  fladdz  13745  2tnp1ge0ge0  13749  flhalf  13750  fldiv  13780  modaddb  13829  modaddmodup  13857  modaddmodlo  13858  addmodlteq  13869  discr1  14162  discr  14163  ccatalpha  14517  2cshw  14736  remim  15040  remullem  15051  01sqrexlem7  15171  absrele  15231  abstri  15254  abs3lem  15262  amgm2  15293  bhmafibid1  15391  mulcn2  15519  o1add  15537  o1sub  15539  lo1add  15550  caucvgrlem  15596  iseraltlem2  15606  iseraltlem3  15607  fsumabs  15724  o1fsum  15736  climcndslem2  15773  tanhlt1  16085  eirrlem  16129  ruclem1  16156  ruclem2  16157  ruclem3  16158  ltoddhalfle  16288  bitscmp  16365  sadcaddlem  16384  sadasslem  16397  smuval2  16409  iserodd  16763  prmreclem4  16847  4sqlem5  16870  4sqlem6  16871  4sqlem12  16884  4sqlem15  16887  4sqlem16  16888  prmgaplem7  16985  prmgaplem8  16986  2expltfac  17020  cshwshashlem2  17024  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  prdsxmetlem  24312  xblss2ps  24345  metustexhalf  24500  nrmmetd  24518  ngptgp  24580  nlmvscnlem2  24629  nlmvscnlem1  24630  nmotri  24683  nghmplusg  24684  blcvx  24742  iccntr  24766  icccmplem2  24768  reconnlem2  24772  metdcnlem  24781  metnrmlem3  24806  cnllycmp  24911  lebnumii  24921  tcphcphlem1  25191  ipcnlem2  25200  ipcnlem1  25201  csbren  25355  trirn  25356  minveclem2  25382  minveclem3b  25384  minveclem4  25388  ivthlem2  25409  ovolgelb  25437  ovollb2lem  25445  ovolunlem1a  25453  ovolunlem1  25454  ovolfiniun  25458  ovoliunlem1  25459  ovoliunlem2  25460  ovolshftlem1  25466  ovolscalem1  25470  ovolicopnf  25481  ismbl2  25484  nulmbl2  25493  unmbl  25494  voliunlem2  25508  ioombl1lem2  25516  ioombl1lem4  25518  ioombl1  25519  ioorcl2  25529  uniioombllem1  25538  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombl  25546  opnmbllem  25558  volcn  25563  itg1addlem4  25656  mbfi1fseqlem4  25675  mbfi1fseqlem6  25677  itg2splitlem  25705  itg2split  25706  itg2monolem3  25709  itg2addlem  25715  ibladdlem  25777  itgaddlem1  25780  itgaddlem2  25781  iblabslem  25785  iblabs  25786  dvferm1lem  25944  dvferm2lem  25946  dvlip2  25956  lhop1lem  25974  lhop1  25975  lhop  25977  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcnvre  25980  dvcvx  25981  dvfsumlem3  25991  dvfsumlem4  25992  dvfsum2  25997  ftc1lem4  26002  coemullem  26211  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  radcnvle  26385  pserdvlem1  26393  pserdv  26395  abelthlem7  26404  pilem2  26418  pilem3  26419  cosordlem  26495  abslogle  26583  logccv  26628  cxpaddle  26718  ang180lem2  26776  heron  26804  atanlogaddlem  26879  atans2  26897  cxp2limlem  26942  scvxcvx  26952  jensenlem2  26954  amgmlem  26956  logdiflbnd  26961  harmonicbnd4  26977  fsumharmonic  26978  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulmlem6  27000  lgambdd  27003  lgamucov  27004  regamcl  27027  ftalem5  27043  efnnfsumcl  27069  efchtdvds  27125  chtublem  27178  chtub  27179  logfaclbnd  27189  perfectlem2  27197  bposlem7  27257  bposlem9  27259  lgsdirprm  27298  gausslemma2dlem1a  27332  2sqlem8  27393  chpchtlim  27446  vmadivsumb  27450  rplogsumlem1  27451  dchrisumlem2  27457  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0re  27480  dchrisum0lem1b  27482  mulog2sumlem1  27501  mulog2sumlem2  27502  logsqvma2  27510  log2sumbnd  27511  selberglem2  27513  selbergb  27516  selberg2b  27519  chpdifbndlem1  27520  chpdifbndlem2  27521  selberg3lem2  27525  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrsumbnd2  27534  selberg3r  27536  selberg34r  27538  pntsf  27540  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem2a  27557  pntibndlem2  27558  pntibndlem3  27559  pntlemg  27565  pntlemr  27569  pntlemk  27573  pntlemo  27574  pntlem3  27576  abvcxp  27582  padicabv  27597  ostth2lem2  27601  ostth3  27605  brbtwn2  28978  axsegconlem8  28997  axsegconlem10  28999  axpaschlem  29013  axpasch  29014  axeuclidlem  29035  axcontlem2  29038  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  vacn  30769  smcnlem  30772  ubthlem2  30946  minvecolem2  30950  minvecolem3  30951  minvecolem4  30955  minvecolem5  30956  nmoptrii  32169  hstle  32305  staddi  32321  stadd3i  32323  lt2addrd  32830  nndiffz1  32866  nexple  32925  wrdt2ind  33035  cshwrnid  33043  fsumrp0cl  33103  pmtrto1cl  33181  fzto1st  33185  psgnfzto1st  33187  constrresqrtcl  33934  cos9thpiminplylem1  33939  1smat1  33961  sqsscirc1  34065  cnre2csqlem  34067  tpr2rico  34069  dya2iocress  34431  dya2iocbrsiga  34432  dya2icobrsiga  34433  dya2icoseg  34434  dya2iocucvr  34441  sxbrsigalem2  34443  omssubaddlem  34456  fibp1  34558  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemsgt1  34668  ballotlemsel1i  34670  plymulx0  34704  breprexplemc  34789  breprexp  34790  logdivsqrle  34807  resconn  35440  faclim  35940  dnizphlfeqhlf  36676  dnibndlem4  36681  dnibndlem6  36683  dnibndlem8  36685  dnibndlem9  36686  dnibndlem10  36687  dnibndlem11  36688  dnibndlem13  36690  dnibnd  36691  knoppcnlem4  36696  unblimceq0lem  36706  unblimceq0  36707  unbdqndv2lem1  36709  poimirlem29  37846  heicant  37852  opnmbllem0  37853  mblfinlem3  37856  mblfinlem4  37857  ismblfin  37858  mbfposadd  37864  itg2addnclem  37868  itg2addnclem3  37870  itg2addnc  37871  itg2gt0cn  37872  ibladdnclem  37873  itgaddnclem1  37875  itgaddnclem2  37876  iblabsnclem  37880  iblabsnc  37881  iblmulc2nc  37882  ftc1cnnclem  37888  ftc1anclem4  37893  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  areacirclem5  37909  mettrifi  37954  isbnd3  37981  ssbnd  37985  cntotbnd  37993  heibor1lem  38006  bfplem2  38020  rrnequiv  38032  iccbnd  38037  lcmineqlem18  42296  lcmineqlem20  42298  aks4d1p1p3  42319  aks4d1p1p2  42320  aks4d1p1p4  42321  aks4d1p1p6  42323  aks4d1p1p7  42324  aks4d1p1p5  42325  aks4d1p1  42326  posbezout  42350  aks6d1c1  42366  aks6d1c2  42380  2np3bcnp1  42394  2ap1caineq  42395  sticksstones6  42401  sticksstones7  42402  sticksstones10  42405  sticksstones12a  42407  sticksstones12  42408  sticksstones22  42418  bcle2d  42429  aks6d1c7lem1  42430  readdridaddlidd  42509  resubeulem1  42626  resubeulem2  42627  resubeu  42628  readdsub  42635  reladdrsub  42636  resubidaddlidlem  42645  renegid2  42665  sn-it0e0  42667  sn-0tie0  42702  sn-addlt0d  42709  sn-addgt0d  42710  cnreeu  42741  dffltz  42873  fltnltalem  42901  fltnlta  42902  3cubeslem1  42922  pellexlem2  43068  pell1qrge1  43108  pell14qrgapw  43114  pellqrexplicit  43115  pellqrex  43117  pellfundge  43120  pellfundgt1  43121  rmspecfund  43147  rmxycomplete  43155  ltrmynn0  43186  jm2.24nn  43197  jm2.24  43201  fzmaxdif  43219  jm2.26lem3  43239  jm3.1lem2  43256  areaquad  43454  sqrtcvallem4  43876  sqrtcvallem5  43877  sqrtcval  43878  imo72b2lem0  44402  hashnzfzclim  44559  binomcxplemnotnn0  44593  zltlesub  45529  lt3addmuld  45545  absnpncan2d  45546  fperiodmullem  45547  lt4addmuld  45550  absnpncan3d  45551  supxrgelem  45578  supxrge  45579  ltadd12dd  45584  xralrple2  45595  infxr  45607  infleinflem2  45611  xralrple4  45613  xralrple3  45614  xrralrecnnle  45623  eliooshift  45748  iccshift  45760  iooshift  45764  iooiinicc  45784  iooiinioc  45798  fsumnncl  45814  climinf  45848  climsuselem1  45849  sumnnodd  45872  lptre2pt  45880  addlimc  45888  0ellimcdiv  45889  limclner  45891  climleltrp  45916  liminfltlem  46044  fperdvper  46159  dvdivbd  46163  dvbdfbdioolem2  46169  dvbdfbdioo  46170  ioodvbdlimc1lem1  46171  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvxpaek  46180  dvnmul  46183  iblsplit  46206  iblspltprt  46213  itgspltprt  46219  itgiccshift  46220  itgperiod  46221  itgsbtaddcnst  46222  stoweidlem1  46241  stoweidlem11  46251  stoweidlem13  46253  stoweidlem14  46254  stoweidlem20  46260  stoweidlem21  46261  stoweidlem26  46266  stoweidlem44  46284  stoweidlem60  46300  wallispilem3  46307  wallispilem4  46308  wallispilem5  46309  wallispi  46310  wallispi2lem1  46311  wallispi2lem2  46312  stirlinglem1  46314  stirlinglem3  46316  stirlinglem5  46318  stirlinglem6  46319  stirlinglem7  46320  stirlinglem10  46323  stirlinglem11  46324  stirlinglem12  46325  dirker2re  46332  dirkerval2  46334  dirkerre  46335  dirkerper  46336  dirkertrigeqlem1  46338  dirkertrigeqlem2  46339  dirkeritg  46342  dirkercncflem1  46343  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem4  46351  fourierdlem5  46352  fourierdlem6  46353  fourierdlem7  46354  fourierdlem9  46356  fourierdlem10  46357  fourierdlem18  46365  fourierdlem19  46366  fourierdlem20  46367  fourierdlem26  46373  fourierdlem28  46375  fourierdlem30  46377  fourierdlem35  46382  fourierdlem40  46387  fourierdlem41  46388  fourierdlem42  46389  fourierdlem47  46393  fourierdlem48  46394  fourierdlem49  46395  fourierdlem50  46396  fourierdlem51  46397  fourierdlem53  46399  fourierdlem57  46403  fourierdlem59  46405  fourierdlem60  46406  fourierdlem61  46407  fourierdlem63  46409  fourierdlem64  46410  fourierdlem65  46411  fourierdlem66  46412  fourierdlem68  46414  fourierdlem71  46417  fourierdlem72  46418  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem78  46424  fourierdlem79  46425  fourierdlem80  46426  fourierdlem81  46427  fourierdlem82  46428  fourierdlem83  46429  fourierdlem84  46430  fourierdlem87  46433  fourierdlem88  46434  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem92  46438  fourierdlem93  46439  fourierdlem94  46440  fourierdlem95  46441  fourierdlem97  46443  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fourierdlem112  46458  fourierdlem113  46459  sqwvfoura  46468  sqwvfourb  46469  fouriersw  46471  qndenserrnbllem  46534  ioorrnopnlem  46544  ioorrnopnxrlem  46546  sge0xaddlem1  46673  sge0xaddlem2  46674  omeiunltfirp  46759  carageniuncllem2  46762  hoidmv1lelem1  46831  hoidmv1lelem2  46832  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hoiqssbllem1  46862  hoiqssbllem2  46863  hoiqssbllem3  46864  hspmbllem2  46867  hspmbllem3  46868  ovolval5lem1  46892  iinhoiicclem  46913  iinhoiicc  46914  iunhoiioolem  46915  iccvonmbllem  46918  vonioolem1  46920  vonioolem2  46921  vonicclem1  46923  vonicclem2  46924  preimaleiinlt  46961  salpreimaltle  46966  smfaddlem1  47003  smfadd  47005  smflimlem3  47013  smflimlem4  47014  smflimlem6  47016  smfmullem1  47031  smfmullem2  47032  smfmullem3  47033  ormkglobd  47115  zm1nn  47544  requad01  47863  requad1  47864  requad2  47865  perfectALTVlem2  47964  nnsum4primesevenALTV  48043  bgoldbtbndlem2  48048  gpgvtxedg0  48305  gpgvtxedg1  48306  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx13starlem2  48314  dignn0flhalflem1  48857  affinecomb1  48944  resum2sqcl  48948  2sphere  48991  line2  48994  itsclc0lem1  48998  itscnhlc0yqe  49001  itsclquadb  49018  2itscp  49023  itscnhlinecirc02plem1  49024  itscnhlinecirc02plem3  49026  itscnhlinecirc02p  49027  inlinecirc02plem  49028  amgmwlem  50043