Theorem readdcld 11239

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7412  ℝcr 11100   + caddc 11104

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

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

This theorem is referenced by:  ltadd2  11315  readdcan  11385  addrid  11391  leadd1  11683  le2add  11697  lesub2  11710  lesub3d  11833  le2addd  11834  supaddc  12183  supadd  12184  cju  12215  nnne0  12271  div4p1lem1div2  12500  difgtsumgt  12558  eluzmn  12870  rpnnen1lem5  13006  addlelt  13133  xralrple  13232  xov1plusxeqvd  13526  zltaddlt1le  13533  elincfzoext  13754  fladdz  13860  2tnp1ge0ge0  13864  flhalf  13865  fldiv  13895  modaddb  13944  modaddmodup  13972  modaddmodlo  13973  addmodlteq  13984  discr1  14277  discr  14278  ccatalpha  14633  2cshw  14852  remim  15170  remullem  15181  01sqrexlem7  15301  absrele  15361  abstri  15384  abs3lem  15392  amgm2  15423  bhmafibid1  15521  mulcn2  15649  o1add  15667  o1sub  15669  lo1add  15680  caucvgrlem  15726  iseraltlem2  15736  iseraltlem3  15737  fsumabs  15855  o1fsum  15867  climcndslem2  15906  tanhlt1  16217  eirrlem  16261  ruclem1  16288  ruclem2  16289  ruclem3  16290  ltoddhalfle  16420  bitscmp  16497  sadcaddlem  16516  sadasslem  16529  smuval2  16541  iserodd  16896  prmreclem4  16980  4sqlem5  17003  4sqlem6  17004  4sqlem12  17017  4sqlem15  17020  4sqlem16  17021  prmgaplem7  17118  prmgaplem8  17119  2expltfac  17153  cshwshashlem2  17157  chfacfscmul0  22996  chfacfscmulgsum  22998  chfacfpmmul0  23000  chfacfpmmulgsum  23002  prdsxmetlem  24506  xblss2ps  24539  metustexhalf  24694  nrmmetd  24712  ngptgp  24774  nlmvscnlem2  24823  nlmvscnlem1  24824  nmotri  24877  nghmplusg  24878  blcvx  24936  iccntr  24960  icccmplem2  24962  reconnlem2  24966  metdcnlem  24975  metnrmlem3  25000  cnllycmp  25096  lebnumii  25106  tcphcphlem1  25375  ipcnlem2  25384  ipcnlem1  25385  csbren  25539  trirn  25540  minveclem2  25566  minveclem3b  25568  minveclem4  25572  ivthlem2  25592  ovolgelb  25620  ovollb2lem  25628  ovolunlem1a  25636  ovolunlem1  25637  ovolfiniun  25641  ovoliunlem1  25642  ovoliunlem2  25643  ovolshftlem1  25649  ovolscalem1  25653  ovolicopnf  25664  ismbl2  25667  nulmbl2  25676  unmbl  25677  voliunlem2  25691  ioombl1lem2  25699  ioombl1lem4  25701  ioombl1  25702  ioorcl2  25712  uniioombllem1  25721  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  uniioombl  25729  opnmbllem  25741  volcn  25746  itg1addlem4  25839  mbfi1fseqlem4  25858  mbfi1fseqlem6  25860  itg2splitlem  25888  itg2split  25889  itg2monolem3  25892  itg2addlem  25898  ibladdlem  25960  itgaddlem1  25963  itgaddlem2  25964  iblabslem  25968  iblabs  25969  dvferm1lem  26124  dvferm2lem  26126  dvlip2  26135  lhop1lem  26153  lhop1  26154  lhop  26156  dvcnvrelem1  26157  dvcnvrelem2  26158  dvcnvre  26159  dvcvx  26160  dvfsumlem3  26168  dvfsumlem4  26169  dvfsum2  26174  ftc1lem4  26179  coemullem  26388  plyn0mulidp  26423  ulmbdd  26539  ulmcn  26540  ulmdvlem1  26541  radcnvle  26561  pserdvlem1  26568  pserdv  26570  abelthlem7  26579  pilem2  26593  pilem3  26594  cosordlem  26673  abslogle  26761  logccv  26806  cxpaddle  26895  ang180lem2  26953  heron  26981  atanlogaddlem  27056  atans2  27074  cxp2limlem  27118  scvxcvx  27128  jensenlem2  27130  amgmlem  27132  logdiflbnd  27137  harmonicbnd4  27153  fsumharmonic  27154  lgamgulmlem3  27173  lgamgulmlem4  27174  lgamgulmlem5  27175  lgamgulmlem6  27176  lgambdd  27179  lgamucov  27180  regamcl  27203  ftalem5  27219  efnnfsumcl  27245  efchtdvds  27301  chtublem  27353  chtub  27354  logfaclbnd  27364  perfectlem2  27372  bposlem7  27432  bposlem9  27434  lgsdirprm  27473  gausslemma2dlem1a  27507  2sqlem8  27568  chpchtlim  27621  vmadivsumb  27625  rplogsumlem1  27626  dchrisumlem2  27632  dchrvmasumlem2  27640  dchrvmasumiflem1  27643  dchrisum0re  27655  dchrisum0lem1b  27657  mulog2sumlem1  27676  mulog2sumlem2  27677  logsqvma2  27685  log2sumbnd  27686  selberglem2  27688  selbergb  27691  selberg2b  27694  chpdifbndlem1  27695  chpdifbndlem2  27696  selberg3lem2  27700  selberg3  27701  selberg4lem1  27702  selberg4  27703  pntrsumbnd2  27709  selberg3r  27711  selberg34r  27713  pntsf  27715  pntrlog2bndlem1  27719  pntrlog2bndlem2  27720  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntrlog2bndlem6  27725  pntrlog2bnd  27726  pntpbnd1a  27727  pntpbnd2  27729  pntibndlem2a  27732  pntibndlem2  27733  pntibndlem3  27734  pntlemg  27740  pntlemr  27744  pntlemk  27748  pntlemo  27749  pntlem3  27751  abvcxp  27757  padicabv  27772  ostth2lem2  27776  ostth3  27780  brbtwn2  29233  axsegconlem8  29252  axsegconlem10  29254  axpaschlem  29268  axpasch  29269  axeuclidlem  29290  axcontlem2  29293  crctcshwlkn0lem3  30139  crctcshwlkn0lem5  30141  vacn  31024  smcnlem  31027  ubthlem2  31201  minvecolem2  31205  minvecolem3  31206  minvecolem4  31210  minvecolem5  31211  nmoptrii  32424  hstle  32560  staddi  32576  stadd3i  32578  lt2addrd  33073  nndiffz1  33109  nexple  33155  wrdt2ind  33251  cshwrnid  33259  fsumrp0cl  33319  pmtrto1cl  33397  fzto1st  33401  psgnfzto1st  33403  constrresqrtcl  34145  cos9thpiminplylem1  34150  1smat1  34172  sqsscirc1  34276  cnre2csqlem  34278  tpr2rico  34280  dya2iocress  34642  dya2iocbrsiga  34643  dya2icobrsiga  34644  dya2icoseg  34645  dya2iocucvr  34652  sxbrsigalem2  34654  omssubaddlem  34667  fibp1  34769  ballotlemfc0  34861  ballotlemfcc  34862  ballotlemsgt1  34879  ballotlemsel1i  34881  breprexplemc  34997  breprexp  34998  logdivsqrle  35015  resconn  35716  faclim  36216  dnizphlfeqhlf  37043  dnibndlem4  37048  dnibndlem6  37050  dnibndlem8  37052  dnibndlem9  37053  dnibndlem10  37054  dnibndlem11  37055  dnibndlem13  37057  dnibnd  37058  knoppcnlem4  37063  unblimceq0lem  37073  unblimceq0  37074  unbdqndv2lem1  37076  poimirlem29  38278  heicant  38284  opnmbllem0  38285  mblfinlem3  38288  mblfinlem4  38289  ismblfin  38290  mbfposadd  38296  itg2addnclem  38300  itg2addnclem3  38302  itg2addnc  38303  itg2gt0cn  38304  ibladdnclem  38305  itgaddnclem1  38307  itgaddnclem2  38308  iblabsnclem  38312  iblabsnc  38313  iblmulc2nc  38314  ftc1cnnclem  38320  ftc1anclem4  38325  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  areacirclem5  38341  mettrifi  38386  isbnd3  38413  ssbnd  38417  cntotbnd  38425  heibor1lem  38438  bfplem2  38452  rrnequiv  38464  iccbnd  38469  lcmineqlem18  42791  lcmineqlem20  42793  aks4d1p1p3  42814  aks4d1p1p2  42815  aks4d1p1p4  42816  aks4d1p1p6  42818  aks4d1p1p7  42819  aks4d1p1p5  42820  aks4d1p1  42821  posbezout  42845  aks6d1c1  42861  aks6d1c2  42875  2np3bcnp1  42889  2ap1caineq  42890  sticksstones6  42896  sticksstones7  42897  sticksstones10  42900  sticksstones12a  42902  sticksstones12  42903  sticksstones22  42913  bcle2d  42924  aks6d1c7lem1  42925  readdridaddlidd  43003  resubeulem1  43114  resubeulem2  43115  resubeu  43116  readdsub  43123  reladdrsub  43124  resubidaddlidlem  43133  renegid2  43153  sn-it0e0  43155  redivdird  43201  sn-0tie0  43203  sn-addlt0d  43210  sn-addgt0d  43211  cnreeu  43242  dffltz  43346  fltnltalem  43374  fltnlta  43375  3cubeslem1  43395  pellexlem2  43537  pell1qrge1  43577  pell14qrgapw  43583  pellqrexplicit  43584  pellqrex  43586  pellfundge  43589  pellfundgt1  43590  rmspecfund  43616  rmxycomplete  43624  ltrmynn0  43655  jm2.24nn  43666  jm2.24  43670  fzmaxdif  43688  jm2.26lem3  43708  jm3.1lem2  43725  areaquad  43923  sqrtcvallem4  44345  sqrtcvallem5  44346  sqrtcval  44347  imo72b2lem0  44871  hashnzfzclim  45012  binomcxplemnotnn0  45046  zltlesub  45984  lt3addmuld  46000  absnpncan2d  46001  fperiodmullem  46002  lt4addmuld  46005  absnpncan3d  46006  supxrgelem  46033  supxrge  46034  ltadd12dd  46039  xralrple2  46050  infxr  46062  infleinflem2  46066  xralrple4  46068  xralrple3  46069  xrralrecnnle  46078  eliooshift  46202  iccshift  46214  iooshift  46218  iooiinicc  46238  iooiinioc  46252  fsumnncl  46268  climinf  46302  climsuselem1  46303  sumnnodd  46326  lptre2pt  46334  addlimc  46342  0ellimcdiv  46343  limclner  46345  climleltrp  46370  liminfltlem  46498  fperdvper  46613  dvdivbd  46617  dvbdfbdioolem2  46623  dvbdfbdioo  46624  ioodvbdlimc1lem1  46625  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvxpaek  46634  dvnmul  46637  iblsplit  46660  iblspltprt  46667  itgspltprt  46673  itgiccshift  46674  itgperiod  46675  itgsbtaddcnst  46676  stoweidlem1  46695  stoweidlem11  46705  stoweidlem13  46707  stoweidlem14  46708  stoweidlem20  46714  stoweidlem21  46715  stoweidlem26  46720  stoweidlem44  46738  stoweidlem60  46754  wallispilem3  46761  wallispilem4  46762  wallispilem5  46763  wallispi  46764  wallispi2lem1  46765  wallispi2lem2  46766  stirlinglem1  46768  stirlinglem3  46770  stirlinglem5  46772  stirlinglem6  46773  stirlinglem7  46774  stirlinglem10  46777  stirlinglem11  46778  stirlinglem12  46779  dirker2re  46786  dirkerval2  46788  dirkerre  46789  dirkerper  46790  dirkertrigeqlem1  46792  dirkertrigeqlem2  46793  dirkeritg  46796  dirkercncflem1  46797  dirkercncflem2  46798  dirkercncflem4  46800  fourierdlem4  46805  fourierdlem5  46806  fourierdlem6  46807  fourierdlem7  46808  fourierdlem9  46810  fourierdlem10  46811  fourierdlem18  46819  fourierdlem19  46820  fourierdlem20  46821  fourierdlem26  46827  fourierdlem28  46829  fourierdlem30  46831  fourierdlem35  46836  fourierdlem40  46841  fourierdlem41  46842  fourierdlem42  46843  fourierdlem47  46847  fourierdlem48  46848  fourierdlem49  46849  fourierdlem50  46850  fourierdlem51  46851  fourierdlem53  46853  fourierdlem57  46857  fourierdlem59  46859  fourierdlem60  46860  fourierdlem61  46861  fourierdlem63  46863  fourierdlem64  46864  fourierdlem65  46865  fourierdlem66  46866  fourierdlem68  46868  fourierdlem71  46871  fourierdlem72  46872  fourierdlem74  46874  fourierdlem75  46875  fourierdlem76  46876  fourierdlem78  46878  fourierdlem79  46879  fourierdlem80  46880  fourierdlem81  46881  fourierdlem82  46882  fourierdlem83  46883  fourierdlem84  46884  fourierdlem87  46887  fourierdlem88  46888  fourierdlem89  46889  fourierdlem90  46890  fourierdlem91  46891  fourierdlem92  46892  fourierdlem93  46893  fourierdlem94  46894  fourierdlem95  46895  fourierdlem97  46897  fourierdlem101  46901  fourierdlem103  46903  fourierdlem104  46904  fourierdlem111  46911  fourierdlem112  46912  fourierdlem113  46913  sqwvfoura  46922  sqwvfourb  46923  fouriersw  46925  qndenserrnbllem  46988  ioorrnopnlem  46998  ioorrnopnxrlem  47000  sge0xaddlem1  47127  sge0xaddlem2  47128  omeiunltfirp  47213  carageniuncllem2  47216  hoidmv1lelem1  47285  hoidmv1lelem2  47286  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  hoidmvlelem4  47292  hoiqssbllem1  47316  hoiqssbllem2  47317  hoiqssbllem3  47318  hspmbllem2  47321  hspmbllem3  47322  ovolval5lem1  47346  iinhoiicclem  47367  iinhoiicc  47368  iunhoiioolem  47369  iccvonmbllem  47372  vonioolem1  47374  vonioolem2  47375  vonicclem1  47377  vonicclem2  47378  preimaleiinlt  47415  salpreimaltle  47420  smfaddlem1  47457  smfadd  47459  smflimlem3  47467  smflimlem4  47468  smflimlem6  47470  smfmullem1  47485  smfmullem2  47486  smfmullem3  47487  ormkglobd  47571  zm1nn  48016  requad01  48363  requad1  48364  requad2  48365  perfectALTVlem2  48464  nnsum4primesevenALTV  48543  bgoldbtbndlem2  48548  gpgvtxedg0  48805  gpgvtxedg1  48806  gpg5nbgrvtx03starlem2  48811  gpg5nbgrvtx13starlem2  48814  dignn0flhalflem1  49372  affinecomb1  49459  resum2sqcl  49463  2sphere  49506  line2  49509  itsclc0lem1  49513  itscnhlc0yqe  49516  itsclquadb  49533  2itscp  49538  itscnhlinecirc02plem1  49539  itscnhlinecirc02plem3  49541  itscnhlinecirc02p  49542  inlinecirc02plem  49543  amgmwlem  50579