Theorem readdcld 11210

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074   + caddc 11078

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

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

This theorem is referenced by:  ltadd2  11285  readdcan  11355  addrid  11361  leadd1  11653  le2add  11667  lesub2  11680  lesub3d  11803  le2addd  11804  supaddc  12157  supadd  12158  cju  12189  nnne0  12227  div4p1lem1div2  12444  difgtsumgt  12502  eluzmn  12807  rpnnen1lem5  12947  addlelt  13074  xralrple  13172  xov1plusxeqvd  13466  zltaddlt1le  13473  elincfzoext  13691  fladdz  13794  2tnp1ge0ge0  13798  flhalf  13799  fldiv  13829  modaddb  13878  modaddmodup  13906  modaddmodlo  13907  addmodlteq  13918  discr1  14211  discr  14212  ccatalpha  14565  2cshw  14785  remim  15090  remullem  15101  01sqrexlem7  15221  absrele  15281  abstri  15304  abs3lem  15312  amgm2  15343  bhmafibid1  15441  mulcn2  15569  o1add  15587  o1sub  15589  lo1add  15600  caucvgrlem  15646  iseraltlem2  15656  iseraltlem3  15657  fsumabs  15774  o1fsum  15786  climcndslem2  15823  tanhlt1  16135  eirrlem  16179  ruclem1  16206  ruclem2  16207  ruclem3  16208  ltoddhalfle  16338  bitscmp  16415  sadcaddlem  16434  sadasslem  16447  smuval2  16459  iserodd  16813  prmreclem4  16897  4sqlem5  16920  4sqlem6  16921  4sqlem12  16934  4sqlem15  16937  4sqlem16  16938  prmgaplem7  17035  prmgaplem8  17036  2expltfac  17070  cshwshashlem2  17074  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulgsum  22758  prdsxmetlem  24263  xblss2ps  24296  metustexhalf  24451  nrmmetd  24469  ngptgp  24531  nlmvscnlem2  24580  nlmvscnlem1  24581  nmotri  24634  nghmplusg  24635  blcvx  24693  iccntr  24717  icccmplem2  24719  reconnlem2  24723  metdcnlem  24732  metnrmlem3  24757  cnllycmp  24862  lebnumii  24872  tcphcphlem1  25142  ipcnlem2  25151  ipcnlem1  25152  csbren  25306  trirn  25307  minveclem2  25333  minveclem3b  25335  minveclem4  25339  ivthlem2  25360  ovolgelb  25388  ovollb2lem  25396  ovolunlem1a  25404  ovolunlem1  25405  ovolfiniun  25409  ovoliunlem1  25410  ovoliunlem2  25411  ovolshftlem1  25417  ovolscalem1  25421  ovolicopnf  25432  ismbl2  25435  nulmbl2  25444  unmbl  25445  voliunlem2  25459  ioombl1lem2  25467  ioombl1lem4  25469  ioombl1  25470  ioorcl2  25480  uniioombllem1  25489  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombl  25497  opnmbllem  25509  volcn  25514  itg1addlem4  25607  mbfi1fseqlem4  25626  mbfi1fseqlem6  25628  itg2splitlem  25656  itg2split  25657  itg2monolem3  25660  itg2addlem  25666  ibladdlem  25728  itgaddlem1  25731  itgaddlem2  25732  iblabslem  25736  iblabs  25737  dvferm1lem  25895  dvferm2lem  25897  dvlip2  25907  lhop1lem  25925  lhop1  25926  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvcvx  25932  dvfsumlem3  25942  dvfsumlem4  25943  dvfsum2  25948  ftc1lem4  25953  coemullem  26162  ulmbdd  26314  ulmcn  26315  ulmdvlem1  26316  radcnvle  26336  pserdvlem1  26344  pserdv  26346  abelthlem7  26355  pilem2  26369  pilem3  26370  cosordlem  26446  abslogle  26534  logccv  26579  cxpaddle  26669  ang180lem2  26727  heron  26755  atanlogaddlem  26830  atans2  26848  cxp2limlem  26893  scvxcvx  26903  jensenlem2  26905  amgmlem  26907  logdiflbnd  26912  harmonicbnd4  26928  fsumharmonic  26929  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  lgambdd  26954  lgamucov  26955  regamcl  26978  ftalem5  26994  efnnfsumcl  27020  efchtdvds  27076  chtublem  27129  chtub  27130  logfaclbnd  27140  perfectlem2  27148  bposlem7  27208  bposlem9  27210  lgsdirprm  27249  gausslemma2dlem1a  27283  2sqlem8  27344  chpchtlim  27397  vmadivsumb  27401  rplogsumlem1  27402  dchrisumlem2  27408  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0re  27431  dchrisum0lem1b  27433  mulog2sumlem1  27452  mulog2sumlem2  27453  logsqvma2  27461  log2sumbnd  27462  selberglem2  27464  selbergb  27467  selberg2b  27470  chpdifbndlem1  27471  chpdifbndlem2  27472  selberg3lem2  27476  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrsumbnd2  27485  selberg3r  27487  selberg34r  27489  pntsf  27491  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem2a  27508  pntibndlem2  27509  pntibndlem3  27510  pntlemg  27516  pntlemr  27520  pntlemk  27524  pntlemo  27525  pntlem3  27527  abvcxp  27533  padicabv  27548  ostth2lem2  27552  ostth3  27556  brbtwn2  28839  axsegconlem8  28858  axsegconlem10  28860  axpaschlem  28874  axpasch  28875  axeuclidlem  28896  axcontlem2  28899  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  vacn  30630  smcnlem  30633  ubthlem2  30807  minvecolem2  30811  minvecolem3  30812  minvecolem4  30816  minvecolem5  30817  nmoptrii  32030  hstle  32166  staddi  32182  stadd3i  32184  lt2addrd  32681  nndiffz1  32716  nexple  32776  wrdt2ind  32882  cshwrnid  32890  fsumrp0cl  32969  pmtrto1cl  33063  fzto1st  33067  psgnfzto1st  33069  constrresqrtcl  33774  cos9thpiminplylem1  33779  1smat1  33801  sqsscirc1  33905  cnre2csqlem  33907  tpr2rico  33909  dya2iocress  34272  dya2iocbrsiga  34273  dya2icobrsiga  34274  dya2icoseg  34275  dya2iocucvr  34282  sxbrsigalem2  34284  omssubaddlem  34297  fibp1  34399  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsgt1  34509  ballotlemsel1i  34511  plymulx0  34545  breprexplemc  34630  breprexp  34631  logdivsqrle  34648  resconn  35240  faclim  35740  dnizphlfeqhlf  36471  dnibndlem4  36476  dnibndlem6  36478  dnibndlem8  36480  dnibndlem9  36481  dnibndlem10  36482  dnibndlem11  36483  dnibndlem13  36485  dnibnd  36486  knoppcnlem4  36491  unblimceq0lem  36501  unblimceq0  36502  unbdqndv2lem1  36504  poimirlem29  37650  heicant  37656  opnmbllem0  37657  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  mbfposadd  37668  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem1  37679  itgaddnclem2  37680  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  ftc1cnnclem  37692  ftc1anclem4  37697  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  areacirclem5  37713  mettrifi  37758  isbnd3  37785  ssbnd  37789  cntotbnd  37797  heibor1lem  37810  bfplem2  37824  rrnequiv  37836  iccbnd  37841  lcmineqlem18  42041  lcmineqlem20  42043  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  posbezout  42095  aks6d1c1  42111  aks6d1c2  42125  2np3bcnp1  42139  2ap1caineq  42140  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  bcle2d  42174  aks6d1c7lem1  42175  readdridaddlidd  42253  resubeulem1  42370  resubeulem2  42371  resubeu  42372  readdsub  42379  reladdrsub  42380  resubidaddlidlem  42389  renegid2  42409  sn-it0e0  42411  sn-0tie0  42446  sn-addlt0d  42453  sn-addgt0d  42454  cnreeu  42485  dffltz  42629  fltnltalem  42657  fltnlta  42658  3cubeslem1  42679  pellexlem2  42825  pell1qrge1  42865  pell14qrgapw  42871  pellqrexplicit  42872  pellqrex  42874  pellfundge  42877  pellfundgt1  42878  rmspecfund  42904  rmxycomplete  42913  ltrmynn0  42944  jm2.24nn  42955  jm2.24  42959  fzmaxdif  42977  jm2.26lem3  42997  jm3.1lem2  43014  areaquad  43212  sqrtcvallem4  43635  sqrtcvallem5  43636  sqrtcval  43637  imo72b2lem0  44161  hashnzfzclim  44318  binomcxplemnotnn0  44352  zltlesub  45290  lt3addmuld  45306  absnpncan2d  45307  fperiodmullem  45308  lt4addmuld  45311  absnpncan3d  45312  supxrgelem  45340  supxrge  45341  ltadd12dd  45346  xralrple2  45357  infxr  45370  infleinflem2  45374  xralrple4  45376  xralrple3  45377  xrralrecnnle  45386  eliooshift  45511  iccshift  45523  iooshift  45527  iooiinicc  45547  iooiinioc  45561  fsumnncl  45577  climinf  45611  climsuselem1  45612  sumnnodd  45635  lptre2pt  45645  addlimc  45653  0ellimcdiv  45654  limclner  45656  climleltrp  45681  liminfltlem  45809  fperdvper  45924  dvdivbd  45928  dvbdfbdioolem2  45934  dvbdfbdioo  45935  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvxpaek  45945  dvnmul  45948  iblsplit  45971  iblspltprt  45978  itgspltprt  45984  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stoweidlem1  46006  stoweidlem11  46016  stoweidlem13  46018  stoweidlem14  46019  stoweidlem20  46025  stoweidlem21  46026  stoweidlem26  46031  stoweidlem44  46049  stoweidlem60  46065  wallispilem3  46072  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem1  46079  stirlinglem3  46081  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  dirker2re  46097  dirkerval2  46099  dirkerre  46100  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkeritg  46107  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem4  46116  fourierdlem5  46117  fourierdlem6  46118  fourierdlem7  46119  fourierdlem9  46121  fourierdlem10  46122  fourierdlem18  46130  fourierdlem19  46131  fourierdlem20  46132  fourierdlem26  46138  fourierdlem28  46140  fourierdlem30  46142  fourierdlem35  46147  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem47  46158  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem53  46164  fourierdlem57  46168  fourierdlem59  46170  fourierdlem60  46171  fourierdlem61  46172  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem66  46177  fourierdlem68  46179  fourierdlem71  46182  fourierdlem72  46183  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem78  46189  fourierdlem79  46190  fourierdlem80  46191  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem84  46195  fourierdlem87  46198  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem94  46205  fourierdlem95  46206  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  qndenserrnbllem  46299  ioorrnopnlem  46309  ioorrnopnxrlem  46311  sge0xaddlem1  46438  sge0xaddlem2  46439  omeiunltfirp  46524  carageniuncllem2  46527  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoiqssbllem1  46627  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem2  46632  hspmbllem3  46633  ovolval5lem1  46657  iinhoiicclem  46678  iinhoiicc  46679  iunhoiioolem  46680  iccvonmbllem  46683  vonioolem1  46685  vonioolem2  46686  vonicclem1  46688  vonicclem2  46689  preimaleiinlt  46726  salpreimaltle  46731  smfaddlem1  46768  smfadd  46770  smflimlem3  46778  smflimlem4  46779  smflimlem6  46781  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  ormkglobd  46880  zm1nn  47307  requad01  47626  requad1  47627  requad2  47628  perfectALTVlem2  47727  nnsum4primesevenALTV  47806  bgoldbtbndlem2  47811  gpgvtxedg0  48058  gpgvtxedg1  48059  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx13starlem2  48067  dignn0flhalflem1  48608  affinecomb1  48695  resum2sqcl  48699  2sphere  48742  line2  48745  itsclc0lem1  48749  itscnhlc0yqe  48752  itsclquadb  48769  2itscp  48774  itscnhlinecirc02plem1  48775  itscnhlinecirc02plem3  48777  itscnhlinecirc02p  48778  inlinecirc02plem  48779  amgmwlem  49795