Theorem readdcld 11174

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037   + caddc 11041

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

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

This theorem is referenced by:  ltadd2  11250  readdcan  11320  addrid  11326  leadd1  11618  le2add  11632  lesub2  11645  lesub3d  11768  le2addd  11769  supaddc  12123  supadd  12124  cju  12155  nnne0  12211  div4p1lem1div2  12432  difgtsumgt  12490  eluzmn  12795  rpnnen1lem5  12931  addlelt  13058  xralrple  13157  xov1plusxeqvd  13451  zltaddlt1le  13458  elincfzoext  13678  fladdz  13784  2tnp1ge0ge0  13788  flhalf  13789  fldiv  13819  modaddb  13868  modaddmodup  13896  modaddmodlo  13897  addmodlteq  13908  discr1  14201  discr  14202  ccatalpha  14556  2cshw  14775  remim  15079  remullem  15090  01sqrexlem7  15210  absrele  15270  abstri  15293  abs3lem  15301  amgm2  15332  bhmafibid1  15430  mulcn2  15558  o1add  15576  o1sub  15578  lo1add  15589  caucvgrlem  15635  iseraltlem2  15645  iseraltlem3  15646  fsumabs  15764  o1fsum  15776  climcndslem2  15815  tanhlt1  16127  eirrlem  16171  ruclem1  16198  ruclem2  16199  ruclem3  16200  ltoddhalfle  16330  bitscmp  16407  sadcaddlem  16426  sadasslem  16439  smuval2  16451  iserodd  16806  prmreclem4  16890  4sqlem5  16913  4sqlem6  16914  4sqlem12  16927  4sqlem15  16930  4sqlem16  16931  prmgaplem7  17028  prmgaplem8  17029  2expltfac  17063  cshwshashlem2  17067  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  prdsxmetlem  24333  xblss2ps  24366  metustexhalf  24521  nrmmetd  24539  ngptgp  24601  nlmvscnlem2  24650  nlmvscnlem1  24651  nmotri  24704  nghmplusg  24705  blcvx  24763  iccntr  24787  icccmplem2  24789  reconnlem2  24793  metdcnlem  24802  metnrmlem3  24827  cnllycmp  24923  lebnumii  24933  tcphcphlem1  25202  ipcnlem2  25211  ipcnlem1  25212  csbren  25366  trirn  25367  minveclem2  25393  minveclem3b  25395  minveclem4  25399  ivthlem2  25419  ovolgelb  25447  ovollb2lem  25455  ovolunlem1a  25463  ovolunlem1  25464  ovolfiniun  25468  ovoliunlem1  25469  ovoliunlem2  25470  ovolshftlem1  25476  ovolscalem1  25480  ovolicopnf  25491  ismbl2  25494  nulmbl2  25503  unmbl  25504  voliunlem2  25518  ioombl1lem2  25526  ioombl1lem4  25528  ioombl1  25529  ioorcl2  25539  uniioombllem1  25548  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombl  25556  opnmbllem  25568  volcn  25573  itg1addlem4  25666  mbfi1fseqlem4  25685  mbfi1fseqlem6  25687  itg2splitlem  25715  itg2split  25716  itg2monolem3  25719  itg2addlem  25725  ibladdlem  25787  itgaddlem1  25790  itgaddlem2  25791  iblabslem  25795  iblabs  25796  dvferm1lem  25951  dvferm2lem  25953  dvlip2  25962  lhop1lem  25980  lhop1  25981  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvcvx  25987  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  ftc1lem4  26006  coemullem  26215  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  radcnvle  26385  pserdvlem1  26392  pserdv  26394  abelthlem7  26403  pilem2  26417  pilem3  26418  cosordlem  26494  abslogle  26582  logccv  26627  cxpaddle  26716  ang180lem2  26774  heron  26802  atanlogaddlem  26877  atans2  26895  cxp2limlem  26939  scvxcvx  26949  jensenlem2  26951  amgmlem  26953  logdiflbnd  26958  harmonicbnd4  26974  fsumharmonic  26975  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgambdd  27000  lgamucov  27001  regamcl  27024  ftalem5  27040  efnnfsumcl  27066  efchtdvds  27122  chtublem  27174  chtub  27175  logfaclbnd  27185  perfectlem2  27193  bposlem7  27253  bposlem9  27255  lgsdirprm  27294  gausslemma2dlem1a  27328  2sqlem8  27389  chpchtlim  27442  vmadivsumb  27446  rplogsumlem1  27447  dchrisumlem2  27453  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0re  27476  dchrisum0lem1b  27478  mulog2sumlem1  27497  mulog2sumlem2  27498  logsqvma2  27506  log2sumbnd  27507  selberglem2  27509  selbergb  27512  selberg2b  27515  chpdifbndlem1  27516  chpdifbndlem2  27517  selberg3lem2  27521  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrsumbnd2  27530  selberg3r  27532  selberg34r  27534  pntsf  27536  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem2a  27553  pntibndlem2  27554  pntibndlem3  27555  pntlemg  27561  pntlemr  27565  pntlemk  27569  pntlemo  27570  pntlem3  27572  abvcxp  27578  padicabv  27593  ostth2lem2  27597  ostth3  27601  brbtwn2  28974  axsegconlem8  28993  axsegconlem10  28995  axpaschlem  29009  axpasch  29010  axeuclidlem  29031  axcontlem2  29034  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  vacn  30765  smcnlem  30768  ubthlem2  30942  minvecolem2  30946  minvecolem3  30947  minvecolem4  30951  minvecolem5  30952  nmoptrii  32165  hstle  32301  staddi  32317  stadd3i  32319  lt2addrd  32823  nndiffz1  32859  nexple  32917  wrdt2ind  33013  cshwrnid  33021  fsumrp0cl  33081  pmtrto1cl  33160  fzto1st  33164  psgnfzto1st  33166  constrresqrtcl  33921  cos9thpiminplylem1  33926  1smat1  33948  sqsscirc1  34052  cnre2csqlem  34054  tpr2rico  34056  dya2iocress  34418  dya2iocbrsiga  34419  dya2icobrsiga  34420  dya2icoseg  34421  dya2iocucvr  34428  sxbrsigalem2  34430  omssubaddlem  34443  fibp1  34545  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsgt1  34655  ballotlemsel1i  34657  plymulx0  34691  breprexplemc  34776  breprexp  34777  logdivsqrle  34794  resconn  35428  faclim  35928  dnizphlfeqhlf  36736  dnibndlem4  36741  dnibndlem6  36743  dnibndlem8  36745  dnibndlem9  36746  dnibndlem10  36747  dnibndlem11  36748  dnibndlem13  36750  dnibnd  36751  knoppcnlem4  36756  unblimceq0lem  36766  unblimceq0  36767  unbdqndv2lem1  36769  poimirlem29  37970  heicant  37976  opnmbllem0  37977  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  mbfposadd  37988  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem1  37999  itgaddnclem2  38000  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  ftc1cnnclem  38012  ftc1anclem4  38017  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirclem5  38033  mettrifi  38078  isbnd3  38105  ssbnd  38109  cntotbnd  38117  heibor1lem  38130  bfplem2  38144  rrnequiv  38156  iccbnd  38161  lcmineqlem18  42485  lcmineqlem20  42487  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  posbezout  42539  aks6d1c1  42555  aks6d1c2  42569  2np3bcnp1  42583  2ap1caineq  42584  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  bcle2d  42618  aks6d1c7lem1  42619  readdridaddlidd  42696  resubeulem1  42807  resubeulem2  42808  resubeu  42809  readdsub  42816  reladdrsub  42817  resubidaddlidlem  42826  renegid2  42846  sn-it0e0  42848  redivdird  42894  sn-0tie0  42896  sn-addlt0d  42903  sn-addgt0d  42904  cnreeu  42935  dffltz  43067  fltnltalem  43095  fltnlta  43096  3cubeslem1  43116  pellexlem2  43258  pell1qrge1  43298  pell14qrgapw  43304  pellqrexplicit  43305  pellqrex  43307  pellfundge  43310  pellfundgt1  43311  rmspecfund  43337  rmxycomplete  43345  ltrmynn0  43376  jm2.24nn  43387  jm2.24  43391  fzmaxdif  43409  jm2.26lem3  43429  jm3.1lem2  43446  areaquad  43644  sqrtcvallem4  44066  sqrtcvallem5  44067  sqrtcval  44068  imo72b2lem0  44592  hashnzfzclim  44749  binomcxplemnotnn0  44783  zltlesub  45718  lt3addmuld  45734  absnpncan2d  45735  fperiodmullem  45736  lt4addmuld  45739  absnpncan3d  45740  supxrgelem  45767  supxrge  45768  ltadd12dd  45773  xralrple2  45784  infxr  45796  infleinflem2  45800  xralrple4  45802  xralrple3  45803  xrralrecnnle  45812  eliooshift  45936  iccshift  45948  iooshift  45952  iooiinicc  45972  iooiinioc  45986  fsumnncl  46002  climinf  46036  climsuselem1  46037  sumnnodd  46060  lptre2pt  46068  addlimc  46076  0ellimcdiv  46077  limclner  46079  climleltrp  46104  liminfltlem  46232  fperdvper  46347  dvdivbd  46351  dvbdfbdioolem2  46357  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvxpaek  46368  dvnmul  46371  iblsplit  46394  iblspltprt  46401  itgspltprt  46407  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem1  46429  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem20  46448  stoweidlem21  46449  stoweidlem26  46454  stoweidlem44  46472  stoweidlem60  46488  wallispilem3  46495  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem1  46502  stirlinglem3  46504  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  dirker2re  46520  dirkerval2  46522  dirkerre  46523  dirkerper  46524  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkeritg  46530  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem4  46539  fourierdlem5  46540  fourierdlem6  46541  fourierdlem7  46542  fourierdlem9  46544  fourierdlem10  46545  fourierdlem18  46553  fourierdlem19  46554  fourierdlem20  46555  fourierdlem26  46561  fourierdlem28  46563  fourierdlem30  46565  fourierdlem35  46570  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem53  46587  fourierdlem57  46591  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem66  46600  fourierdlem68  46602  fourierdlem71  46605  fourierdlem72  46606  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem79  46613  fourierdlem80  46614  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem84  46618  fourierdlem87  46621  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem94  46628  fourierdlem95  46629  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  qndenserrnbllem  46722  ioorrnopnlem  46732  ioorrnopnxrlem  46734  sge0xaddlem1  46861  sge0xaddlem2  46862  omeiunltfirp  46947  carageniuncllem2  46950  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoiqssbllem1  47050  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem2  47055  hspmbllem3  47056  ovolval5lem1  47080  iinhoiicclem  47101  iinhoiicc  47102  iunhoiioolem  47103  iccvonmbllem  47106  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  preimaleiinlt  47149  salpreimaltle  47154  smfaddlem1  47191  smfadd  47193  smflimlem3  47201  smflimlem4  47202  smflimlem6  47204  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  ormkglobd  47305  zm1nn  47750  requad01  48097  requad1  48098  requad2  48099  perfectALTVlem2  48198  nnsum4primesevenALTV  48277  bgoldbtbndlem2  48282  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  dignn0flhalflem1  49091  affinecomb1  49178  resum2sqcl  49182  2sphere  49225  line2  49228  itsclc0lem1  49232  itscnhlc0yqe  49235  itsclquadb  49252  2itscp  49257  itscnhlinecirc02plem1  49258  itscnhlinecirc02plem3  49260  itscnhlinecirc02p  49261  inlinecirc02plem  49262  amgmwlem  50277