Theorem readdcld 11226

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

Syntax hints:   → wi 4   ∈ wcel 2145  (class class class)co 7400  ℝcr 11087   + caddc 11091

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  ltadd2  11302  readdcan  11372  addrid  11378  leadd1  11670  le2add  11684  lesub2  11697  lesub3d  11820  le2addd  11821  supaddc  12173  supadd  12174  cju  12205  nnne0  12261  div4p1lem1div2  12490  difgtsumgt  12548  eluzmn  12860  rpnnen1lem5  12996  addlelt  13123  xralrple  13222  xov1plusxeqvd  13516  zltaddlt1le  13523  elincfzoext  13743  fladdz  13849  2tnp1ge0ge0  13853  flhalf  13854  fldiv  13884  modaddb  13933  modaddmodup  13961  modaddmodlo  13962  addmodlteq  13973  discr1  14266  discr  14267  ccatalpha  14621  2cshw  14840  remim  15158  remullem  15169  01sqrexlem7  15289  absrele  15349  abstri  15372  abs3lem  15380  amgm2  15411  bhmafibid1  15509  mulcn2  15637  o1add  15655  o1sub  15657  lo1add  15668  caucvgrlem  15714  iseraltlem2  15724  iseraltlem3  15725  fsumabs  15843  o1fsum  15855  climcndslem2  15894  tanhlt1  16206  eirrlem  16250  ruclem1  16277  ruclem2  16278  ruclem3  16279  ltoddhalfle  16409  bitscmp  16486  sadcaddlem  16505  sadasslem  16518  smuval2  16530  iserodd  16885  prmreclem4  16969  4sqlem5  16992  4sqlem6  16993  4sqlem12  17006  4sqlem15  17009  4sqlem16  17010  prmgaplem7  17107  prmgaplem8  17108  2expltfac  17142  cshwshashlem2  17146  chfacfscmul0  22976  chfacfscmulgsum  22978  chfacfpmmul0  22980  chfacfpmmulgsum  22982  prdsxmetlem  24486  xblss2ps  24519  metustexhalf  24674  nrmmetd  24692  ngptgp  24754  nlmvscnlem2  24803  nlmvscnlem1  24804  nmotri  24857  nghmplusg  24858  blcvx  24916  iccntr  24940  icccmplem2  24942  reconnlem2  24946  metdcnlem  24955  metnrmlem3  24980  cnllycmp  25076  lebnumii  25086  tcphcphlem1  25355  ipcnlem2  25364  ipcnlem1  25365  csbren  25519  trirn  25520  minveclem2  25546  minveclem3b  25548  minveclem4  25552  ivthlem2  25572  ovolgelb  25600  ovollb2lem  25608  ovolunlem1a  25616  ovolunlem1  25617  ovolfiniun  25621  ovoliunlem1  25622  ovoliunlem2  25623  ovolshftlem1  25629  ovolscalem1  25633  ovolicopnf  25644  ismbl2  25647  nulmbl2  25656  unmbl  25657  voliunlem2  25671  ioombl1lem2  25679  ioombl1lem4  25681  ioombl1  25682  ioorcl2  25692  uniioombllem1  25701  uniioombllem3  25705  uniioombllem4  25706  uniioombllem5  25707  uniioombl  25709  opnmbllem  25721  volcn  25726  itg1addlem4  25819  mbfi1fseqlem4  25838  mbfi1fseqlem6  25840  itg2splitlem  25868  itg2split  25869  itg2monolem3  25872  itg2addlem  25878  ibladdlem  25940  itgaddlem1  25943  itgaddlem2  25944  iblabslem  25948  iblabs  25949  dvferm1lem  26104  dvferm2lem  26106  dvlip2  26115  lhop1lem  26133  lhop1  26134  lhop  26136  dvcnvrelem1  26137  dvcnvrelem2  26138  dvcnvre  26139  dvcvx  26140  dvfsumlem3  26148  dvfsumlem4  26149  dvfsum2  26154  ftc1lem4  26159  coemullem  26368  plyn0mulidp  26403  ulmbdd  26519  ulmcn  26520  ulmdvlem1  26521  radcnvle  26541  pserdvlem1  26548  pserdv  26550  abelthlem7  26559  pilem2  26573  pilem3  26574  cosordlem  26653  abslogle  26741  logccv  26786  cxpaddle  26875  ang180lem2  26933  heron  26961  atanlogaddlem  27036  atans2  27054  cxp2limlem  27098  scvxcvx  27108  jensenlem2  27110  amgmlem  27112  logdiflbnd  27117  harmonicbnd4  27133  fsumharmonic  27134  lgamgulmlem3  27153  lgamgulmlem4  27154  lgamgulmlem5  27155  lgamgulmlem6  27156  lgambdd  27159  lgamucov  27160  regamcl  27183  ftalem5  27199  efnnfsumcl  27225  efchtdvds  27281  chtublem  27333  chtub  27334  logfaclbnd  27344  perfectlem2  27352  bposlem7  27412  bposlem9  27414  lgsdirprm  27453  gausslemma2dlem1a  27487  2sqlem8  27548  chpchtlim  27601  vmadivsumb  27605  rplogsumlem1  27606  dchrisumlem2  27612  dchrvmasumlem2  27620  dchrvmasumiflem1  27623  dchrisum0re  27635  dchrisum0lem1b  27637  mulog2sumlem1  27656  mulog2sumlem2  27657  logsqvma2  27665  log2sumbnd  27666  selberglem2  27668  selbergb  27671  selberg2b  27674  chpdifbndlem1  27675  chpdifbndlem2  27676  selberg3lem2  27680  selberg3  27681  selberg4lem1  27682  selberg4  27683  pntrsumbnd2  27689  selberg3r  27691  selberg34r  27693  pntsf  27695  pntrlog2bndlem1  27699  pntrlog2bndlem2  27700  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntrlog2bndlem6  27705  pntrlog2bnd  27706  pntpbnd1a  27707  pntpbnd2  27709  pntibndlem2a  27712  pntibndlem2  27713  pntibndlem3  27714  pntlemg  27720  pntlemr  27724  pntlemk  27728  pntlemo  27729  pntlem3  27731  abvcxp  27737  padicabv  27752  ostth2lem2  27756  ostth3  27760  brbtwn2  29164  axsegconlem8  29183  axsegconlem10  29185  axpaschlem  29199  axpasch  29200  axeuclidlem  29221  axcontlem2  29224  crctcshwlkn0lem3  30070  crctcshwlkn0lem5  30072  vacn  30955  smcnlem  30958  ubthlem2  31132  minvecolem2  31136  minvecolem3  31137  minvecolem4  31141  minvecolem5  31142  nmoptrii  32355  hstle  32491  staddi  32507  stadd3i  32509  lt2addrd  33007  nndiffz1  33043  nexple  33090  wrdt2ind  33186  cshwrnid  33194  fsumrp0cl  33254  pmtrto1cl  33332  fzto1st  33336  psgnfzto1st  33338  constrresqrtcl  34084  cos9thpiminplylem1  34089  1smat1  34111  sqsscirc1  34215  cnre2csqlem  34217  tpr2rico  34219  dya2iocress  34581  dya2iocbrsiga  34582  dya2icobrsiga  34583  dya2icoseg  34584  dya2iocucvr  34591  sxbrsigalem2  34593  omssubaddlem  34606  fibp1  34708  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemsgt1  34818  ballotlemsel1i  34820  breprexplemc  34936  breprexp  34937  logdivsqrle  34954  resconn  35609  faclim  36109  dnizphlfeqhlf  36927  dnibndlem4  36932  dnibndlem6  36934  dnibndlem8  36936  dnibndlem9  36937  dnibndlem10  36938  dnibndlem11  36939  dnibndlem13  36941  dnibnd  36942  knoppcnlem4  36947  unblimceq0lem  36957  unblimceq0  36958  unbdqndv2lem1  36960  poimirlem29  38160  heicant  38166  opnmbllem0  38167  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  mbfposadd  38178  itg2addnclem  38182  itg2addnclem3  38184  itg2addnc  38185  itg2gt0cn  38186  ibladdnclem  38187  itgaddnclem1  38189  itgaddnclem2  38190  iblabsnclem  38194  iblabsnc  38195  iblmulc2nc  38196  ftc1cnnclem  38202  ftc1anclem4  38207  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  areacirclem5  38223  mettrifi  38268  isbnd3  38295  ssbnd  38299  cntotbnd  38307  heibor1lem  38320  bfplem2  38334  rrnequiv  38346  iccbnd  38351  lcmineqlem18  42675  lcmineqlem20  42677  aks4d1p1p3  42698  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1p6  42702  aks4d1p1p7  42703  aks4d1p1p5  42704  aks4d1p1  42705  posbezout  42729  aks6d1c1  42745  aks6d1c2  42759  2np3bcnp1  42773  2ap1caineq  42774  sticksstones6  42780  sticksstones7  42781  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  sticksstones22  42797  bcle2d  42808  aks6d1c7lem1  42809  readdridaddlidd  42885  resubeulem1  42996  resubeulem2  42997  resubeu  42998  readdsub  43005  reladdrsub  43006  resubidaddlidlem  43015  renegid2  43035  sn-it0e0  43037  redivdird  43083  sn-0tie0  43085  sn-addlt0d  43092  sn-addgt0d  43093  cnreeu  43124  dffltz  43228  fltnltalem  43256  fltnlta  43257  3cubeslem1  43277  pellexlem2  43419  pell1qrge1  43459  pell14qrgapw  43465  pellqrexplicit  43466  pellqrex  43468  pellfundge  43471  pellfundgt1  43472  rmspecfund  43498  rmxycomplete  43506  ltrmynn0  43537  jm2.24nn  43548  jm2.24  43552  fzmaxdif  43570  jm2.26lem3  43590  jm3.1lem2  43607  areaquad  43805  sqrtcvallem4  44227  sqrtcvallem5  44228  sqrtcval  44229  imo72b2lem0  44753  hashnzfzclim  44896  binomcxplemnotnn0  44930  zltlesub  45862  lt3addmuld  45878  absnpncan2d  45879  fperiodmullem  45880  lt4addmuld  45883  absnpncan3d  45884  supxrgelem  45911  supxrge  45912  ltadd12dd  45917  xralrple2  45928  infxr  45940  infleinflem2  45944  xralrple4  45946  xralrple3  45947  xrralrecnnle  45956  eliooshift  46080  iccshift  46092  iooshift  46096  iooiinicc  46116  iooiinioc  46130  fsumnncl  46146  climinf  46180  climsuselem1  46181  sumnnodd  46204  lptre2pt  46212  addlimc  46220  0ellimcdiv  46221  limclner  46223  climleltrp  46248  liminfltlem  46376  fperdvper  46491  dvdivbd  46495  dvbdfbdioolem2  46501  dvbdfbdioo  46502  ioodvbdlimc1lem1  46503  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvxpaek  46512  dvnmul  46515  iblsplit  46538  iblspltprt  46545  itgspltprt  46551  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  stoweidlem1  46573  stoweidlem11  46583  stoweidlem13  46585  stoweidlem14  46586  stoweidlem20  46592  stoweidlem21  46593  stoweidlem26  46598  stoweidlem44  46616  stoweidlem60  46632  wallispilem3  46639  wallispilem4  46640  wallispilem5  46641  wallispi  46642  wallispi2lem1  46643  wallispi2lem2  46644  stirlinglem1  46646  stirlinglem3  46648  stirlinglem5  46650  stirlinglem6  46651  stirlinglem7  46652  stirlinglem10  46655  stirlinglem11  46656  stirlinglem12  46657  dirker2re  46664  dirkerval2  46666  dirkerre  46667  dirkerper  46668  dirkertrigeqlem1  46670  dirkertrigeqlem2  46671  dirkeritg  46674  dirkercncflem1  46675  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem4  46683  fourierdlem5  46684  fourierdlem6  46685  fourierdlem7  46686  fourierdlem9  46688  fourierdlem10  46689  fourierdlem18  46697  fourierdlem19  46698  fourierdlem20  46699  fourierdlem26  46705  fourierdlem28  46707  fourierdlem30  46709  fourierdlem35  46714  fourierdlem40  46719  fourierdlem41  46720  fourierdlem42  46721  fourierdlem47  46725  fourierdlem48  46726  fourierdlem49  46727  fourierdlem50  46728  fourierdlem51  46729  fourierdlem53  46731  fourierdlem57  46735  fourierdlem59  46737  fourierdlem60  46738  fourierdlem61  46739  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem66  46744  fourierdlem68  46746  fourierdlem71  46749  fourierdlem72  46750  fourierdlem74  46752  fourierdlem75  46753  fourierdlem76  46754  fourierdlem78  46756  fourierdlem79  46757  fourierdlem80  46758  fourierdlem81  46759  fourierdlem82  46760  fourierdlem83  46761  fourierdlem84  46762  fourierdlem87  46765  fourierdlem88  46766  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem92  46770  fourierdlem93  46771  fourierdlem94  46772  fourierdlem95  46773  fourierdlem97  46775  fourierdlem101  46779  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fourierdlem112  46790  fourierdlem113  46791  sqwvfoura  46800  sqwvfourb  46801  fouriersw  46803  qndenserrnbllem  46866  ioorrnopnlem  46876  ioorrnopnxrlem  46878  sge0xaddlem1  47005  sge0xaddlem2  47006  omeiunltfirp  47091  carageniuncllem2  47094  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem4  47170  hoiqssbllem1  47194  hoiqssbllem2  47195  hoiqssbllem3  47196  hspmbllem2  47199  hspmbllem3  47200  ovolval5lem1  47224  iinhoiicclem  47245  iinhoiicc  47246  iunhoiioolem  47247  iccvonmbllem  47250  vonioolem1  47252  vonioolem2  47253  vonicclem1  47255  vonicclem2  47256  preimaleiinlt  47293  salpreimaltle  47298  smfaddlem1  47335  smfadd  47337  smflimlem3  47345  smflimlem4  47346  smflimlem6  47348  smfmullem1  47363  smfmullem2  47364  smfmullem3  47365  ormkglobd  47449  zm1nn  47894  requad01  48241  requad1  48242  requad2  48243  perfectALTVlem2  48342  nnsum4primesevenALTV  48421  bgoldbtbndlem2  48426  gpgvtxedg0  48683  gpgvtxedg1  48684  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx13starlem2  48692  dignn0flhalflem1  49246  affinecomb1  49333  resum2sqcl  49337  2sphere  49380  line2  49383  itsclc0lem1  49387  itscnhlc0yqe  49390  itsclquadb  49407  2itscp  49412  itscnhlinecirc02plem1  49413  itscnhlinecirc02plem3  49415  itscnhlinecirc02p  49416  inlinecirc02plem  49417  amgmwlem  50431