Theorem readdcld 11050

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

Syntax hints:   → wi 4   ∈ wcel 2104  (class class class)co 7307  ℝcr 10916   + caddc 10920

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

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

This theorem is referenced by:  ltadd2  11125  readdcan  11195  addid1  11201  leadd1  11489  le2add  11503  lesub2  11516  lesub3d  11639  supaddc  11988  supadd  11989  cju  12015  nnne0  12053  div4p1lem1div2  12274  difgtsumgt  12332  eluzmn  12635  rpnnen1lem5  12767  addlelt  12890  xralrple  12985  xov1plusxeqvd  13276  zltaddlt1le  13283  elincfzoext  13491  fladdz  13591  2tnp1ge0ge0  13595  flhalf  13596  fldiv  13626  modaddmodup  13700  modaddmodlo  13701  addmodlteq  13712  discr1  14000  discr  14001  ccatalpha  14343  2cshw  14571  remim  14873  remullem  14884  sqrlem7  15005  absrele  15065  abstri  15087  abs3lem  15095  amgm2  15126  bhmafibid1  15222  mulcn2  15350  o1add  15368  o1sub  15370  lo1add  15381  caucvgrlem  15429  iseraltlem2  15439  iseraltlem3  15440  fsumabs  15558  o1fsum  15570  climcndslem2  15607  tanhlt1  15914  eirrlem  15958  ruclem1  15985  ruclem2  15986  ruclem3  15987  ltoddhalfle  16115  bitscmp  16190  sadcaddlem  16209  sadasslem  16222  smuval2  16234  iserodd  16581  prmreclem4  16665  4sqlem5  16688  4sqlem6  16689  4sqlem12  16702  4sqlem15  16705  4sqlem16  16706  prmgaplem7  16803  prmgaplem8  16804  2expltfac  16839  cshwshashlem2  16843  chfacfscmul0  22052  chfacfscmulgsum  22054  chfacfpmmul0  22056  chfacfpmmulgsum  22058  prdsxmetlem  23566  xblss2ps  23599  metustexhalf  23757  nrmmetd  23775  ngptgp  23837  nlmvscnlem2  23894  nlmvscnlem1  23895  nmotri  23948  nghmplusg  23949  blcvx  24006  iccntr  24029  icccmplem2  24031  reconnlem2  24035  metdcnlem  24044  metnrmlem3  24069  cnllycmp  24164  lebnumii  24174  tcphcphlem1  24444  ipcnlem2  24453  ipcnlem1  24454  csbren  24608  trirn  24609  minveclem2  24635  minveclem3b  24637  minveclem4  24641  ivthlem2  24661  ovolgelb  24689  ovollb2lem  24697  ovolunlem1a  24705  ovolunlem1  24706  ovolfiniun  24710  ovoliunlem1  24711  ovoliunlem2  24712  ovolshftlem1  24718  ovolscalem1  24722  ovolicopnf  24733  ismbl2  24736  nulmbl2  24745  unmbl  24746  voliunlem2  24760  ioombl1lem2  24768  ioombl1lem4  24770  ioombl1  24771  ioorcl2  24781  uniioombllem1  24790  uniioombllem3  24794  uniioombllem4  24795  uniioombllem5  24796  uniioombl  24798  opnmbllem  24810  volcn  24815  itg1addlem4  24908  itg1addlem4OLD  24909  mbfi1fseqlem4  24928  mbfi1fseqlem6  24930  itg2splitlem  24958  itg2split  24959  itg2monolem3  24962  itg2addlem  24968  ibladdlem  25029  itgaddlem1  25032  itgaddlem2  25033  iblabslem  25037  iblabs  25038  dvferm1lem  25193  dvferm2lem  25195  dvlip2  25204  lhop1lem  25222  lhop1  25223  lhop  25225  dvcnvrelem1  25226  dvcnvrelem2  25227  dvcnvre  25228  dvcvx  25229  dvfsumlem3  25237  dvfsumlem4  25238  dvfsum2  25243  ftc1lem4  25248  coemullem  25456  ulmbdd  25602  ulmcn  25603  ulmdvlem1  25604  radcnvle  25624  pserdvlem1  25631  pserdv  25633  abelthlem7  25642  pilem2  25656  pilem3  25657  cosordlem  25731  abslogle  25818  logccv  25863  cxpaddle  25950  ang180lem2  26005  heron  26033  atanlogaddlem  26108  atans2  26126  cxp2limlem  26170  scvxcvx  26180  jensenlem2  26182  amgmlem  26184  logdiflbnd  26189  harmonicbnd4  26205  fsumharmonic  26206  lgamgulmlem3  26225  lgamgulmlem4  26226  lgamgulmlem5  26227  lgamgulmlem6  26228  lgambdd  26231  lgamucov  26232  regamcl  26255  ftalem5  26271  efnnfsumcl  26297  efchtdvds  26353  chtublem  26404  chtub  26405  logfaclbnd  26415  perfectlem2  26423  bposlem7  26483  bposlem9  26485  lgsdirprm  26524  gausslemma2dlem1a  26558  2sqlem8  26619  chpchtlim  26672  vmadivsumb  26676  rplogsumlem1  26677  dchrisumlem2  26683  dchrvmasumlem2  26691  dchrvmasumiflem1  26694  dchrisum0re  26706  dchrisum0lem1b  26708  mulog2sumlem1  26727  mulog2sumlem2  26728  logsqvma2  26736  log2sumbnd  26737  selberglem2  26739  selbergb  26742  selberg2b  26745  chpdifbndlem1  26746  chpdifbndlem2  26747  selberg3lem2  26751  selberg3  26752  selberg4lem1  26753  selberg4  26754  pntrsumbnd2  26760  selberg3r  26762  selberg34r  26764  pntsf  26766  pntrlog2bndlem1  26770  pntrlog2bndlem2  26771  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  pntrlog2bndlem6  26776  pntrlog2bnd  26777  pntpbnd1a  26778  pntpbnd2  26780  pntibndlem2a  26783  pntibndlem2  26784  pntibndlem3  26785  pntlemg  26791  pntlemr  26795  pntlemk  26799  pntlemo  26800  pntlem3  26802  abvcxp  26808  padicabv  26823  ostth2lem2  26827  ostth3  26831  brbtwn2  27318  axsegconlem8  27337  axsegconlem10  27339  axpaschlem  27353  axpasch  27354  axeuclidlem  27375  axcontlem2  27378  crctcshwlkn0lem3  28222  crctcshwlkn0lem5  28224  vacn  29101  smcnlem  29104  ubthlem2  29278  minvecolem2  29282  minvecolem3  29283  minvecolem4  29287  minvecolem5  29288  nmoptrii  30501  hstle  30637  staddi  30653  stadd3i  30655  lt2addrd  31119  nndiffz1  31152  wrdt2ind  31270  cshwrnid  31278  fsumrp0cl  31349  pmtrto1cl  31411  fzto1st  31415  psgnfzto1st  31417  1smat1  31799  sqsscirc1  31903  cnre2csqlem  31905  tpr2rico  31907  nexple  32022  dya2iocress  32286  dya2iocbrsiga  32287  dya2icobrsiga  32288  dya2icoseg  32289  dya2iocucvr  32296  sxbrsigalem2  32298  omssubaddlem  32311  fibp1  32413  ballotlemfc0  32504  ballotlemfcc  32505  ballotlemsgt1  32522  ballotlemsel1i  32524  plymulx0  32571  breprexplemc  32657  breprexp  32658  logdivsqrle  32675  resconn  33253  faclim  33757  dnizphlfeqhlf  34701  dnibndlem4  34706  dnibndlem6  34708  dnibndlem8  34710  dnibndlem9  34711  dnibndlem10  34712  dnibndlem11  34713  dnibndlem13  34715  dnibnd  34716  knoppcnlem4  34721  unblimceq0lem  34731  unblimceq0  34732  unbdqndv2lem1  34734  poimirlem29  35850  heicant  35856  opnmbllem0  35857  mblfinlem3  35860  mblfinlem4  35861  ismblfin  35862  mbfposadd  35868  itg2addnclem  35872  itg2addnclem3  35874  itg2addnc  35875  itg2gt0cn  35876  ibladdnclem  35877  itgaddnclem1  35879  itgaddnclem2  35880  iblabsnclem  35884  iblabsnc  35885  iblmulc2nc  35886  ftc1cnnclem  35892  ftc1anclem4  35897  ftc1anclem7  35900  ftc1anclem8  35901  ftc1anc  35902  areacirclem5  35913  mettrifi  35959  isbnd3  35986  ssbnd  35990  cntotbnd  35998  heibor1lem  36011  bfplem2  36025  rrnequiv  36037  iccbnd  36042  lcmineqlem18  40096  lcmineqlem20  40098  aks4d1p1p3  40119  aks4d1p1p2  40120  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  2np3bcnp1  40142  2ap1caineq  40143  sticksstones6  40149  sticksstones7  40150  sticksstones10  40153  sticksstones12a  40155  sticksstones12  40156  sticksstones22  40166  metakunt29  40195  2xp3dxp2ge1d  40204  factwoffsmonot  40205  readdid1addid2d  40331  resubeulem1  40395  resubeulem2  40396  resubeu  40397  readdsub  40404  reladdrsub  40405  resubidaddid1lem  40414  renegid2  40433  sn-it0e0  40434  sn-0tie0  40458  cnreeu  40475  dffltz  40508  fltnltalem  40536  fltnlta  40537  3cubeslem1  40543  pellexlem2  40689  pell1qrge1  40729  pell14qrgapw  40735  pellqrexplicit  40736  pellqrex  40738  pellfundge  40741  pellfundgt1  40742  rmspecfund  40768  rmxycomplete  40777  ltrmynn0  40808  jm2.24nn  40819  jm2.24  40823  fzmaxdif  40841  jm2.26lem3  40861  jm3.1lem2  40878  areaquad  41085  sqrtcvallem4  41285  sqrtcvallem5  41286  sqrtcval  41287  imo72b2lem0  41814  hashnzfzclim  41978  binomcxplemnotnn0  42012  zltlesub  42872  lt3addmuld  42888  absnpncan2d  42889  fperiodmullem  42890  lt4addmuld  42893  absnpncan3d  42894  leadd12dd  42903  supxrgelem  42924  supxrge  42925  ltadd12dd  42930  xralrple2  42941  infxr  42954  infleinflem2  42958  xralrple4  42960  xralrple3  42961  xrralrecnnle  42970  eliooshift  43093  iccshift  43105  iooshift  43109  iooiinicc  43129  iooiinioc  43143  fsumnncl  43162  climinf  43196  climsuselem1  43197  sumnnodd  43220  lptre2pt  43230  addlimc  43238  0ellimcdiv  43239  limclner  43241  climleltrp  43266  liminfltlem  43394  fperdvper  43509  dvdivbd  43513  dvbdfbdioolem2  43519  dvbdfbdioo  43520  ioodvbdlimc1lem1  43521  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvxpaek  43530  dvnmul  43533  iblsplit  43556  iblspltprt  43563  itgspltprt  43569  itgiccshift  43570  itgperiod  43571  itgsbtaddcnst  43572  stoweidlem1  43591  stoweidlem11  43601  stoweidlem13  43603  stoweidlem14  43604  stoweidlem20  43610  stoweidlem21  43611  stoweidlem26  43616  stoweidlem44  43634  stoweidlem60  43650  wallispilem3  43657  wallispilem4  43658  wallispilem5  43659  wallispi  43660  wallispi2lem1  43661  wallispi2lem2  43662  stirlinglem1  43664  stirlinglem3  43666  stirlinglem5  43668  stirlinglem6  43669  stirlinglem7  43670  stirlinglem10  43673  stirlinglem11  43674  stirlinglem12  43675  dirker2re  43682  dirkerval2  43684  dirkerre  43685  dirkerper  43686  dirkertrigeqlem1  43688  dirkertrigeqlem2  43689  dirkeritg  43692  dirkercncflem1  43693  dirkercncflem2  43694  dirkercncflem4  43696  fourierdlem4  43701  fourierdlem5  43702  fourierdlem6  43703  fourierdlem7  43704  fourierdlem9  43706  fourierdlem10  43707  fourierdlem18  43715  fourierdlem19  43716  fourierdlem20  43717  fourierdlem26  43723  fourierdlem28  43725  fourierdlem30  43727  fourierdlem35  43732  fourierdlem40  43737  fourierdlem41  43738  fourierdlem42  43739  fourierdlem47  43743  fourierdlem48  43744  fourierdlem49  43745  fourierdlem50  43746  fourierdlem51  43747  fourierdlem53  43749  fourierdlem57  43753  fourierdlem59  43755  fourierdlem60  43756  fourierdlem61  43757  fourierdlem63  43759  fourierdlem64  43760  fourierdlem65  43761  fourierdlem66  43762  fourierdlem68  43764  fourierdlem71  43767  fourierdlem72  43768  fourierdlem74  43770  fourierdlem75  43771  fourierdlem76  43772  fourierdlem78  43774  fourierdlem79  43775  fourierdlem80  43776  fourierdlem81  43777  fourierdlem82  43778  fourierdlem83  43779  fourierdlem84  43780  fourierdlem87  43783  fourierdlem88  43784  fourierdlem89  43785  fourierdlem90  43786  fourierdlem91  43787  fourierdlem92  43788  fourierdlem93  43789  fourierdlem94  43790  fourierdlem95  43791  fourierdlem97  43793  fourierdlem101  43797  fourierdlem103  43799  fourierdlem104  43800  fourierdlem111  43807  fourierdlem112  43808  fourierdlem113  43809  sqwvfoura  43818  sqwvfourb  43819  fouriersw  43821  qndenserrnbllem  43884  ioorrnopnlem  43894  ioorrnopnxrlem  43896  sge0xaddlem1  44021  sge0xaddlem2  44022  omeiunltfirp  44107  carageniuncllem2  44110  hoidmv1lelem1  44179  hoidmv1lelem2  44180  hoidmvlelem1  44183  hoidmvlelem2  44184  hoidmvlelem3  44185  hoidmvlelem4  44186  hoiqssbllem1  44210  hoiqssbllem2  44211  hoiqssbllem3  44212  hspmbllem2  44215  hspmbllem3  44216  ovolval5lem1  44240  iinhoiicclem  44261  iinhoiicc  44262  iunhoiioolem  44263  iccvonmbllem  44266  vonioolem1  44268  vonioolem2  44269  vonicclem1  44271  vonicclem2  44272  preimaleiinlt  44309  salpreimaltle  44314  smfaddlem1  44351  smfadd  44353  smflimlem3  44361  smflimlem4  44362  smflimlem6  44364  smfmullem1  44379  smfmullem2  44380  smfmullem3  44381  zm1nn  44852  requad01  45131  requad1  45132  requad2  45133  perfectALTVlem2  45232  nnsum4primesevenALTV  45311  bgoldbtbndlem2  45316  dignn0flhalflem1  46019  affinecomb1  46106  resum2sqcl  46110  2sphere  46153  line2  46156  itsclc0lem1  46160  itscnhlc0yqe  46163  itsclquadb  46180  2itscp  46185  itscnhlinecirc02plem1  46186  itscnhlinecirc02plem3  46188  itscnhlinecirc02p  46189  inlinecirc02plem  46190  amgmwlem  46564