Theorem readdcld 11208

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 7392  ℝcr 11069   + caddc 11073

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  ltadd2  11284  readdcan  11354  addrid  11360  leadd1  11652  le2add  11666  lesub2  11679  lesub3d  11802  le2addd  11803  supaddc  12156  supadd  12157  cju  12188  nnne0  12244  div4p1lem1div2  12473  difgtsumgt  12531  eluzmn  12843  rpnnen1lem5  12979  addlelt  13106  xralrple  13205  xov1plusxeqvd  13499  zltaddlt1le  13506  elincfzoext  13726  fladdz  13832  2tnp1ge0ge0  13836  flhalf  13837  fldiv  13867  modaddb  13916  modaddmodup  13944  modaddmodlo  13945  addmodlteq  13956  discr1  14249  discr  14250  ccatalpha  14604  2cshw  14823  remim  15127  remullem  15138  01sqrexlem7  15258  absrele  15318  abstri  15341  abs3lem  15349  amgm2  15380  bhmafibid1  15478  mulcn2  15606  o1add  15624  o1sub  15626  lo1add  15637  caucvgrlem  15683  iseraltlem2  15693  iseraltlem3  15694  fsumabs  15812  o1fsum  15824  climcndslem2  15863  tanhlt1  16175  eirrlem  16219  ruclem1  16246  ruclem2  16247  ruclem3  16248  ltoddhalfle  16378  bitscmp  16455  sadcaddlem  16474  sadasslem  16487  smuval2  16499  iserodd  16854  prmreclem4  16938  4sqlem5  16961  4sqlem6  16962  4sqlem12  16975  4sqlem15  16978  4sqlem16  16979  prmgaplem7  17076  prmgaplem8  17077  2expltfac  17111  cshwshashlem2  17115  chfacfscmul0  22898  chfacfscmulgsum  22900  chfacfpmmul0  22902  chfacfpmmulgsum  22904  prdsxmetlem  24408  xblss2ps  24441  metustexhalf  24596  nrmmetd  24614  ngptgp  24676  nlmvscnlem2  24725  nlmvscnlem1  24726  nmotri  24779  nghmplusg  24780  blcvx  24838  iccntr  24862  icccmplem2  24864  reconnlem2  24868  metdcnlem  24877  metnrmlem3  24902  cnllycmp  24998  lebnumii  25008  tcphcphlem1  25277  ipcnlem2  25286  ipcnlem1  25287  csbren  25441  trirn  25442  minveclem2  25468  minveclem3b  25470  minveclem4  25474  ivthlem2  25494  ovolgelb  25522  ovollb2lem  25530  ovolunlem1a  25538  ovolunlem1  25539  ovolfiniun  25543  ovoliunlem1  25544  ovoliunlem2  25545  ovolshftlem1  25551  ovolscalem1  25555  ovolicopnf  25566  ismbl2  25569  nulmbl2  25578  unmbl  25579  voliunlem2  25593  ioombl1lem2  25601  ioombl1lem4  25603  ioombl1  25604  ioorcl2  25614  uniioombllem1  25623  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  uniioombl  25631  opnmbllem  25643  volcn  25648  itg1addlem4  25741  mbfi1fseqlem4  25760  mbfi1fseqlem6  25762  itg2splitlem  25790  itg2split  25791  itg2monolem3  25794  itg2addlem  25800  ibladdlem  25862  itgaddlem1  25865  itgaddlem2  25866  iblabslem  25870  iblabs  25871  dvferm1lem  26026  dvferm2lem  26028  dvlip2  26037  lhop1lem  26055  lhop1  26056  lhop  26058  dvcnvrelem1  26059  dvcnvrelem2  26060  dvcnvre  26061  dvcvx  26062  dvfsumlem3  26070  dvfsumlem4  26071  dvfsum2  26076  ftc1lem4  26081  coemullem  26290  ulmbdd  26438  ulmcn  26439  ulmdvlem1  26440  radcnvle  26460  pserdvlem1  26467  pserdv  26469  abelthlem7  26478  pilem2  26492  pilem3  26493  cosordlem  26572  abslogle  26660  logccv  26705  cxpaddle  26794  ang180lem2  26852  heron  26880  atanlogaddlem  26955  atans2  26973  cxp2limlem  27017  scvxcvx  27027  jensenlem2  27029  amgmlem  27031  logdiflbnd  27036  harmonicbnd4  27052  fsumharmonic  27053  lgamgulmlem3  27072  lgamgulmlem4  27073  lgamgulmlem5  27074  lgamgulmlem6  27075  lgambdd  27078  lgamucov  27079  regamcl  27102  ftalem5  27118  efnnfsumcl  27144  efchtdvds  27200  chtublem  27252  chtub  27253  logfaclbnd  27263  perfectlem2  27271  bposlem7  27331  bposlem9  27333  lgsdirprm  27372  gausslemma2dlem1a  27406  2sqlem8  27467  chpchtlim  27520  vmadivsumb  27524  rplogsumlem1  27525  dchrisumlem2  27531  dchrvmasumlem2  27539  dchrvmasumiflem1  27542  dchrisum0re  27554  dchrisum0lem1b  27556  mulog2sumlem1  27575  mulog2sumlem2  27576  logsqvma2  27584  log2sumbnd  27585  selberglem2  27587  selbergb  27590  selberg2b  27593  chpdifbndlem1  27594  chpdifbndlem2  27595  selberg3lem2  27599  selberg3  27600  selberg4lem1  27601  selberg4  27602  pntrsumbnd2  27608  selberg3r  27610  selberg34r  27612  pntsf  27614  pntrlog2bndlem1  27618  pntrlog2bndlem2  27619  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntrlog2bndlem6  27624  pntrlog2bnd  27625  pntpbnd1a  27626  pntpbnd2  27628  pntibndlem2a  27631  pntibndlem2  27632  pntibndlem3  27633  pntlemg  27639  pntlemr  27643  pntlemk  27647  pntlemo  27648  pntlem3  27650  abvcxp  27656  padicabv  27671  ostth2lem2  27675  ostth3  27679  brbtwn2  29052  axsegconlem8  29071  axsegconlem10  29073  axpaschlem  29087  axpasch  29088  axeuclidlem  29109  axcontlem2  29112  crctcshwlkn0lem3  29958  crctcshwlkn0lem5  29960  vacn  30843  smcnlem  30846  ubthlem2  31020  minvecolem2  31024  minvecolem3  31025  minvecolem4  31029  minvecolem5  31030  nmoptrii  32243  hstle  32379  staddi  32395  stadd3i  32397  lt2addrd  32902  nndiffz1  32938  nexple  32996  wrdt2ind  33092  cshwrnid  33100  fsumrp0cl  33160  pmtrto1cl  33240  fzto1st  33244  psgnfzto1st  33246  constrresqrtcl  34035  cos9thpiminplylem1  34040  1smat1  34062  sqsscirc1  34166  cnre2csqlem  34168  tpr2rico  34170  dya2iocress  34532  dya2iocbrsiga  34533  dya2icobrsiga  34534  dya2icoseg  34535  dya2iocucvr  34542  sxbrsigalem2  34544  omssubaddlem  34557  fibp1  34659  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemsgt1  34769  ballotlemsel1i  34771  plymulx0  34805  breprexplemc  34890  breprexp  34891  logdivsqrle  34908  resconn  35560  faclim  36060  dnizphlfeqhlf  36878  dnibndlem4  36883  dnibndlem6  36885  dnibndlem8  36887  dnibndlem9  36888  dnibndlem10  36889  dnibndlem11  36890  dnibndlem13  36892  dnibnd  36893  knoppcnlem4  36898  unblimceq0lem  36908  unblimceq0  36909  unbdqndv2lem1  36911  poimirlem29  38112  heicant  38118  opnmbllem0  38119  mblfinlem3  38122  mblfinlem4  38123  ismblfin  38124  mbfposadd  38130  itg2addnclem  38134  itg2addnclem3  38136  itg2addnc  38137  itg2gt0cn  38138  ibladdnclem  38139  itgaddnclem1  38141  itgaddnclem2  38142  iblabsnclem  38146  iblabsnc  38147  iblmulc2nc  38148  ftc1cnnclem  38154  ftc1anclem4  38159  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  areacirclem5  38175  mettrifi  38220  isbnd3  38247  ssbnd  38251  cntotbnd  38259  heibor1lem  38272  bfplem2  38286  rrnequiv  38298  iccbnd  38303  lcmineqlem18  42627  lcmineqlem20  42629  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1p6  42654  aks4d1p1p7  42655  aks4d1p1p5  42656  aks4d1p1  42657  posbezout  42681  aks6d1c1  42697  aks6d1c2  42711  2np3bcnp1  42725  2ap1caineq  42726  sticksstones6  42732  sticksstones7  42733  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  sticksstones22  42749  bcle2d  42760  aks6d1c7lem1  42761  readdridaddlidd  42837  resubeulem1  42948  resubeulem2  42949  resubeu  42950  readdsub  42957  reladdrsub  42958  resubidaddlidlem  42967  renegid2  42987  sn-it0e0  42989  redivdird  43035  sn-0tie0  43037  sn-addlt0d  43044  sn-addgt0d  43045  cnreeu  43076  dffltz  43180  fltnltalem  43208  fltnlta  43209  3cubeslem1  43229  pellexlem2  43371  pell1qrge1  43411  pell14qrgapw  43417  pellqrexplicit  43418  pellqrex  43420  pellfundge  43423  pellfundgt1  43424  rmspecfund  43450  rmxycomplete  43458  ltrmynn0  43489  jm2.24nn  43500  jm2.24  43504  fzmaxdif  43522  jm2.26lem3  43542  jm3.1lem2  43559  areaquad  43757  sqrtcvallem4  44179  sqrtcvallem5  44180  sqrtcval  44181  imo72b2lem0  44705  hashnzfzclim  44862  binomcxplemnotnn0  44896  zltlesub  45828  lt3addmuld  45844  absnpncan2d  45845  fperiodmullem  45846  lt4addmuld  45849  absnpncan3d  45850  supxrgelem  45877  supxrge  45878  ltadd12dd  45883  xralrple2  45894  infxr  45906  infleinflem2  45910  xralrple4  45912  xralrple3  45913  xrralrecnnle  45922  eliooshift  46046  iccshift  46058  iooshift  46062  iooiinicc  46082  iooiinioc  46096  fsumnncl  46112  climinf  46146  climsuselem1  46147  sumnnodd  46170  lptre2pt  46178  addlimc  46186  0ellimcdiv  46187  limclner  46189  climleltrp  46214  liminfltlem  46342  fperdvper  46457  dvdivbd  46461  dvbdfbdioolem2  46467  dvbdfbdioo  46468  ioodvbdlimc1lem1  46469  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvxpaek  46478  dvnmul  46481  iblsplit  46504  iblspltprt  46511  itgspltprt  46517  itgiccshift  46518  itgperiod  46519  itgsbtaddcnst  46520  stoweidlem1  46539  stoweidlem11  46549  stoweidlem13  46551  stoweidlem14  46552  stoweidlem20  46558  stoweidlem21  46559  stoweidlem26  46564  stoweidlem44  46582  stoweidlem60  46598  wallispilem3  46605  wallispilem4  46606  wallispilem5  46607  wallispi  46608  wallispi2lem1  46609  wallispi2lem2  46610  stirlinglem1  46612  stirlinglem3  46614  stirlinglem5  46616  stirlinglem6  46617  stirlinglem7  46618  stirlinglem10  46621  stirlinglem11  46622  stirlinglem12  46623  dirker2re  46630  dirkerval2  46632  dirkerre  46633  dirkerper  46634  dirkertrigeqlem1  46636  dirkertrigeqlem2  46637  dirkeritg  46640  dirkercncflem1  46641  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem4  46649  fourierdlem5  46650  fourierdlem6  46651  fourierdlem7  46652  fourierdlem9  46654  fourierdlem10  46655  fourierdlem18  46663  fourierdlem19  46664  fourierdlem20  46665  fourierdlem26  46671  fourierdlem28  46673  fourierdlem30  46675  fourierdlem35  46680  fourierdlem40  46685  fourierdlem41  46686  fourierdlem42  46687  fourierdlem47  46691  fourierdlem48  46692  fourierdlem49  46693  fourierdlem50  46694  fourierdlem51  46695  fourierdlem53  46697  fourierdlem57  46701  fourierdlem59  46703  fourierdlem60  46704  fourierdlem61  46705  fourierdlem63  46707  fourierdlem64  46708  fourierdlem65  46709  fourierdlem66  46710  fourierdlem68  46712  fourierdlem71  46715  fourierdlem72  46716  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem78  46722  fourierdlem79  46723  fourierdlem80  46724  fourierdlem81  46725  fourierdlem82  46726  fourierdlem83  46727  fourierdlem84  46728  fourierdlem87  46731  fourierdlem88  46732  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem92  46736  fourierdlem93  46737  fourierdlem94  46738  fourierdlem95  46739  fourierdlem97  46741  fourierdlem101  46745  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierdlem112  46756  fourierdlem113  46757  sqwvfoura  46766  sqwvfourb  46767  fouriersw  46769  qndenserrnbllem  46832  ioorrnopnlem  46842  ioorrnopnxrlem  46844  sge0xaddlem1  46971  sge0xaddlem2  46972  omeiunltfirp  47057  carageniuncllem2  47060  hoidmv1lelem1  47129  hoidmv1lelem2  47130  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  hoiqssbllem1  47160  hoiqssbllem2  47161  hoiqssbllem3  47162  hspmbllem2  47165  hspmbllem3  47166  ovolval5lem1  47190  iinhoiicclem  47211  iinhoiicc  47212  iunhoiioolem  47213  iccvonmbllem  47216  vonioolem1  47218  vonioolem2  47219  vonicclem1  47221  vonicclem2  47222  preimaleiinlt  47259  salpreimaltle  47264  smfaddlem1  47301  smfadd  47303  smflimlem3  47311  smflimlem4  47312  smflimlem6  47314  smfmullem1  47329  smfmullem2  47330  smfmullem3  47331  ormkglobd  47415  zm1nn  47860  requad01  48207  requad1  48208  requad2  48209  perfectALTVlem2  48308  nnsum4primesevenALTV  48387  bgoldbtbndlem2  48392  gpgvtxedg0  48649  gpgvtxedg1  48650  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx13starlem2  48658  dignn0flhalflem1  49201  affinecomb1  49288  resum2sqcl  49292  2sphere  49335  line2  49338  itsclc0lem1  49342  itscnhlc0yqe  49345  itsclquadb  49362  2itscp  49367  itscnhlinecirc02plem1  49368  itscnhlinecirc02plem3  49370  itscnhlinecirc02p  49371  inlinecirc02plem  49372  amgmwlem  50387