Theorem readdcld 11368

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7446  ℝcr 11229   + caddc 11233

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

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

This theorem is used by:  ltadd2  11444  readdcan  11514  addrid  11520  leadd1  11814  le2add  11828  lesub2  11841  lesub3d  11964  le2addd  11965  supaddc  12314  supadd  12315  cju  12346  nnne0  12402  div4p1lem1div2  12631  difgtsumgt  12689  eluzmn  13002  rpnnen1lem5  13139  addlelt  13266  xralrple  13365  xov1plusxeqvd  13659  zltaddlt1le  13666  elincfzoext  13888  fladdz  13995  2tnp1ge0ge0  13999  flhalf  14000  fldiv  14030  modaddb  14079  modaddmodup  14107  modaddmodlo  14108  addmodlteq  14119  discr1  14413  discr  14414  ccatalpha  14770  2cshw  14995  remim  15316  remullem  15327  01sqrexlem7  15447  absrele  15507  abstri  15530  abs3lem  15538  amgm2  15569  bhmafibid1  15667  mulcn2  15795  o1add  15813  o1sub  15815  lo1add  15826  caucvgrlem  15872  iseraltlem2  15882  iseraltlem3  15883  fsumabs  16000  o1fsum  16012  climcndslem2  16051  tanhlt1  16360  eirrlem  16404  ruclem1  16431  ruclem2  16432  ruclem3  16433  ltoddhalfle  16563  bitscmp  16640  sadcaddlem  16659  sadasslem  16672  smuval2  16684  iserodd  17045  prmreclem4  17129  4sqlem5  17152  4sqlem6  17153  4sqlem12  17166  4sqlem15  17169  4sqlem16  17170  prmgaplem7  17267  prmgaplem8  17268  2expltfac  17302  cshwshashlem2  17306  chfacfscmul0  23209  chfacfscmulgsum  23211  chfacfpmmul0  23213  chfacfpmmulgsum  23215  prdsxmetlem  24720  xblss2ps  24753  metustexhalf  24908  nrmmetd  24926  ngptgp  24988  nlmvscnlem2  25037  nlmvscnlem1  25038  nmotri  25091  nghmplusg  25092  blcvx  25150  iccntr  25174  icccmplem2  25176  reconnlem2  25180  metdcnlem  25189  metnrmlem3  25214  cnllycmp  25310  lebnumii  25320  tcphcphlem1  25589  ipcnlem2  25598  ipcnlem1  25599  csbren  25753  trirn  25754  minveclem2  25780  minveclem3b  25782  minveclem4  25786  ivthlem2  25806  ovolgelb  25834  ovollb2lem  25842  ovolunlem1a  25850  ovolunlem1  25851  ovolfiniun  25855  ovoliunlem1  25856  ovoliunlem2  25857  ovolshftlem1  25863  ovolscalem1  25867  ovolicopnf  25878  ismbl2  25881  nulmbl2  25890  unmbl  25891  voliunlem2  25905  ioombl1lem2  25913  ioombl1lem4  25915  ioombl1  25916  ioorcl2  25926  uniioombllem1  25935  uniioombllem3  25939  uniioombllem4  25940  uniioombllem5  25941  uniioombl  25943  opnmbllem  25955  volcn  25960  itg1addlem4  26053  mbfi1fseqlem4  26072  mbfi1fseqlem6  26074  itg2splitlem  26102  itg2split  26103  itg2monolem3  26106  itg2addlem  26112  ibladdlem  26173  itgaddlem1  26176  itgaddlem2  26177  iblabslem  26181  iblabs  26182  dvferm1lem  26337  dvferm2lem  26339  dvlip2  26348  lhop1lem  26366  lhop1  26367  lhop  26369  dvcnvrelem1  26370  dvcnvrelem2  26371  dvcnvre  26372  dvcvx  26373  dvfsumlem3  26381  dvfsumlem4  26382  dvfsum2  26387  ftc1lem4  26392  coemullem  26602  plyn0mulidp  26635  ulmbdd  26758  ulmcn  26759  ulmdvlem1  26760  radcnvle  26780  pserdvlem1  26787  pserdv  26789  abelthlem7  26798  pilem2  26812  pilem3  26813  cosordlem  26891  abslogle  26979  logccv  27024  cxpaddle  27113  ang180lem2  27171  heron  27199  atanlogaddlem  27274  atans2  27292  cxp2limlem  27336  scvxcvx  27346  jensenlem2  27348  amgmlem  27350  logdiflbnd  27355  harmonicbnd4  27371  fsumharmonic  27372  lgamgulmlem3  27391  lgamgulmlem4  27392  lgamgulmlem5  27393  lgamgulmlem6  27394  lgambdd  27397  lgamucov  27398  regamcl  27421  ftalem5  27437  efnnfsumcl  27463  efchtdvds  27519  chtublem  27571  chtub  27572  logfaclbnd  27582  perfectlem2  27590  bposlem7  27650  bposlem9  27652  lgsdirprm  27691  gausslemma2dlem1a  27725  2sqlem8  27786  chpchtlim  27839  vmadivsumb  27843  rplogsumlem1  27844  dchrisumlem2  27850  dchrvmasumlem2  27858  dchrvmasumiflem1  27861  dchrisum0re  27873  dchrisum0lem1b  27875  mulog2sumlem1  27894  mulog2sumlem2  27895  logsqvma2  27903  log2sumbnd  27904  selberglem2  27906  selbergb  27909  selberg2b  27912  chpdifbndlem1  27913  chpdifbndlem2  27914  selberg3lem2  27918  selberg3  27919  selberg4lem1  27920  selberg4  27921  pntrsumbnd2  27927  selberg3r  27929  selberg34r  27931  pntsf  27933  pntrlog2bndlem1  27937  pntrlog2bndlem2  27938  pntrlog2bndlem4  27940  pntrlog2bndlem5  27941  pntrlog2bndlem6  27943  pntrlog2bnd  27944  pntpbnd1a  27945  pntpbnd2  27947  pntibndlem2a  27950  pntibndlem2  27951  pntibndlem3  27952  pntlemg  27958  pntlemr  27962  pntlemk  27966  pntlemo  27967  pntlem3  27969  abvcxp  27975  padicabv  27990  ostth2lem2  27994  ostth3  27998  brbtwn2  29516  axsegconlem8  29535  axsegconlem10  29537  axpaschlem  29551  axpasch  29552  axeuclidlem  29573  axcontlem2  29576  crctcshwlkn0lem3  30434  crctcshwlkn0lem5  30436  vacn  31329  smcnlem  31332  ubthlem2  31506  minvecolem2  31510  minvecolem3  31511  minvecolem4  31515  minvecolem5  31516  nmoptrii  32729  hstle  32865  staddi  32881  stadd3i  32883  lt2addrd  33415  nndiffz1  33451  nexple  33497  wrdt2ind  33589  cshwrnid  33595  fsumrp0cl  33658  pmtrto1cl  33736  fzto1st  33740  psgnfzto1st  33742  constrresqrtcl  34492  cos9thpiminplylem1  34497  1smat1  34519  sqsscirc1  34623  cnre2csqlem  34625  tpr2rico  34627  dya2iocress  34989  dya2iocbrsiga  34990  dya2icobrsiga  34991  dya2icoseg  34992  dya2iocucvr  34999  sxbrsigalem2  35001  omssubaddlem  35014  fibp1  35116  ballotlemfc0  35208  ballotlemfcc  35209  ballotlemsgt1  35226  ballotlemsel1i  35228  breprexplemc  35344  breprexp  35345  logdivsqrle  35362  resconn  36191  faclim  36702  dnizphlfeqhlf  37533  dnibndlem4  37538  dnibndlem6  37540  dnibndlem8  37542  dnibndlem9  37543  dnibndlem10  37544  dnibndlem11  37545  dnibndlem13  37547  dnibnd  37548  knoppcnlem4  37553  unblimceq0lem  37563  unblimceq0  37564  unbdqndv2lem1  37566  poimirlem29  38772  heicant  38778  opnmbllem0  38779  mblfinlem3  38782  mblfinlem4  38783  ismblfin  38784  mbfposadd  38790  itg2addnclem  38794  itg2addnclem3  38796  itg2addnc  38797  itg2gt0cn  38798  ibladdnclem  38799  itgaddnclem1  38801  itgaddnclem2  38802  iblabsnclem  38806  iblabsnc  38807  iblmulc2nc  38808  ftc1cnnclem  38814  ftc1anclem4  38819  ftc1anclem7  38822  ftc1anclem8  38823  ftc1anc  38824  areacirclem5  38835  mettrifi  38894  isbnd3  38921  ssbnd  38925  cntotbnd  38933  heibor1lem  38946  bfplem2  38960  rrnequiv  38972  iccbnd  38977  lcmineqlem18  43299  lcmineqlem20  43301  aks4d1p1p3  43322  aks4d1p1p2  43323  aks4d1p1p4  43324  aks4d1p1p6  43326  aks4d1p1p7  43327  aks4d1p1p5  43328  aks4d1p1  43329  posbezout  43353  aks6d1c1  43369  aks6d1c2  43383  2np3bcnp1  43397  2ap1caineq  43398  sticksstones6  43404  sticksstones7  43405  sticksstones10  43408  sticksstones12a  43410  sticksstones12  43411  sticksstones22  43421  bcle2d  43432  aks6d1c7lem1  43433  readdridaddlidd  43512  resubeulem1  43630  resubeulem2  43631  resubeu  43632  readdsub  43639  reladdrsub  43640  resubidaddlidlem  43649  renegid2  43669  sn-it0e0  43671  redivdird  43717  sn-0tie0  43719  sn-addlt0d  43726  sn-addgt0d  43727  cnreeu  43758  dffltz  43874  fltnltalem  43877  fltnlta  43878  3cubeslem1  43898  pellexlem2  44041  pell1qrge1  44081  pell14qrgapw  44087  pellqrexplicit  44088  pellqrex  44090  pellfundge  44093  pellfundgt1  44094  rmspecfund  44120  rmxycomplete  44128  ltrmynn0  44159  jm2.24nn  44170  jm2.24  44174  fzmaxdif  44192  jm2.26lem3  44212  jm3.1lem2  44229  areaquad  44421  sqrtcvallem4  44842  sqrtcvallem5  44843  sqrtcval  44844  imo72b2lem0  45368  hashnzfzclim  45509  binomcxplemnotnn0  45543  zltlesub  46516  lt3addmuld  46532  absnpncan2d  46533  fperiodmullem  46534  lt4addmuld  46537  absnpncan3d  46538  supxrgelem  46564  supxrge  46565  ltadd12dd  46570  xralrple2  46581  infxr  46593  infleinflem2  46597  xralrple4  46599  xralrple3  46600  xrralrecnnle  46609  eliooshift  46733  iccshift  46745  iooshift  46749  iooiinicc  46769  iooiinioc  46783  fsumnncl  46799  climinf  46833  climsuselem1  46834  sumnnodd  46857  lptre2pt  46865  addlimc  46873  0ellimcdiv  46874  limclner  46876  climleltrp  46901  liminfltlem  47029  fperdvper  47144  dvdivbd  47148  dvbdfbdioolem2  47154  dvbdfbdioo  47155  ioodvbdlimc1lem1  47156  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  dvxpaek  47165  dvnmul  47168  iblsplit  47191  iblspltprt  47198  itgspltprt  47204  itgiccshift  47205  itgperiod  47206  itgsbtaddcnst  47207  stoweidlem1  47226  stoweidlem11  47236  stoweidlem13  47238  stoweidlem14  47239  stoweidlem20  47245  stoweidlem21  47246  stoweidlem26  47251  stoweidlem44  47269  stoweidlem60  47285  wallispilem3  47292  wallispilem4  47293  wallispilem5  47294  wallispi  47295  wallispi2lem1  47296  wallispi2lem2  47297  stirlinglem1  47299  stirlinglem3  47301  stirlinglem5  47303  stirlinglem6  47304  stirlinglem7  47305  stirlinglem10  47308  stirlinglem11  47309  stirlinglem12  47310  dirker2re  47317  dirkerval2  47319  dirkerre  47320  dirkerper  47321  dirkertrigeqlem1  47323  dirkertrigeqlem2  47324  dirkeritg  47327  dirkercncflem1  47328  dirkercncflem2  47329  dirkercncflem4  47331  fourierdlem4  47336  fourierdlem5  47337  fourierdlem6  47338  fourierdlem7  47339  fourierdlem9  47341  fourierdlem10  47342  fourierdlem18  47350  fourierdlem19  47351  fourierdlem20  47352  fourierdlem26  47358  fourierdlem28  47360  fourierdlem30  47362  fourierdlem35  47367  fourierdlem40  47372  fourierdlem41  47373  fourierdlem42  47374  fourierdlem47  47378  fourierdlem48  47379  fourierdlem49  47380  fourierdlem50  47381  fourierdlem51  47382  fourierdlem53  47384  fourierdlem57  47388  fourierdlem59  47390  fourierdlem60  47391  fourierdlem61  47392  fourierdlem63  47394  fourierdlem64  47395  fourierdlem65  47396  fourierdlem66  47397  fourierdlem68  47399  fourierdlem71  47402  fourierdlem72  47403  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem78  47409  fourierdlem79  47410  fourierdlem80  47411  fourierdlem81  47412  fourierdlem82  47413  fourierdlem83  47414  fourierdlem84  47415  fourierdlem87  47418  fourierdlem88  47419  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem92  47423  fourierdlem93  47424  fourierdlem94  47425  fourierdlem95  47426  fourierdlem97  47428  fourierdlem101  47432  fourierdlem103  47434  fourierdlem104  47435  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  sqwvfoura  47453  sqwvfourb  47454  fouriersw  47456  qndenserrnbllem  47519  ioorrnopnlem  47529  ioorrnopnxrlem  47531  sge0xaddlem1  47658  sge0xaddlem2  47659  omeiunltfirp  47744  carageniuncllem2  47747  hoidmv1lelem1  47816  hoidmv1lelem2  47817  hoidmvlelem1  47820  hoidmvlelem2  47821  hoidmvlelem3  47822  hoidmvlelem4  47823  hoiqssbllem1  47847  hoiqssbllem2  47848  hoiqssbllem3  47849  hspmbllem2  47852  hspmbllem3  47853  ovolval5lem1  47877  iinhoiicclem  47898  iinhoiicc  47899  iunhoiioolem  47900  iccvonmbllem  47903  vonioolem1  47905  vonioolem2  47906  vonicclem1  47908  vonicclem2  47909  preimaleiinlt  47946  salpreimaltle  47951  smfaddlem1  47988  smfadd  47990  smflimlem3  47998  smflimlem4  47999  smflimlem6  48001  smfmullem1  48016  smfmullem2  48017  smfmullem3  48018  ormkglobd  48102  zm1nn  48587  requad01  48934  requad1  48935  requad2  48936  perfectALTVlem2  49035  nnsum4primesevenALTV  49114  bgoldbtbndlem2  49119  gpgvtxedg0  49376  gpgvtxedg1  49377  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx13starlem2  49385  dignn0flhalflem1  49942  affinecomb1  50029  resum2sqcl  50033  2sphere  50076  line2  50079  itsclc0lem1  50083  itscnhlc0yqe  50086  itsclquadb  50103  2itscp  50108  itscnhlinecirc02plem1  50109  itscnhlinecirc02plem3  50111  itscnhlinecirc02p  50112  inlinecirc02plem  50113  crossp3d  51279  veronesefvcl  51284  veronesev1lem  51285  veronesev2lem  51286  veronesev3lem  51287  veronesev4lem  51288  veronesev5lem  51289  veronesev6lem  51290  amgmwlem  51299