Theorem readdcld 11165

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7360  ℝcr 11028   + caddc 11032

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

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

This theorem is referenced by:  ltadd2  11241  readdcan  11311  addrid  11317  leadd1  11609  le2add  11623  lesub2  11636  lesub3d  11759  le2addd  11760  supaddc  12114  supadd  12115  cju  12146  nnne0  12202  div4p1lem1div2  12423  difgtsumgt  12481  eluzmn  12786  rpnnen1lem5  12922  addlelt  13049  xralrple  13148  xov1plusxeqvd  13442  zltaddlt1le  13449  elincfzoext  13669  fladdz  13775  2tnp1ge0ge0  13779  flhalf  13780  fldiv  13810  modaddb  13859  modaddmodup  13887  modaddmodlo  13888  addmodlteq  13899  discr1  14192  discr  14193  ccatalpha  14547  2cshw  14766  remim  15070  remullem  15081  01sqrexlem7  15201  absrele  15261  abstri  15284  abs3lem  15292  amgm2  15323  bhmafibid1  15421  mulcn2  15549  o1add  15567  o1sub  15569  lo1add  15580  caucvgrlem  15626  iseraltlem2  15636  iseraltlem3  15637  fsumabs  15755  o1fsum  15767  climcndslem2  15806  tanhlt1  16118  eirrlem  16162  ruclem1  16189  ruclem2  16190  ruclem3  16191  ltoddhalfle  16321  bitscmp  16398  sadcaddlem  16417  sadasslem  16430  smuval2  16442  iserodd  16797  prmreclem4  16881  4sqlem5  16904  4sqlem6  16905  4sqlem12  16918  4sqlem15  16921  4sqlem16  16922  prmgaplem7  17019  prmgaplem8  17020  2expltfac  17054  cshwshashlem2  17058  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  prdsxmetlem  24343  xblss2ps  24376  metustexhalf  24531  nrmmetd  24549  ngptgp  24611  nlmvscnlem2  24660  nlmvscnlem1  24661  nmotri  24714  nghmplusg  24715  blcvx  24773  iccntr  24797  icccmplem2  24799  reconnlem2  24803  metdcnlem  24812  metnrmlem3  24837  cnllycmp  24933  lebnumii  24943  tcphcphlem1  25212  ipcnlem2  25221  ipcnlem1  25222  csbren  25376  trirn  25377  minveclem2  25403  minveclem3b  25405  minveclem4  25409  ivthlem2  25429  ovolgelb  25457  ovollb2lem  25465  ovolunlem1a  25473  ovolunlem1  25474  ovolfiniun  25478  ovoliunlem1  25479  ovoliunlem2  25480  ovolshftlem1  25486  ovolscalem1  25490  ovolicopnf  25501  ismbl2  25504  nulmbl2  25513  unmbl  25514  voliunlem2  25528  ioombl1lem2  25536  ioombl1lem4  25538  ioombl1  25539  ioorcl2  25549  uniioombllem1  25558  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  uniioombl  25566  opnmbllem  25578  volcn  25583  itg1addlem4  25676  mbfi1fseqlem4  25695  mbfi1fseqlem6  25697  itg2splitlem  25725  itg2split  25726  itg2monolem3  25729  itg2addlem  25735  ibladdlem  25797  itgaddlem1  25800  itgaddlem2  25801  iblabslem  25805  iblabs  25806  dvferm1lem  25961  dvferm2lem  25963  dvlip2  25972  lhop1lem  25990  lhop1  25991  lhop  25993  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  dvcvx  25997  dvfsumlem3  26005  dvfsumlem4  26006  dvfsum2  26011  ftc1lem4  26016  coemullem  26225  ulmbdd  26376  ulmcn  26377  ulmdvlem1  26378  radcnvle  26398  pserdvlem1  26405  pserdv  26407  abelthlem7  26416  pilem2  26430  pilem3  26431  cosordlem  26507  abslogle  26595  logccv  26640  cxpaddle  26729  ang180lem2  26787  heron  26815  atanlogaddlem  26890  atans2  26908  cxp2limlem  26953  scvxcvx  26963  jensenlem2  26965  amgmlem  26967  logdiflbnd  26972  harmonicbnd4  26988  fsumharmonic  26989  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgambdd  27014  lgamucov  27015  regamcl  27038  ftalem5  27054  efnnfsumcl  27080  efchtdvds  27136  chtublem  27188  chtub  27189  logfaclbnd  27199  perfectlem2  27207  bposlem7  27267  bposlem9  27269  lgsdirprm  27308  gausslemma2dlem1a  27342  2sqlem8  27403  chpchtlim  27456  vmadivsumb  27460  rplogsumlem1  27461  dchrisumlem2  27467  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  dchrisum0re  27490  dchrisum0lem1b  27492  mulog2sumlem1  27511  mulog2sumlem2  27512  logsqvma2  27520  log2sumbnd  27521  selberglem2  27523  selbergb  27526  selberg2b  27529  chpdifbndlem1  27530  chpdifbndlem2  27531  selberg3lem2  27535  selberg3  27536  selberg4lem1  27537  selberg4  27538  pntrsumbnd2  27544  selberg3r  27546  selberg34r  27548  pntsf  27550  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntpbnd1a  27562  pntpbnd2  27564  pntibndlem2a  27567  pntibndlem2  27568  pntibndlem3  27569  pntlemg  27575  pntlemr  27579  pntlemk  27583  pntlemo  27584  pntlem3  27586  abvcxp  27592  padicabv  27607  ostth2lem2  27611  ostth3  27615  brbtwn2  28988  axsegconlem8  29007  axsegconlem10  29009  axpaschlem  29023  axpasch  29024  axeuclidlem  29045  axcontlem2  29048  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  vacn  30780  smcnlem  30783  ubthlem2  30957  minvecolem2  30961  minvecolem3  30962  minvecolem4  30966  minvecolem5  30967  nmoptrii  32180  hstle  32316  staddi  32332  stadd3i  32334  lt2addrd  32838  nndiffz1  32874  nexple  32932  wrdt2ind  33028  cshwrnid  33036  fsumrp0cl  33096  pmtrto1cl  33175  fzto1st  33179  psgnfzto1st  33181  constrresqrtcl  33937  cos9thpiminplylem1  33942  1smat1  33964  sqsscirc1  34068  cnre2csqlem  34070  tpr2rico  34072  dya2iocress  34434  dya2iocbrsiga  34435  dya2icobrsiga  34436  dya2icoseg  34437  dya2iocucvr  34444  sxbrsigalem2  34446  omssubaddlem  34459  fibp1  34561  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemsgt1  34671  ballotlemsel1i  34673  plymulx0  34707  breprexplemc  34792  breprexp  34793  logdivsqrle  34810  resconn  35444  faclim  35944  dnizphlfeqhlf  36752  dnibndlem4  36757  dnibndlem6  36759  dnibndlem8  36761  dnibndlem9  36762  dnibndlem10  36763  dnibndlem11  36764  dnibndlem13  36766  dnibnd  36767  knoppcnlem4  36772  unblimceq0lem  36782  unblimceq0  36783  unbdqndv2lem1  36785  poimirlem29  37984  heicant  37990  opnmbllem0  37991  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  mbfposadd  38002  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  ibladdnclem  38011  itgaddnclem1  38013  itgaddnclem2  38014  iblabsnclem  38018  iblabsnc  38019  iblmulc2nc  38020  ftc1cnnclem  38026  ftc1anclem4  38031  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  areacirclem5  38047  mettrifi  38092  isbnd3  38119  ssbnd  38123  cntotbnd  38131  heibor1lem  38144  bfplem2  38158  rrnequiv  38170  iccbnd  38175  lcmineqlem18  42499  lcmineqlem20  42501  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  posbezout  42553  aks6d1c1  42569  aks6d1c2  42583  2np3bcnp1  42597  2ap1caineq  42598  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  bcle2d  42632  aks6d1c7lem1  42633  readdridaddlidd  42710  resubeulem1  42821  resubeulem2  42822  resubeu  42823  readdsub  42830  reladdrsub  42831  resubidaddlidlem  42840  renegid2  42860  sn-it0e0  42862  redivdird  42908  sn-0tie0  42910  sn-addlt0d  42917  sn-addgt0d  42918  cnreeu  42949  dffltz  43081  fltnltalem  43109  fltnlta  43110  3cubeslem1  43130  pellexlem2  43276  pell1qrge1  43316  pell14qrgapw  43322  pellqrexplicit  43323  pellqrex  43325  pellfundge  43328  pellfundgt1  43329  rmspecfund  43355  rmxycomplete  43363  ltrmynn0  43394  jm2.24nn  43405  jm2.24  43409  fzmaxdif  43427  jm2.26lem3  43447  jm3.1lem2  43464  areaquad  43662  sqrtcvallem4  44084  sqrtcvallem5  44085  sqrtcval  44086  imo72b2lem0  44610  hashnzfzclim  44767  binomcxplemnotnn0  44801  zltlesub  45736  lt3addmuld  45752  absnpncan2d  45753  fperiodmullem  45754  lt4addmuld  45757  absnpncan3d  45758  supxrgelem  45785  supxrge  45786  ltadd12dd  45791  xralrple2  45802  infxr  45814  infleinflem2  45818  xralrple4  45820  xralrple3  45821  xrralrecnnle  45830  eliooshift  45954  iccshift  45966  iooshift  45970  iooiinicc  45990  iooiinioc  46004  fsumnncl  46020  climinf  46054  climsuselem1  46055  sumnnodd  46078  lptre2pt  46086  addlimc  46094  0ellimcdiv  46095  limclner  46097  climleltrp  46122  liminfltlem  46250  fperdvper  46365  dvdivbd  46369  dvbdfbdioolem2  46375  dvbdfbdioo  46376  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvxpaek  46386  dvnmul  46389  iblsplit  46412  iblspltprt  46419  itgspltprt  46425  itgiccshift  46426  itgperiod  46427  itgsbtaddcnst  46428  stoweidlem1  46447  stoweidlem11  46457  stoweidlem13  46459  stoweidlem14  46460  stoweidlem20  46466  stoweidlem21  46467  stoweidlem26  46472  stoweidlem44  46490  stoweidlem60  46506  wallispilem3  46513  wallispilem4  46514  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem1  46520  stirlinglem3  46522  stirlinglem5  46524  stirlinglem6  46525  stirlinglem7  46526  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  dirker2re  46538  dirkerval2  46540  dirkerre  46541  dirkerper  46542  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkeritg  46548  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem4  46557  fourierdlem5  46558  fourierdlem6  46559  fourierdlem7  46560  fourierdlem9  46562  fourierdlem10  46563  fourierdlem18  46571  fourierdlem19  46572  fourierdlem20  46573  fourierdlem26  46579  fourierdlem28  46581  fourierdlem30  46583  fourierdlem35  46588  fourierdlem40  46593  fourierdlem41  46594  fourierdlem42  46595  fourierdlem47  46599  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem53  46605  fourierdlem57  46609  fourierdlem59  46611  fourierdlem60  46612  fourierdlem61  46613  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem66  46618  fourierdlem68  46620  fourierdlem71  46623  fourierdlem72  46624  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem79  46631  fourierdlem80  46632  fourierdlem81  46633  fourierdlem82  46634  fourierdlem83  46635  fourierdlem84  46636  fourierdlem87  46639  fourierdlem88  46640  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem93  46645  fourierdlem94  46646  fourierdlem95  46647  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  qndenserrnbllem  46740  ioorrnopnlem  46750  ioorrnopnxrlem  46752  sge0xaddlem1  46879  sge0xaddlem2  46880  omeiunltfirp  46965  carageniuncllem2  46968  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoiqssbllem1  47068  hoiqssbllem2  47069  hoiqssbllem3  47070  hspmbllem2  47073  hspmbllem3  47074  ovolval5lem1  47098  iinhoiicclem  47119  iinhoiicc  47120  iunhoiioolem  47121  iccvonmbllem  47124  vonioolem1  47126  vonioolem2  47127  vonicclem1  47129  vonicclem2  47130  preimaleiinlt  47167  salpreimaltle  47172  smfaddlem1  47209  smfadd  47211  smflimlem3  47219  smflimlem4  47220  smflimlem6  47222  smfmullem1  47237  smfmullem2  47238  smfmullem3  47239  ormkglobd  47321  zm1nn  47762  requad01  48109  requad1  48110  requad2  48111  perfectALTVlem2  48210  nnsum4primesevenALTV  48289  bgoldbtbndlem2  48294  gpgvtxedg0  48551  gpgvtxedg1  48552  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx13starlem2  48560  dignn0flhalflem1  49103  affinecomb1  49190  resum2sqcl  49194  2sphere  49237  line2  49240  itsclc0lem1  49244  itscnhlc0yqe  49247  itsclquadb  49264  2itscp  49269  itscnhlinecirc02plem1  49270  itscnhlinecirc02plem3  49272  itscnhlinecirc02p  49273  inlinecirc02plem  49274  amgmwlem  50289