Theorem readdcld 11138

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℝcr 11002   + caddc 11006

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

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

This theorem is referenced by:  ltadd2  11214  readdcan  11284  addrid  11290  leadd1  11582  le2add  11596  lesub2  11609  lesub3d  11732  le2addd  11733  supaddc  12086  supadd  12087  cju  12118  nnne0  12156  div4p1lem1div2  12373  difgtsumgt  12431  eluzmn  12736  rpnnen1lem5  12876  addlelt  13003  xralrple  13101  xov1plusxeqvd  13395  zltaddlt1le  13402  elincfzoext  13620  fladdz  13726  2tnp1ge0ge0  13730  flhalf  13731  fldiv  13761  modaddb  13810  modaddmodup  13838  modaddmodlo  13839  addmodlteq  13850  discr1  14143  discr  14144  ccatalpha  14498  2cshw  14717  remim  15021  remullem  15032  01sqrexlem7  15152  absrele  15212  abstri  15235  abs3lem  15243  amgm2  15274  bhmafibid1  15372  mulcn2  15500  o1add  15518  o1sub  15520  lo1add  15531  caucvgrlem  15577  iseraltlem2  15587  iseraltlem3  15588  fsumabs  15705  o1fsum  15717  climcndslem2  15754  tanhlt1  16066  eirrlem  16110  ruclem1  16137  ruclem2  16138  ruclem3  16139  ltoddhalfle  16269  bitscmp  16346  sadcaddlem  16365  sadasslem  16378  smuval2  16390  iserodd  16744  prmreclem4  16828  4sqlem5  16851  4sqlem6  16852  4sqlem12  16865  4sqlem15  16868  4sqlem16  16869  prmgaplem7  16966  prmgaplem8  16967  2expltfac  17001  cshwshashlem2  17005  chfacfscmul0  22771  chfacfscmulgsum  22773  chfacfpmmul0  22775  chfacfpmmulgsum  22777  prdsxmetlem  24281  xblss2ps  24314  metustexhalf  24469  nrmmetd  24487  ngptgp  24549  nlmvscnlem2  24598  nlmvscnlem1  24599  nmotri  24652  nghmplusg  24653  blcvx  24711  iccntr  24735  icccmplem2  24737  reconnlem2  24741  metdcnlem  24750  metnrmlem3  24775  cnllycmp  24880  lebnumii  24890  tcphcphlem1  25160  ipcnlem2  25169  ipcnlem1  25170  csbren  25324  trirn  25325  minveclem2  25351  minveclem3b  25353  minveclem4  25357  ivthlem2  25378  ovolgelb  25406  ovollb2lem  25414  ovolunlem1a  25422  ovolunlem1  25423  ovolfiniun  25427  ovoliunlem1  25428  ovoliunlem2  25429  ovolshftlem1  25435  ovolscalem1  25439  ovolicopnf  25450  ismbl2  25453  nulmbl2  25462  unmbl  25463  voliunlem2  25477  ioombl1lem2  25485  ioombl1lem4  25487  ioombl1  25488  ioorcl2  25498  uniioombllem1  25507  uniioombllem3  25511  uniioombllem4  25512  uniioombllem5  25513  uniioombl  25515  opnmbllem  25527  volcn  25532  itg1addlem4  25625  mbfi1fseqlem4  25644  mbfi1fseqlem6  25646  itg2splitlem  25674  itg2split  25675  itg2monolem3  25678  itg2addlem  25684  ibladdlem  25746  itgaddlem1  25749  itgaddlem2  25750  iblabslem  25754  iblabs  25755  dvferm1lem  25913  dvferm2lem  25915  dvlip2  25925  lhop1lem  25943  lhop1  25944  lhop  25946  dvcnvrelem1  25947  dvcnvrelem2  25948  dvcnvre  25949  dvcvx  25950  dvfsumlem3  25960  dvfsumlem4  25961  dvfsum2  25966  ftc1lem4  25971  coemullem  26180  ulmbdd  26332  ulmcn  26333  ulmdvlem1  26334  radcnvle  26354  pserdvlem1  26362  pserdv  26364  abelthlem7  26373  pilem2  26387  pilem3  26388  cosordlem  26464  abslogle  26552  logccv  26597  cxpaddle  26687  ang180lem2  26745  heron  26773  atanlogaddlem  26848  atans2  26866  cxp2limlem  26911  scvxcvx  26921  jensenlem2  26923  amgmlem  26925  logdiflbnd  26930  harmonicbnd4  26946  fsumharmonic  26947  lgamgulmlem3  26966  lgamgulmlem4  26967  lgamgulmlem5  26968  lgamgulmlem6  26969  lgambdd  26972  lgamucov  26973  regamcl  26996  ftalem5  27012  efnnfsumcl  27038  efchtdvds  27094  chtublem  27147  chtub  27148  logfaclbnd  27158  perfectlem2  27166  bposlem7  27226  bposlem9  27228  lgsdirprm  27267  gausslemma2dlem1a  27301  2sqlem8  27362  chpchtlim  27415  vmadivsumb  27419  rplogsumlem1  27420  dchrisumlem2  27426  dchrvmasumlem2  27434  dchrvmasumiflem1  27437  dchrisum0re  27449  dchrisum0lem1b  27451  mulog2sumlem1  27470  mulog2sumlem2  27471  logsqvma2  27479  log2sumbnd  27480  selberglem2  27482  selbergb  27485  selberg2b  27488  chpdifbndlem1  27489  chpdifbndlem2  27490  selberg3lem2  27494  selberg3  27495  selberg4lem1  27496  selberg4  27497  pntrsumbnd2  27503  selberg3r  27505  selberg34r  27507  pntsf  27509  pntrlog2bndlem1  27513  pntrlog2bndlem2  27514  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntrlog2bndlem6  27519  pntrlog2bnd  27520  pntpbnd1a  27521  pntpbnd2  27523  pntibndlem2a  27526  pntibndlem2  27527  pntibndlem3  27528  pntlemg  27534  pntlemr  27538  pntlemk  27542  pntlemo  27543  pntlem3  27545  abvcxp  27551  padicabv  27566  ostth2lem2  27570  ostth3  27574  brbtwn2  28881  axsegconlem8  28900  axsegconlem10  28902  axpaschlem  28916  axpasch  28917  axeuclidlem  28938  axcontlem2  28941  crctcshwlkn0lem3  29788  crctcshwlkn0lem5  29790  vacn  30669  smcnlem  30672  ubthlem2  30846  minvecolem2  30850  minvecolem3  30851  minvecolem4  30855  minvecolem5  30856  nmoptrii  32069  hstle  32205  staddi  32221  stadd3i  32223  lt2addrd  32729  nndiffz1  32764  nexple  32822  wrdt2ind  32929  cshwrnid  32937  fsumrp0cl  32997  pmtrto1cl  33063  fzto1st  33067  psgnfzto1st  33069  constrresqrtcl  33785  cos9thpiminplylem1  33790  1smat1  33812  sqsscirc1  33916  cnre2csqlem  33918  tpr2rico  33920  dya2iocress  34282  dya2iocbrsiga  34283  dya2icobrsiga  34284  dya2icoseg  34285  dya2iocucvr  34292  sxbrsigalem2  34294  omssubaddlem  34307  fibp1  34409  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemsgt1  34519  ballotlemsel1i  34521  plymulx0  34555  breprexplemc  34640  breprexp  34641  logdivsqrle  34658  resconn  35278  faclim  35778  dnizphlfeqhlf  36509  dnibndlem4  36514  dnibndlem6  36516  dnibndlem8  36518  dnibndlem9  36519  dnibndlem10  36520  dnibndlem11  36521  dnibndlem13  36523  dnibnd  36524  knoppcnlem4  36529  unblimceq0lem  36539  unblimceq0  36540  unbdqndv2lem1  36542  poimirlem29  37688  heicant  37694  opnmbllem0  37695  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  mbfposadd  37706  itg2addnclem  37710  itg2addnclem3  37712  itg2addnc  37713  itg2gt0cn  37714  ibladdnclem  37715  itgaddnclem1  37717  itgaddnclem2  37718  iblabsnclem  37722  iblabsnc  37723  iblmulc2nc  37724  ftc1cnnclem  37730  ftc1anclem4  37735  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  areacirclem5  37751  mettrifi  37796  isbnd3  37823  ssbnd  37827  cntotbnd  37835  heibor1lem  37848  bfplem2  37862  rrnequiv  37874  iccbnd  37879  lcmineqlem18  42078  lcmineqlem20  42080  aks4d1p1p3  42101  aks4d1p1p2  42102  aks4d1p1p4  42103  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1p5  42107  aks4d1p1  42108  posbezout  42132  aks6d1c1  42148  aks6d1c2  42162  2np3bcnp1  42176  2ap1caineq  42177  sticksstones6  42183  sticksstones7  42184  sticksstones10  42187  sticksstones12a  42189  sticksstones12  42190  sticksstones22  42200  bcle2d  42211  aks6d1c7lem1  42212  readdridaddlidd  42290  resubeulem1  42407  resubeulem2  42408  resubeu  42409  readdsub  42416  reladdrsub  42417  resubidaddlidlem  42426  renegid2  42446  sn-it0e0  42448  sn-0tie0  42483  sn-addlt0d  42490  sn-addgt0d  42491  cnreeu  42522  dffltz  42666  fltnltalem  42694  fltnlta  42695  3cubeslem1  42716  pellexlem2  42862  pell1qrge1  42902  pell14qrgapw  42908  pellqrexplicit  42909  pellqrex  42911  pellfundge  42914  pellfundgt1  42915  rmspecfund  42941  rmxycomplete  42949  ltrmynn0  42980  jm2.24nn  42991  jm2.24  42995  fzmaxdif  43013  jm2.26lem3  43033  jm3.1lem2  43050  areaquad  43248  sqrtcvallem4  43671  sqrtcvallem5  43672  sqrtcval  43673  imo72b2lem0  44197  hashnzfzclim  44354  binomcxplemnotnn0  44388  zltlesub  45325  lt3addmuld  45341  absnpncan2d  45342  fperiodmullem  45343  lt4addmuld  45346  absnpncan3d  45347  supxrgelem  45375  supxrge  45376  ltadd12dd  45381  xralrple2  45392  infxr  45404  infleinflem2  45408  xralrple4  45410  xralrple3  45411  xrralrecnnle  45420  eliooshift  45545  iccshift  45557  iooshift  45561  iooiinicc  45581  iooiinioc  45595  fsumnncl  45611  climinf  45645  climsuselem1  45646  sumnnodd  45669  lptre2pt  45677  addlimc  45685  0ellimcdiv  45686  limclner  45688  climleltrp  45713  liminfltlem  45841  fperdvper  45956  dvdivbd  45960  dvbdfbdioolem2  45966  dvbdfbdioo  45967  ioodvbdlimc1lem1  45968  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvxpaek  45977  dvnmul  45980  iblsplit  46003  iblspltprt  46010  itgspltprt  46016  itgiccshift  46017  itgperiod  46018  itgsbtaddcnst  46019  stoweidlem1  46038  stoweidlem11  46048  stoweidlem13  46050  stoweidlem14  46051  stoweidlem20  46057  stoweidlem21  46058  stoweidlem26  46063  stoweidlem44  46081  stoweidlem60  46097  wallispilem3  46104  wallispilem4  46105  wallispilem5  46106  wallispi  46107  wallispi2lem1  46108  wallispi2lem2  46109  stirlinglem1  46111  stirlinglem3  46113  stirlinglem5  46115  stirlinglem6  46116  stirlinglem7  46117  stirlinglem10  46120  stirlinglem11  46121  stirlinglem12  46122  dirker2re  46129  dirkerval2  46131  dirkerre  46132  dirkerper  46133  dirkertrigeqlem1  46135  dirkertrigeqlem2  46136  dirkeritg  46139  dirkercncflem1  46140  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem4  46148  fourierdlem5  46149  fourierdlem6  46150  fourierdlem7  46151  fourierdlem9  46153  fourierdlem10  46154  fourierdlem18  46162  fourierdlem19  46163  fourierdlem20  46164  fourierdlem26  46170  fourierdlem28  46172  fourierdlem30  46174  fourierdlem35  46179  fourierdlem40  46184  fourierdlem41  46185  fourierdlem42  46186  fourierdlem47  46190  fourierdlem48  46191  fourierdlem49  46192  fourierdlem50  46193  fourierdlem51  46194  fourierdlem53  46196  fourierdlem57  46200  fourierdlem59  46202  fourierdlem60  46203  fourierdlem61  46204  fourierdlem63  46206  fourierdlem64  46207  fourierdlem65  46208  fourierdlem66  46209  fourierdlem68  46211  fourierdlem71  46214  fourierdlem72  46215  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem78  46221  fourierdlem79  46222  fourierdlem80  46223  fourierdlem81  46224  fourierdlem82  46225  fourierdlem83  46226  fourierdlem84  46227  fourierdlem87  46230  fourierdlem88  46231  fourierdlem89  46232  fourierdlem90  46233  fourierdlem91  46234  fourierdlem92  46235  fourierdlem93  46236  fourierdlem94  46237  fourierdlem95  46238  fourierdlem97  46240  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem112  46255  fourierdlem113  46256  sqwvfoura  46265  sqwvfourb  46266  fouriersw  46268  qndenserrnbllem  46331  ioorrnopnlem  46341  ioorrnopnxrlem  46343  sge0xaddlem1  46470  sge0xaddlem2  46471  omeiunltfirp  46556  carageniuncllem2  46559  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hoiqssbllem1  46659  hoiqssbllem2  46660  hoiqssbllem3  46661  hspmbllem2  46664  hspmbllem3  46665  ovolval5lem1  46689  iinhoiicclem  46710  iinhoiicc  46711  iunhoiioolem  46712  iccvonmbllem  46715  vonioolem1  46717  vonioolem2  46718  vonicclem1  46720  vonicclem2  46721  preimaleiinlt  46758  salpreimaltle  46763  smfaddlem1  46800  smfadd  46802  smflimlem3  46810  smflimlem4  46811  smflimlem6  46813  smfmullem1  46828  smfmullem2  46829  smfmullem3  46830  ormkglobd  46912  zm1nn  47332  requad01  47651  requad1  47652  requad2  47653  perfectALTVlem2  47752  nnsum4primesevenALTV  47831  bgoldbtbndlem2  47836  gpgvtxedg0  48093  gpgvtxedg1  48094  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx13starlem2  48102  dignn0flhalflem1  48646  affinecomb1  48733  resum2sqcl  48737  2sphere  48780  line2  48783  itsclc0lem1  48787  itscnhlc0yqe  48790  itsclquadb  48807  2itscp  48812  itscnhlinecirc02plem1  48813  itscnhlinecirc02plem3  48815  itscnhlinecirc02p  48816  inlinecirc02plem  48817  amgmwlem  49833