Theorem readdcld 11256

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7423  ℝcr 11117   + caddc 11121

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

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

This theorem is used by:  ltadd2  11332  readdcan  11402  addrid  11408  leadd1  11700  le2add  11714  lesub2  11727  lesub3d  11850  le2addd  11851  supaddc  12200  supadd  12201  cju  12232  nnne0  12288  div4p1lem1div2  12517  difgtsumgt  12575  eluzmn  12887  rpnnen1lem5  13023  addlelt  13150  xralrple  13249  xov1plusxeqvd  13543  zltaddlt1le  13550  elincfzoext  13771  fladdz  13878  2tnp1ge0ge0  13882  flhalf  13883  fldiv  13913  modaddb  13962  modaddmodup  13990  modaddmodlo  13991  addmodlteq  14002  discr1  14295  discr  14296  ccatalpha  14652  2cshw  14876  remim  15194  remullem  15205  01sqrexlem7  15325  absrele  15385  abstri  15408  abs3lem  15416  amgm2  15447  bhmafibid1  15545  mulcn2  15673  o1add  15691  o1sub  15693  lo1add  15704  caucvgrlem  15750  iseraltlem2  15760  iseraltlem3  15761  fsumabs  15879  o1fsum  15891  climcndslem2  15930  tanhlt1  16241  eirrlem  16285  ruclem1  16312  ruclem2  16313  ruclem3  16314  ltoddhalfle  16444  bitscmp  16521  sadcaddlem  16540  sadasslem  16553  smuval2  16565  iserodd  16920  prmreclem4  17004  4sqlem5  17027  4sqlem6  17028  4sqlem12  17041  4sqlem15  17044  4sqlem16  17045  prmgaplem7  17142  prmgaplem8  17143  2expltfac  17177  cshwshashlem2  17181  chfacfscmul0  23052  chfacfscmulgsum  23054  chfacfpmmul0  23056  chfacfpmmulgsum  23058  prdsxmetlem  24562  xblss2ps  24595  metustexhalf  24750  nrmmetd  24768  ngptgp  24830  nlmvscnlem2  24879  nlmvscnlem1  24880  nmotri  24933  nghmplusg  24934  blcvx  24992  iccntr  25016  icccmplem2  25018  reconnlem2  25022  metdcnlem  25031  metnrmlem3  25056  cnllycmp  25152  lebnumii  25162  tcphcphlem1  25431  ipcnlem2  25440  ipcnlem1  25441  csbren  25595  trirn  25596  minveclem2  25622  minveclem3b  25624  minveclem4  25628  ivthlem2  25648  ovolgelb  25676  ovollb2lem  25684  ovolunlem1a  25692  ovolunlem1  25693  ovolfiniun  25697  ovoliunlem1  25698  ovoliunlem2  25699  ovolshftlem1  25705  ovolscalem1  25709  ovolicopnf  25720  ismbl2  25723  nulmbl2  25732  unmbl  25733  voliunlem2  25747  ioombl1lem2  25755  ioombl1lem4  25757  ioombl1  25758  ioorcl2  25768  uniioombllem1  25777  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  uniioombl  25785  opnmbllem  25797  volcn  25802  itg1addlem4  25895  mbfi1fseqlem4  25914  mbfi1fseqlem6  25916  itg2splitlem  25944  itg2split  25945  itg2monolem3  25948  itg2addlem  25954  ibladdlem  26016  itgaddlem1  26019  itgaddlem2  26020  iblabslem  26024  iblabs  26025  dvferm1lem  26180  dvferm2lem  26182  dvlip2  26191  lhop1lem  26209  lhop1  26210  lhop  26212  dvcnvrelem1  26213  dvcnvrelem2  26214  dvcnvre  26215  dvcvx  26216  dvfsumlem3  26224  dvfsumlem4  26225  dvfsum2  26230  ftc1lem4  26235  coemullem  26444  plyn0mulidp  26479  ulmbdd  26598  ulmcn  26599  ulmdvlem1  26600  radcnvle  26620  pserdvlem1  26627  pserdv  26629  abelthlem7  26638  pilem2  26652  pilem3  26653  cosordlem  26732  abslogle  26820  logccv  26865  cxpaddle  26954  ang180lem2  27012  heron  27040  atanlogaddlem  27115  atans2  27133  cxp2limlem  27177  scvxcvx  27187  jensenlem2  27189  amgmlem  27191  logdiflbnd  27196  harmonicbnd4  27212  fsumharmonic  27213  lgamgulmlem3  27232  lgamgulmlem4  27233  lgamgulmlem5  27234  lgamgulmlem6  27235  lgambdd  27238  lgamucov  27239  regamcl  27262  ftalem5  27278  efnnfsumcl  27304  efchtdvds  27360  chtublem  27412  chtub  27413  logfaclbnd  27423  perfectlem2  27431  bposlem7  27491  bposlem9  27493  lgsdirprm  27532  gausslemma2dlem1a  27566  2sqlem8  27627  chpchtlim  27680  vmadivsumb  27684  rplogsumlem1  27685  dchrisumlem2  27691  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  dchrisum0re  27714  dchrisum0lem1b  27716  mulog2sumlem1  27735  mulog2sumlem2  27736  logsqvma2  27744  log2sumbnd  27745  selberglem2  27747  selbergb  27750  selberg2b  27753  chpdifbndlem1  27754  chpdifbndlem2  27755  selberg3lem2  27759  selberg3  27760  selberg4lem1  27761  selberg4  27762  pntrsumbnd2  27768  selberg3r  27770  selberg34r  27772  pntsf  27774  pntrlog2bndlem1  27778  pntrlog2bndlem2  27779  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntrlog2bndlem6  27784  pntrlog2bnd  27785  pntpbnd1a  27786  pntpbnd2  27788  pntibndlem2a  27791  pntibndlem2  27792  pntibndlem3  27793  pntlemg  27799  pntlemr  27803  pntlemk  27807  pntlemo  27808  pntlem3  27810  abvcxp  27816  padicabv  27831  ostth2lem2  27835  ostth3  27839  brbtwn2  29292  axsegconlem8  29311  axsegconlem10  29313  axpaschlem  29327  axpasch  29328  axeuclidlem  29349  axcontlem2  29352  crctcshwlkn0lem3  30198  crctcshwlkn0lem5  30200  vacn  31083  smcnlem  31086  ubthlem2  31260  minvecolem2  31264  minvecolem3  31265  minvecolem4  31269  minvecolem5  31270  nmoptrii  32483  hstle  32619  staddi  32635  stadd3i  32637  lt2addrd  33132  nndiffz1  33168  nexple  33214  wrdt2ind  33306  cshwrnid  33312  fsumrp0cl  33372  pmtrto1cl  33450  fzto1st  33454  psgnfzto1st  33456  constrresqrtcl  34198  cos9thpiminplylem1  34203  1smat1  34225  sqsscirc1  34329  cnre2csqlem  34331  tpr2rico  34333  dya2iocress  34696  dya2iocbrsiga  34697  dya2icobrsiga  34698  dya2icoseg  34699  dya2iocucvr  34706  sxbrsigalem2  34708  omssubaddlem  34721  fibp1  34823  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemsgt1  34933  ballotlemsel1i  34935  breprexplemc  35051  breprexp  35052  logdivsqrle  35069  resconn  35759  faclim  36259  dnizphlfeqhlf  37106  dnibndlem4  37111  dnibndlem6  37113  dnibndlem8  37115  dnibndlem9  37116  dnibndlem10  37117  dnibndlem11  37118  dnibndlem13  37120  dnibnd  37121  knoppcnlem4  37126  unblimceq0lem  37136  unblimceq0  37137  unbdqndv2lem1  37139  poimirlem29  38341  heicant  38347  opnmbllem0  38348  mblfinlem3  38351  mblfinlem4  38352  ismblfin  38353  mbfposadd  38359  itg2addnclem  38363  itg2addnclem3  38365  itg2addnc  38366  itg2gt0cn  38367  ibladdnclem  38368  itgaddnclem1  38370  itgaddnclem2  38371  iblabsnclem  38375  iblabsnc  38376  iblmulc2nc  38377  ftc1cnnclem  38383  ftc1anclem4  38388  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  areacirclem5  38404  mettrifi  38449  isbnd3  38476  ssbnd  38480  cntotbnd  38488  heibor1lem  38501  bfplem2  38515  rrnequiv  38527  iccbnd  38532  lcmineqlem18  42854  lcmineqlem20  42856  aks4d1p1p3  42877  aks4d1p1p2  42878  aks4d1p1p4  42879  aks4d1p1p6  42881  aks4d1p1p7  42882  aks4d1p1p5  42883  aks4d1p1  42884  posbezout  42908  aks6d1c1  42924  aks6d1c2  42938  2np3bcnp1  42952  2ap1caineq  42953  sticksstones6  42959  sticksstones7  42960  sticksstones10  42963  sticksstones12a  42965  sticksstones12  42966  sticksstones22  42976  bcle2d  42987  aks6d1c7lem1  42988  readdridaddlidd  43066  resubeulem1  43177  resubeulem2  43178  resubeu  43179  readdsub  43186  reladdrsub  43187  resubidaddlidlem  43196  renegid2  43216  sn-it0e0  43218  redivdird  43264  sn-0tie0  43266  sn-addlt0d  43273  sn-addgt0d  43274  cnreeu  43305  dffltz  43407  fltnltalem  43435  fltnlta  43436  3cubeslem1  43456  pellexlem2  43598  pell1qrge1  43638  pell14qrgapw  43644  pellqrexplicit  43645  pellqrex  43647  pellfundge  43650  pellfundgt1  43651  rmspecfund  43677  rmxycomplete  43685  ltrmynn0  43716  jm2.24nn  43727  jm2.24  43731  fzmaxdif  43749  jm2.26lem3  43769  jm3.1lem2  43786  areaquad  43984  sqrtcvallem4  44406  sqrtcvallem5  44407  sqrtcval  44408  imo72b2lem0  44932  hashnzfzclim  45073  binomcxplemnotnn0  45107  zltlesub  46045  lt3addmuld  46061  absnpncan2d  46062  fperiodmullem  46063  lt4addmuld  46066  absnpncan3d  46067  supxrgelem  46094  supxrge  46095  ltadd12dd  46100  xralrple2  46111  infxr  46123  infleinflem2  46127  xralrple4  46129  xralrple3  46130  xrralrecnnle  46139  eliooshift  46263  iccshift  46275  iooshift  46279  iooiinicc  46299  iooiinioc  46313  fsumnncl  46329  climinf  46363  climsuselem1  46364  sumnnodd  46387  lptre2pt  46395  addlimc  46403  0ellimcdiv  46404  limclner  46406  climleltrp  46431  liminfltlem  46559  fperdvper  46674  dvdivbd  46678  dvbdfbdioolem2  46684  dvbdfbdioo  46685  ioodvbdlimc1lem1  46686  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvxpaek  46695  dvnmul  46698  iblsplit  46721  iblspltprt  46728  itgspltprt  46734  itgiccshift  46735  itgperiod  46736  itgsbtaddcnst  46737  stoweidlem1  46756  stoweidlem11  46766  stoweidlem13  46768  stoweidlem14  46769  stoweidlem20  46775  stoweidlem21  46776  stoweidlem26  46781  stoweidlem44  46799  stoweidlem60  46815  wallispilem3  46822  wallispilem4  46823  wallispilem5  46824  wallispi  46825  wallispi2lem1  46826  wallispi2lem2  46827  stirlinglem1  46829  stirlinglem3  46831  stirlinglem5  46833  stirlinglem6  46834  stirlinglem7  46835  stirlinglem10  46838  stirlinglem11  46839  stirlinglem12  46840  dirker2re  46847  dirkerval2  46849  dirkerre  46850  dirkerper  46851  dirkertrigeqlem1  46853  dirkertrigeqlem2  46854  dirkeritg  46857  dirkercncflem1  46858  dirkercncflem2  46859  dirkercncflem4  46861  fourierdlem4  46866  fourierdlem5  46867  fourierdlem6  46868  fourierdlem7  46869  fourierdlem9  46871  fourierdlem10  46872  fourierdlem18  46880  fourierdlem19  46881  fourierdlem20  46882  fourierdlem26  46888  fourierdlem28  46890  fourierdlem30  46892  fourierdlem35  46897  fourierdlem40  46902  fourierdlem41  46903  fourierdlem42  46904  fourierdlem47  46908  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem51  46912  fourierdlem53  46914  fourierdlem57  46918  fourierdlem59  46920  fourierdlem60  46921  fourierdlem61  46922  fourierdlem63  46924  fourierdlem64  46925  fourierdlem65  46926  fourierdlem66  46927  fourierdlem68  46929  fourierdlem71  46932  fourierdlem72  46933  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem78  46939  fourierdlem79  46940  fourierdlem80  46941  fourierdlem81  46942  fourierdlem82  46943  fourierdlem83  46944  fourierdlem84  46945  fourierdlem87  46948  fourierdlem88  46949  fourierdlem89  46950  fourierdlem90  46951  fourierdlem91  46952  fourierdlem92  46953  fourierdlem93  46954  fourierdlem94  46955  fourierdlem95  46956  fourierdlem97  46958  fourierdlem101  46962  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  sqwvfoura  46983  sqwvfourb  46984  fouriersw  46986  qndenserrnbllem  47049  ioorrnopnlem  47059  ioorrnopnxrlem  47061  sge0xaddlem1  47188  sge0xaddlem2  47189  omeiunltfirp  47274  carageniuncllem2  47277  hoidmv1lelem1  47346  hoidmv1lelem2  47347  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  hoiqssbllem1  47377  hoiqssbllem2  47378  hoiqssbllem3  47379  hspmbllem2  47382  hspmbllem3  47383  ovolval5lem1  47407  iinhoiicclem  47428  iinhoiicc  47429  iunhoiioolem  47430  iccvonmbllem  47433  vonioolem1  47435  vonioolem2  47436  vonicclem1  47438  vonicclem2  47439  preimaleiinlt  47476  salpreimaltle  47481  smfaddlem1  47518  smfadd  47520  smflimlem3  47528  smflimlem4  47529  smflimlem6  47531  smfmullem1  47546  smfmullem2  47547  smfmullem3  47548  ormkglobd  47632  zm1nn  48080  requad01  48427  requad1  48428  requad2  48429  perfectALTVlem2  48528  nnsum4primesevenALTV  48607  bgoldbtbndlem2  48612  gpgvtxedg0  48869  gpgvtxedg1  48870  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx13starlem2  48878  dignn0flhalflem1  49436  affinecomb1  49523  resum2sqcl  49527  2sphere  49570  line2  49573  itsclc0lem1  49577  itscnhlc0yqe  49580  itsclquadb  49597  2itscp  49602  itscnhlinecirc02plem1  49603  itscnhlinecirc02plem3  49605  itscnhlinecirc02p  49606  inlinecirc02plem  49607  amgmwlem  50691