Theorem readdcld 11209

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7389  ℝcr 11073   + caddc 11077

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

This theorem depends on definitions:  df-bi 207  df-an 396

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  12183  nnne0  12221  div4p1lem1div2  12443  difgtsumgt  12501  eluzmn  12806  rpnnen1lem5  12946  addlelt  13073  xralrple  13171  xov1plusxeqvd  13465  zltaddlt1le  13472  elincfzoext  13690  fladdz  13793  2tnp1ge0ge0  13797  flhalf  13798  fldiv  13828  modaddb  13877  modaddmodup  13905  modaddmodlo  13906  addmodlteq  13917  discr1  14210  discr  14211  ccatalpha  14564  2cshw  14784  remim  15089  remullem  15100  01sqrexlem7  15220  absrele  15280  abstri  15303  abs3lem  15311  amgm2  15342  bhmafibid1  15440  mulcn2  15568  o1add  15586  o1sub  15588  lo1add  15599  caucvgrlem  15645  iseraltlem2  15655  iseraltlem3  15656  fsumabs  15773  o1fsum  15785  climcndslem2  15822  tanhlt1  16134  eirrlem  16178  ruclem1  16205  ruclem2  16206  ruclem3  16207  ltoddhalfle  16337  bitscmp  16414  sadcaddlem  16433  sadasslem  16446  smuval2  16458  iserodd  16812  prmreclem4  16896  4sqlem5  16919  4sqlem6  16920  4sqlem12  16933  4sqlem15  16936  4sqlem16  16937  prmgaplem7  17034  prmgaplem8  17035  2expltfac  17069  cshwshashlem2  17073  chfacfscmul0  22751  chfacfscmulgsum  22753  chfacfpmmul0  22755  chfacfpmmulgsum  22757  prdsxmetlem  24262  xblss2ps  24295  metustexhalf  24450  nrmmetd  24468  ngptgp  24530  nlmvscnlem2  24579  nlmvscnlem1  24580  nmotri  24633  nghmplusg  24634  blcvx  24692  iccntr  24716  icccmplem2  24718  reconnlem2  24722  metdcnlem  24731  metnrmlem3  24756  cnllycmp  24861  lebnumii  24871  tcphcphlem1  25141  ipcnlem2  25150  ipcnlem1  25151  csbren  25305  trirn  25306  minveclem2  25332  minveclem3b  25334  minveclem4  25338  ivthlem2  25359  ovolgelb  25387  ovollb2lem  25395  ovolunlem1a  25403  ovolunlem1  25404  ovolfiniun  25408  ovoliunlem1  25409  ovoliunlem2  25410  ovolshftlem1  25416  ovolscalem1  25420  ovolicopnf  25431  ismbl2  25434  nulmbl2  25443  unmbl  25444  voliunlem2  25458  ioombl1lem2  25466  ioombl1lem4  25468  ioombl1  25469  ioorcl2  25479  uniioombllem1  25488  uniioombllem3  25492  uniioombllem4  25493  uniioombllem5  25494  uniioombl  25496  opnmbllem  25508  volcn  25513  itg1addlem4  25606  mbfi1fseqlem4  25625  mbfi1fseqlem6  25627  itg2splitlem  25655  itg2split  25656  itg2monolem3  25659  itg2addlem  25665  ibladdlem  25727  itgaddlem1  25730  itgaddlem2  25731  iblabslem  25735  iblabs  25736  dvferm1lem  25894  dvferm2lem  25896  dvlip2  25906  lhop1lem  25924  lhop1  25925  lhop  25927  dvcnvrelem1  25928  dvcnvrelem2  25929  dvcnvre  25930  dvcvx  25931  dvfsumlem3  25941  dvfsumlem4  25942  dvfsum2  25947  ftc1lem4  25952  coemullem  26161  ulmbdd  26313  ulmcn  26314  ulmdvlem1  26315  radcnvle  26335  pserdvlem1  26343  pserdv  26345  abelthlem7  26354  pilem2  26368  pilem3  26369  cosordlem  26445  abslogle  26533  logccv  26578  cxpaddle  26668  ang180lem2  26726  heron  26754  atanlogaddlem  26829  atans2  26847  cxp2limlem  26892  scvxcvx  26902  jensenlem2  26904  amgmlem  26906  logdiflbnd  26911  harmonicbnd4  26927  fsumharmonic  26928  lgamgulmlem3  26947  lgamgulmlem4  26948  lgamgulmlem5  26949  lgamgulmlem6  26950  lgambdd  26953  lgamucov  26954  regamcl  26977  ftalem5  26993  efnnfsumcl  27019  efchtdvds  27075  chtublem  27128  chtub  27129  logfaclbnd  27139  perfectlem2  27147  bposlem7  27207  bposlem9  27209  lgsdirprm  27248  gausslemma2dlem1a  27282  2sqlem8  27343  chpchtlim  27396  vmadivsumb  27400  rplogsumlem1  27401  dchrisumlem2  27407  dchrvmasumlem2  27415  dchrvmasumiflem1  27418  dchrisum0re  27430  dchrisum0lem1b  27432  mulog2sumlem1  27451  mulog2sumlem2  27452  logsqvma2  27460  log2sumbnd  27461  selberglem2  27463  selbergb  27466  selberg2b  27469  chpdifbndlem1  27470  chpdifbndlem2  27471  selberg3lem2  27475  selberg3  27476  selberg4lem1  27477  selberg4  27478  pntrsumbnd2  27484  selberg3r  27486  selberg34r  27488  pntsf  27490  pntrlog2bndlem1  27494  pntrlog2bndlem2  27495  pntrlog2bndlem4  27497  pntrlog2bndlem5  27498  pntrlog2bndlem6  27500  pntrlog2bnd  27501  pntpbnd1a  27502  pntpbnd2  27504  pntibndlem2a  27507  pntibndlem2  27508  pntibndlem3  27509  pntlemg  27515  pntlemr  27519  pntlemk  27523  pntlemo  27524  pntlem3  27526  abvcxp  27532  padicabv  27547  ostth2lem2  27551  ostth3  27555  brbtwn2  28838  axsegconlem8  28857  axsegconlem10  28859  axpaschlem  28873  axpasch  28874  axeuclidlem  28895  axcontlem2  28898  crctcshwlkn0lem3  29748  crctcshwlkn0lem5  29750  vacn  30629  smcnlem  30632  ubthlem2  30806  minvecolem2  30810  minvecolem3  30811  minvecolem4  30815  minvecolem5  30816  nmoptrii  32029  hstle  32165  staddi  32181  stadd3i  32183  lt2addrd  32680  nndiffz1  32715  nexple  32775  wrdt2ind  32881  cshwrnid  32889  fsumrp0cl  32968  pmtrto1cl  33062  fzto1st  33066  psgnfzto1st  33068  constrresqrtcl  33773  cos9thpiminplylem1  33778  1smat1  33800  sqsscirc1  33904  cnre2csqlem  33906  tpr2rico  33908  dya2iocress  34271  dya2iocbrsiga  34272  dya2icobrsiga  34273  dya2icoseg  34274  dya2iocucvr  34281  sxbrsigalem2  34283  omssubaddlem  34296  fibp1  34398  ballotlemfc0  34490  ballotlemfcc  34491  ballotlemsgt1  34508  ballotlemsel1i  34510  plymulx0  34544  breprexplemc  34629  breprexp  34630  logdivsqrle  34647  resconn  35233  faclim  35728  dnizphlfeqhlf  36459  dnibndlem4  36464  dnibndlem6  36466  dnibndlem8  36468  dnibndlem9  36469  dnibndlem10  36470  dnibndlem11  36471  dnibndlem13  36473  dnibnd  36474  knoppcnlem4  36479  unblimceq0lem  36489  unblimceq0  36490  unbdqndv2lem1  36492  poimirlem29  37638  heicant  37644  opnmbllem0  37645  mblfinlem3  37648  mblfinlem4  37649  ismblfin  37650  mbfposadd  37656  itg2addnclem  37660  itg2addnclem3  37662  itg2addnc  37663  itg2gt0cn  37664  ibladdnclem  37665  itgaddnclem1  37667  itgaddnclem2  37668  iblabsnclem  37672  iblabsnc  37673  iblmulc2nc  37674  ftc1cnnclem  37680  ftc1anclem4  37685  ftc1anclem7  37688  ftc1anclem8  37689  ftc1anc  37690  areacirclem5  37701  mettrifi  37746  isbnd3  37773  ssbnd  37777  cntotbnd  37785  heibor1lem  37798  bfplem2  37812  rrnequiv  37824  iccbnd  37829  lcmineqlem18  42029  lcmineqlem20  42031  aks4d1p1p3  42052  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p7  42057  aks4d1p1p5  42058  aks4d1p1  42059  posbezout  42083  aks6d1c1  42099  aks6d1c2  42113  2np3bcnp1  42127  2ap1caineq  42128  sticksstones6  42134  sticksstones7  42135  sticksstones10  42138  sticksstones12a  42140  sticksstones12  42141  sticksstones22  42151  bcle2d  42162  aks6d1c7lem1  42163  readdridaddlidd  42241  resubeulem1  42358  resubeulem2  42359  resubeu  42360  readdsub  42367  reladdrsub  42368  resubidaddlidlem  42377  renegid2  42397  sn-it0e0  42399  sn-0tie0  42434  sn-addlt0d  42441  sn-addgt0d  42442  cnreeu  42471  dffltz  42615  fltnltalem  42643  fltnlta  42644  3cubeslem1  42665  pellexlem2  42811  pell1qrge1  42851  pell14qrgapw  42857  pellqrexplicit  42858  pellqrex  42860  pellfundge  42863  pellfundgt1  42864  rmspecfund  42890  rmxycomplete  42899  ltrmynn0  42930  jm2.24nn  42941  jm2.24  42945  fzmaxdif  42963  jm2.26lem3  42983  jm3.1lem2  43000  areaquad  43198  sqrtcvallem4  43621  sqrtcvallem5  43622  sqrtcval  43623  imo72b2lem0  44147  hashnzfzclim  44304  binomcxplemnotnn0  44338  zltlesub  45276  lt3addmuld  45292  absnpncan2d  45293  fperiodmullem  45294  lt4addmuld  45297  absnpncan3d  45298  supxrgelem  45326  supxrge  45327  ltadd12dd  45332  xralrple2  45343  infxr  45356  infleinflem2  45360  xralrple4  45362  xralrple3  45363  xrralrecnnle  45372  eliooshift  45497  iccshift  45509  iooshift  45513  iooiinicc  45533  iooiinioc  45547  fsumnncl  45563  climinf  45597  climsuselem1  45598  sumnnodd  45621  lptre2pt  45631  addlimc  45639  0ellimcdiv  45640  limclner  45642  climleltrp  45667  liminfltlem  45795  fperdvper  45910  dvdivbd  45914  dvbdfbdioolem2  45920  dvbdfbdioo  45921  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvxpaek  45931  dvnmul  45934  iblsplit  45957  iblspltprt  45964  itgspltprt  45970  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  stoweidlem1  45992  stoweidlem11  46002  stoweidlem13  46004  stoweidlem14  46005  stoweidlem20  46011  stoweidlem21  46012  stoweidlem26  46017  stoweidlem44  46035  stoweidlem60  46051  wallispilem3  46058  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  wallispi2lem2  46063  stirlinglem1  46065  stirlinglem3  46067  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  stirlinglem12  46076  dirker2re  46083  dirkerval2  46085  dirkerre  46086  dirkerper  46087  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkeritg  46093  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem4  46102  fourierdlem5  46103  fourierdlem6  46104  fourierdlem7  46105  fourierdlem9  46107  fourierdlem10  46108  fourierdlem18  46116  fourierdlem19  46117  fourierdlem20  46118  fourierdlem26  46124  fourierdlem28  46126  fourierdlem30  46128  fourierdlem35  46133  fourierdlem40  46138  fourierdlem41  46139  fourierdlem42  46140  fourierdlem47  46144  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem51  46148  fourierdlem53  46150  fourierdlem57  46154  fourierdlem59  46156  fourierdlem60  46157  fourierdlem61  46158  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem66  46163  fourierdlem68  46165  fourierdlem71  46168  fourierdlem72  46169  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem79  46176  fourierdlem80  46177  fourierdlem81  46178  fourierdlem82  46179  fourierdlem83  46180  fourierdlem84  46181  fourierdlem87  46184  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem92  46189  fourierdlem93  46190  fourierdlem94  46191  fourierdlem95  46192  fourierdlem97  46194  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem112  46209  fourierdlem113  46210  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  qndenserrnbllem  46285  ioorrnopnlem  46295  ioorrnopnxrlem  46297  sge0xaddlem1  46424  sge0xaddlem2  46425  omeiunltfirp  46510  carageniuncllem2  46513  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  hoiqssbllem1  46613  hoiqssbllem2  46614  hoiqssbllem3  46615  hspmbllem2  46618  hspmbllem3  46619  ovolval5lem1  46643  iinhoiicclem  46664  iinhoiicc  46665  iunhoiioolem  46666  iccvonmbllem  46669  vonioolem1  46671  vonioolem2  46672  vonicclem1  46674  vonicclem2  46675  preimaleiinlt  46712  salpreimaltle  46717  smfaddlem1  46754  smfadd  46756  smflimlem3  46764  smflimlem4  46765  smflimlem6  46767  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  ormkglobd  46866  zm1nn  47293  requad01  47612  requad1  47613  requad2  47614  perfectALTVlem2  47713  nnsum4primesevenALTV  47792  bgoldbtbndlem2  47797  gpgvtxedg0  48044  gpgvtxedg1  48045  gpg5nbgrvtx03starlem2  48050  gpg5nbgrvtx13starlem2  48053  dignn0flhalflem1  48594  affinecomb1  48681  resum2sqcl  48685  2sphere  48728  line2  48731  itsclc0lem1  48735  itscnhlc0yqe  48738  itsclquadb  48755  2itscp  48760  itscnhlinecirc02plem1  48761  itscnhlinecirc02plem3  48763  itscnhlinecirc02p  48764  inlinecirc02plem  48765  amgmwlem  49781