Theorem readdcld 11266

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7417  ℝcr 11127   + caddc 11131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11189

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ltadd2  11342  readdcan  11412  addrid  11418  leadd1  11710  le2add  11724  lesub2  11737  lesub3d  11860  le2addd  11861  supaddc  12210  supadd  12211  cju  12242  nnne0  12298  div4p1lem1div2  12527  difgtsumgt  12585  eluzmn  12898  rpnnen1lem5  13035  addlelt  13162  xralrple  13261  xov1plusxeqvd  13555  zltaddlt1le  13562  elincfzoext  13783  fladdz  13890  2tnp1ge0ge0  13894  flhalf  13895  fldiv  13925  modaddb  13974  modaddmodup  14002  modaddmodlo  14003  addmodlteq  14014  discr1  14307  discr  14308  ccatalpha  14664  2cshw  14888  remim  15208  remullem  15219  01sqrexlem7  15339  absrele  15399  abstri  15422  abs3lem  15430  amgm2  15461  bhmafibid1  15559  mulcn2  15687  o1add  15705  o1sub  15707  lo1add  15718  caucvgrlem  15764  iseraltlem2  15774  iseraltlem3  15775  fsumabs  15892  o1fsum  15904  climcndslem2  15943  tanhlt1  16254  eirrlem  16298  ruclem1  16325  ruclem2  16326  ruclem3  16327  ltoddhalfle  16457  bitscmp  16534  sadcaddlem  16553  sadasslem  16566  smuval2  16578  iserodd  16933  prmreclem4  17017  4sqlem5  17040  4sqlem6  17041  4sqlem12  17054  4sqlem15  17057  4sqlem16  17058  prmgaplem7  17155  prmgaplem8  17156  2expltfac  17190  cshwshashlem2  17194  chfacfscmul0  23089  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulgsum  23095  prdsxmetlem  24600  xblss2ps  24633  metustexhalf  24788  nrmmetd  24806  ngptgp  24868  nlmvscnlem2  24917  nlmvscnlem1  24918  nmotri  24971  nghmplusg  24972  blcvx  25030  iccntr  25054  icccmplem2  25056  reconnlem2  25060  metdcnlem  25069  metnrmlem3  25094  cnllycmp  25190  lebnumii  25200  tcphcphlem1  25469  ipcnlem2  25478  ipcnlem1  25479  csbren  25633  trirn  25634  minveclem2  25660  minveclem3b  25662  minveclem4  25666  ivthlem2  25686  ovolgelb  25714  ovollb2lem  25722  ovolunlem1a  25730  ovolunlem1  25731  ovolfiniun  25735  ovoliunlem1  25736  ovoliunlem2  25737  ovolshftlem1  25743  ovolscalem1  25747  ovolicopnf  25758  ismbl2  25761  nulmbl2  25770  unmbl  25771  voliunlem2  25785  ioombl1lem2  25793  ioombl1lem4  25795  ioombl1  25796  ioorcl2  25806  uniioombllem1  25815  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  uniioombl  25823  opnmbllem  25835  volcn  25840  itg1addlem4  25933  mbfi1fseqlem4  25952  mbfi1fseqlem6  25954  itg2splitlem  25982  itg2split  25983  itg2monolem3  25986  itg2addlem  25992  ibladdlem  26054  itgaddlem1  26057  itgaddlem2  26058  iblabslem  26062  iblabs  26063  dvferm1lem  26218  dvferm2lem  26220  dvlip2  26229  lhop1lem  26247  lhop1  26248  lhop  26250  dvcnvrelem1  26251  dvcnvrelem2  26252  dvcnvre  26253  dvcvx  26254  dvfsumlem3  26262  dvfsumlem4  26263  dvfsum2  26268  ftc1lem4  26273  coemullem  26483  plyn0mulidp  26518  ulmbdd  26641  ulmcn  26642  ulmdvlem1  26643  radcnvle  26663  pserdvlem1  26670  pserdv  26672  abelthlem7  26681  pilem2  26695  pilem3  26696  cosordlem  26775  abslogle  26863  logccv  26908  cxpaddle  26997  ang180lem2  27055  heron  27083  atanlogaddlem  27158  atans2  27176  cxp2limlem  27220  scvxcvx  27230  jensenlem2  27232  amgmlem  27234  logdiflbnd  27239  harmonicbnd4  27255  fsumharmonic  27256  lgamgulmlem3  27275  lgamgulmlem4  27276  lgamgulmlem5  27277  lgamgulmlem6  27278  lgambdd  27281  lgamucov  27282  regamcl  27305  ftalem5  27321  efnnfsumcl  27347  efchtdvds  27403  chtublem  27455  chtub  27456  logfaclbnd  27466  perfectlem2  27474  bposlem7  27534  bposlem9  27536  lgsdirprm  27575  gausslemma2dlem1a  27609  2sqlem8  27670  chpchtlim  27723  vmadivsumb  27727  rplogsumlem1  27728  dchrisumlem2  27734  dchrvmasumlem2  27742  dchrvmasumiflem1  27745  dchrisum0re  27757  dchrisum0lem1b  27759  mulog2sumlem1  27778  mulog2sumlem2  27779  logsqvma2  27787  log2sumbnd  27788  selberglem2  27790  selbergb  27793  selberg2b  27796  chpdifbndlem1  27797  chpdifbndlem2  27798  selberg3lem2  27802  selberg3  27803  selberg4lem1  27804  selberg4  27805  pntrsumbnd2  27811  selberg3r  27813  selberg34r  27815  pntsf  27817  pntrlog2bndlem1  27821  pntrlog2bndlem2  27822  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntrlog2bndlem6  27827  pntrlog2bnd  27828  pntpbnd1a  27829  pntpbnd2  27831  pntibndlem2a  27834  pntibndlem2  27835  pntibndlem3  27836  pntlemg  27842  pntlemr  27846  pntlemk  27850  pntlemo  27851  pntlem3  27853  abvcxp  27859  padicabv  27874  ostth2lem2  27878  ostth3  27882  brbtwn2  29370  axsegconlem8  29389  axsegconlem10  29391  axpaschlem  29405  axpasch  29406  axeuclidlem  29427  axcontlem2  29430  crctcshwlkn0lem3  30288  crctcshwlkn0lem5  30290  vacn  31183  smcnlem  31186  ubthlem2  31360  minvecolem2  31364  minvecolem3  31365  minvecolem4  31369  minvecolem5  31370  nmoptrii  32583  hstle  32719  staddi  32735  stadd3i  32737  lt2addrd  33229  nndiffz1  33265  nexple  33311  wrdt2ind  33403  cshwrnid  33409  fsumrp0cl  33469  pmtrto1cl  33547  fzto1st  33551  psgnfzto1st  33553  constrresqrtcl  34295  cos9thpiminplylem1  34300  1smat1  34322  sqsscirc1  34426  cnre2csqlem  34428  tpr2rico  34430  dya2iocress  34793  dya2iocbrsiga  34794  dya2icobrsiga  34795  dya2icoseg  34796  dya2iocucvr  34803  sxbrsigalem2  34805  omssubaddlem  34818  fibp1  34920  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemsgt1  35030  ballotlemsel1i  35032  breprexplemc  35148  breprexp  35149  logdivsqrle  35166  resconn  35833  faclim  36333  dnizphlfeqhlf  37181  dnibndlem4  37186  dnibndlem6  37188  dnibndlem8  37190  dnibndlem9  37191  dnibndlem10  37192  dnibndlem11  37193  dnibndlem13  37195  dnibnd  37196  knoppcnlem4  37201  unblimceq0lem  37211  unblimceq0  37212  unbdqndv2lem1  37214  poimirlem29  38406  heicant  38412  opnmbllem0  38413  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  mbfposadd  38424  itg2addnclem  38428  itg2addnclem3  38430  itg2addnc  38431  itg2gt0cn  38432  ibladdnclem  38433  itgaddnclem1  38435  itgaddnclem2  38436  iblabsnclem  38440  iblabsnc  38441  iblmulc2nc  38442  ftc1cnnclem  38448  ftc1anclem4  38453  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  areacirclem5  38469  mettrifi  38515  isbnd3  38542  ssbnd  38546  cntotbnd  38554  heibor1lem  38567  bfplem2  38581  rrnequiv  38593  iccbnd  38598  lcmineqlem18  42920  lcmineqlem20  42922  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1p6  42947  aks4d1p1p7  42948  aks4d1p1p5  42949  aks4d1p1  42950  posbezout  42974  aks6d1c1  42990  aks6d1c2  43004  2np3bcnp1  43018  2ap1caineq  43019  sticksstones6  43025  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  sticksstones22  43042  bcle2d  43053  aks6d1c7lem1  43054  readdridaddlidd  43132  resubeulem1  43258  resubeulem2  43259  resubeu  43260  readdsub  43267  reladdrsub  43268  resubidaddlidlem  43277  renegid2  43297  sn-it0e0  43299  redivdird  43345  sn-0tie0  43347  sn-addlt0d  43354  sn-addgt0d  43355  cnreeu  43386  dffltz  43488  fltnltalem  43516  fltnlta  43517  3cubeslem1  43537  pellexlem2  43679  pell1qrge1  43719  pell14qrgapw  43725  pellqrexplicit  43726  pellqrex  43728  pellfundge  43731  pellfundgt1  43732  rmspecfund  43758  rmxycomplete  43766  ltrmynn0  43797  jm2.24nn  43808  jm2.24  43812  fzmaxdif  43830  jm2.26lem3  43850  jm3.1lem2  43867  areaquad  44065  sqrtcvallem4  44487  sqrtcvallem5  44488  sqrtcval  44489  imo72b2lem0  45013  hashnzfzclim  45154  binomcxplemnotnn0  45188  zltlesub  46126  lt3addmuld  46142  absnpncan2d  46143  fperiodmullem  46144  lt4addmuld  46147  absnpncan3d  46148  supxrgelem  46175  supxrge  46176  ltadd12dd  46181  xralrple2  46192  infxr  46204  infleinflem2  46208  xralrple4  46210  xralrple3  46211  xrralrecnnle  46220  eliooshift  46344  iccshift  46356  iooshift  46360  iooiinicc  46380  iooiinioc  46394  fsumnncl  46410  climinf  46444  climsuselem1  46445  sumnnodd  46468  lptre2pt  46476  addlimc  46484  0ellimcdiv  46485  limclner  46487  climleltrp  46512  liminfltlem  46640  fperdvper  46755  dvdivbd  46759  dvbdfbdioolem2  46765  dvbdfbdioo  46766  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvxpaek  46776  dvnmul  46779  iblsplit  46802  iblspltprt  46809  itgspltprt  46815  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  stoweidlem1  46837  stoweidlem11  46847  stoweidlem13  46849  stoweidlem14  46850  stoweidlem20  46856  stoweidlem21  46857  stoweidlem26  46862  stoweidlem44  46880  stoweidlem60  46896  wallispilem3  46903  wallispilem4  46904  wallispilem5  46905  wallispi  46906  wallispi2lem1  46907  wallispi2lem2  46908  stirlinglem1  46910  stirlinglem3  46912  stirlinglem5  46914  stirlinglem6  46915  stirlinglem7  46916  stirlinglem10  46919  stirlinglem11  46920  stirlinglem12  46921  dirker2re  46928  dirkerval2  46930  dirkerre  46931  dirkerper  46932  dirkertrigeqlem1  46934  dirkertrigeqlem2  46935  dirkeritg  46938  dirkercncflem1  46939  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem4  46947  fourierdlem5  46948  fourierdlem6  46949  fourierdlem7  46950  fourierdlem9  46952  fourierdlem10  46953  fourierdlem18  46961  fourierdlem19  46962  fourierdlem20  46963  fourierdlem26  46969  fourierdlem28  46971  fourierdlem30  46973  fourierdlem35  46978  fourierdlem40  46983  fourierdlem41  46984  fourierdlem42  46985  fourierdlem47  46989  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem53  46995  fourierdlem57  46999  fourierdlem59  47001  fourierdlem60  47002  fourierdlem61  47003  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem66  47008  fourierdlem68  47010  fourierdlem71  47013  fourierdlem72  47014  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem78  47020  fourierdlem79  47021  fourierdlem80  47022  fourierdlem81  47023  fourierdlem82  47024  fourierdlem83  47025  fourierdlem84  47026  fourierdlem87  47029  fourierdlem88  47030  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem92  47034  fourierdlem93  47035  fourierdlem94  47036  fourierdlem95  47037  fourierdlem97  47039  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  sqwvfoura  47064  sqwvfourb  47065  fouriersw  47067  qndenserrnbllem  47130  ioorrnopnlem  47140  ioorrnopnxrlem  47142  sge0xaddlem1  47269  sge0xaddlem2  47270  omeiunltfirp  47355  carageniuncllem2  47358  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  hoiqssbllem1  47458  hoiqssbllem2  47459  hoiqssbllem3  47460  hspmbllem2  47463  hspmbllem3  47464  ovolval5lem1  47488  iinhoiicclem  47509  iinhoiicc  47510  iunhoiioolem  47511  iccvonmbllem  47514  vonioolem1  47516  vonioolem2  47517  vonicclem1  47519  vonicclem2  47520  preimaleiinlt  47557  salpreimaltle  47562  smfaddlem1  47599  smfadd  47601  smflimlem3  47609  smflimlem4  47610  smflimlem6  47612  smfmullem1  47627  smfmullem2  47628  smfmullem3  47629  ormkglobd  47713  zm1nn  48198  requad01  48545  requad1  48546  requad2  48547  perfectALTVlem2  48646  nnsum4primesevenALTV  48725  bgoldbtbndlem2  48730  gpgvtxedg0  48987  gpgvtxedg1  48988  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx13starlem2  48996  dignn0flhalflem1  49553  affinecomb1  49640  resum2sqcl  49644  2sphere  49687  line2  49690  itsclc0lem1  49694  itscnhlc0yqe  49697  itsclquadb  49714  2itscp  49719  itscnhlinecirc02plem1  49720  itscnhlinecirc02plem3  49722  itscnhlinecirc02p  49723  inlinecirc02plem  49724  crossp3d  50808  veronesefvcl  50813  veronesev1lem  50814  veronesev2lem  50815  veronesev3lem  50816  veronesev4lem  50817  veronesev5lem  50818  veronesev6lem  50819  amgmwlem  50828