Theorem readdcld 11148

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7352  ℝcr 11012   + caddc 11016

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

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

This theorem is referenced by:  ltadd2  11224  readdcan  11294  addrid  11300  leadd1  11592  le2add  11606  lesub2  11619  lesub3d  11742  le2addd  11743  supaddc  12096  supadd  12097  cju  12128  nnne0  12166  div4p1lem1div2  12383  difgtsumgt  12441  eluzmn  12745  rpnnen1lem5  12881  addlelt  13008  xralrple  13106  xov1plusxeqvd  13400  zltaddlt1le  13407  elincfzoext  13625  fladdz  13731  2tnp1ge0ge0  13735  flhalf  13736  fldiv  13766  modaddb  13815  modaddmodup  13843  modaddmodlo  13844  addmodlteq  13855  discr1  14148  discr  14149  ccatalpha  14503  2cshw  14722  remim  15026  remullem  15037  01sqrexlem7  15157  absrele  15217  abstri  15240  abs3lem  15248  amgm2  15279  bhmafibid1  15377  mulcn2  15505  o1add  15523  o1sub  15525  lo1add  15536  caucvgrlem  15582  iseraltlem2  15592  iseraltlem3  15593  fsumabs  15710  o1fsum  15722  climcndslem2  15759  tanhlt1  16071  eirrlem  16115  ruclem1  16142  ruclem2  16143  ruclem3  16144  ltoddhalfle  16274  bitscmp  16351  sadcaddlem  16370  sadasslem  16383  smuval2  16395  iserodd  16749  prmreclem4  16833  4sqlem5  16856  4sqlem6  16857  4sqlem12  16870  4sqlem15  16873  4sqlem16  16874  prmgaplem7  16971  prmgaplem8  16972  2expltfac  17006  cshwshashlem2  17010  chfacfscmul0  22774  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulgsum  22780  prdsxmetlem  24284  xblss2ps  24317  metustexhalf  24472  nrmmetd  24490  ngptgp  24552  nlmvscnlem2  24601  nlmvscnlem1  24602  nmotri  24655  nghmplusg  24656  blcvx  24714  iccntr  24738  icccmplem2  24740  reconnlem2  24744  metdcnlem  24753  metnrmlem3  24778  cnllycmp  24883  lebnumii  24893  tcphcphlem1  25163  ipcnlem2  25172  ipcnlem1  25173  csbren  25327  trirn  25328  minveclem2  25354  minveclem3b  25356  minveclem4  25360  ivthlem2  25381  ovolgelb  25409  ovollb2lem  25417  ovolunlem1a  25425  ovolunlem1  25426  ovolfiniun  25430  ovoliunlem1  25431  ovoliunlem2  25432  ovolshftlem1  25438  ovolscalem1  25442  ovolicopnf  25453  ismbl2  25456  nulmbl2  25465  unmbl  25466  voliunlem2  25480  ioombl1lem2  25488  ioombl1lem4  25490  ioombl1  25491  ioorcl2  25501  uniioombllem1  25510  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  uniioombl  25518  opnmbllem  25530  volcn  25535  itg1addlem4  25628  mbfi1fseqlem4  25647  mbfi1fseqlem6  25649  itg2splitlem  25677  itg2split  25678  itg2monolem3  25681  itg2addlem  25687  ibladdlem  25749  itgaddlem1  25752  itgaddlem2  25753  iblabslem  25757  iblabs  25758  dvferm1lem  25916  dvferm2lem  25918  dvlip2  25928  lhop1lem  25946  lhop1  25947  lhop  25949  dvcnvrelem1  25950  dvcnvrelem2  25951  dvcnvre  25952  dvcvx  25953  dvfsumlem3  25963  dvfsumlem4  25964  dvfsum2  25969  ftc1lem4  25974  coemullem  26183  ulmbdd  26335  ulmcn  26336  ulmdvlem1  26337  radcnvle  26357  pserdvlem1  26365  pserdv  26367  abelthlem7  26376  pilem2  26390  pilem3  26391  cosordlem  26467  abslogle  26555  logccv  26600  cxpaddle  26690  ang180lem2  26748  heron  26776  atanlogaddlem  26851  atans2  26869  cxp2limlem  26914  scvxcvx  26924  jensenlem2  26926  amgmlem  26928  logdiflbnd  26933  harmonicbnd4  26949  fsumharmonic  26950  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem5  26971  lgamgulmlem6  26972  lgambdd  26975  lgamucov  26976  regamcl  26999  ftalem5  27015  efnnfsumcl  27041  efchtdvds  27097  chtublem  27150  chtub  27151  logfaclbnd  27161  perfectlem2  27169  bposlem7  27229  bposlem9  27231  lgsdirprm  27270  gausslemma2dlem1a  27304  2sqlem8  27365  chpchtlim  27418  vmadivsumb  27422  rplogsumlem1  27423  dchrisumlem2  27429  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  dchrisum0re  27452  dchrisum0lem1b  27454  mulog2sumlem1  27473  mulog2sumlem2  27474  logsqvma2  27482  log2sumbnd  27483  selberglem2  27485  selbergb  27488  selberg2b  27491  chpdifbndlem1  27492  chpdifbndlem2  27493  selberg3lem2  27497  selberg3  27498  selberg4lem1  27499  selberg4  27500  pntrsumbnd2  27506  selberg3r  27508  selberg34r  27510  pntsf  27512  pntrlog2bndlem1  27516  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  pntrlog2bnd  27523  pntpbnd1a  27524  pntpbnd2  27526  pntibndlem2a  27529  pntibndlem2  27530  pntibndlem3  27531  pntlemg  27537  pntlemr  27541  pntlemk  27545  pntlemo  27546  pntlem3  27548  abvcxp  27554  padicabv  27569  ostth2lem2  27573  ostth3  27577  brbtwn2  28885  axsegconlem8  28904  axsegconlem10  28906  axpaschlem  28920  axpasch  28921  axeuclidlem  28942  axcontlem2  28945  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  vacn  30676  smcnlem  30679  ubthlem2  30853  minvecolem2  30857  minvecolem3  30858  minvecolem4  30862  minvecolem5  30863  nmoptrii  32076  hstle  32212  staddi  32228  stadd3i  32230  lt2addrd  32738  nndiffz1  32773  nexple  32832  wrdt2ind  32941  cshwrnid  32949  fsumrp0cl  33009  pmtrto1cl  33075  fzto1st  33079  psgnfzto1st  33081  constrresqrtcl  33811  cos9thpiminplylem1  33816  1smat1  33838  sqsscirc1  33942  cnre2csqlem  33944  tpr2rico  33946  dya2iocress  34308  dya2iocbrsiga  34309  dya2icobrsiga  34310  dya2icoseg  34311  dya2iocucvr  34318  sxbrsigalem2  34320  omssubaddlem  34333  fibp1  34435  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemsgt1  34545  ballotlemsel1i  34547  plymulx0  34581  breprexplemc  34666  breprexp  34667  logdivsqrle  34684  resconn  35311  faclim  35811  dnizphlfeqhlf  36541  dnibndlem4  36546  dnibndlem6  36548  dnibndlem8  36550  dnibndlem9  36551  dnibndlem10  36552  dnibndlem11  36553  dnibndlem13  36555  dnibnd  36556  knoppcnlem4  36561  unblimceq0lem  36571  unblimceq0  36572  unbdqndv2lem1  36574  poimirlem29  37709  heicant  37715  opnmbllem0  37716  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  mbfposadd  37727  itg2addnclem  37731  itg2addnclem3  37733  itg2addnc  37734  itg2gt0cn  37735  ibladdnclem  37736  itgaddnclem1  37738  itgaddnclem2  37739  iblabsnclem  37743  iblabsnc  37744  iblmulc2nc  37745  ftc1cnnclem  37751  ftc1anclem4  37756  ftc1anclem7  37759  ftc1anclem8  37760  ftc1anc  37761  areacirclem5  37772  mettrifi  37817  isbnd3  37844  ssbnd  37848  cntotbnd  37856  heibor1lem  37869  bfplem2  37883  rrnequiv  37895  iccbnd  37900  lcmineqlem18  42159  lcmineqlem20  42161  aks4d1p1p3  42182  aks4d1p1p2  42183  aks4d1p1p4  42184  aks4d1p1p6  42186  aks4d1p1p7  42187  aks4d1p1p5  42188  aks4d1p1  42189  posbezout  42213  aks6d1c1  42229  aks6d1c2  42243  2np3bcnp1  42257  2ap1caineq  42258  sticksstones6  42264  sticksstones7  42265  sticksstones10  42268  sticksstones12a  42270  sticksstones12  42271  sticksstones22  42281  bcle2d  42292  aks6d1c7lem1  42293  readdridaddlidd  42376  resubeulem1  42493  resubeulem2  42494  resubeu  42495  readdsub  42502  reladdrsub  42503  resubidaddlidlem  42512  renegid2  42532  sn-it0e0  42534  sn-0tie0  42569  sn-addlt0d  42576  sn-addgt0d  42577  cnreeu  42608  dffltz  42752  fltnltalem  42780  fltnlta  42781  3cubeslem1  42801  pellexlem2  42947  pell1qrge1  42987  pell14qrgapw  42993  pellqrexplicit  42994  pellqrex  42996  pellfundge  42999  pellfundgt1  43000  rmspecfund  43026  rmxycomplete  43034  ltrmynn0  43065  jm2.24nn  43076  jm2.24  43080  fzmaxdif  43098  jm2.26lem3  43118  jm3.1lem2  43135  areaquad  43333  sqrtcvallem4  43756  sqrtcvallem5  43757  sqrtcval  43758  imo72b2lem0  44282  hashnzfzclim  44439  binomcxplemnotnn0  44473  zltlesub  45410  lt3addmuld  45426  absnpncan2d  45427  fperiodmullem  45428  lt4addmuld  45431  absnpncan3d  45432  supxrgelem  45460  supxrge  45461  ltadd12dd  45466  xralrple2  45477  infxr  45489  infleinflem2  45493  xralrple4  45495  xralrple3  45496  xrralrecnnle  45505  eliooshift  45630  iccshift  45642  iooshift  45646  iooiinicc  45666  iooiinioc  45680  fsumnncl  45696  climinf  45730  climsuselem1  45731  sumnnodd  45754  lptre2pt  45762  addlimc  45770  0ellimcdiv  45771  limclner  45773  climleltrp  45798  liminfltlem  45926  fperdvper  46041  dvdivbd  46045  dvbdfbdioolem2  46051  dvbdfbdioo  46052  ioodvbdlimc1lem1  46053  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvxpaek  46062  dvnmul  46065  iblsplit  46088  iblspltprt  46095  itgspltprt  46101  itgiccshift  46102  itgperiod  46103  itgsbtaddcnst  46104  stoweidlem1  46123  stoweidlem11  46133  stoweidlem13  46135  stoweidlem14  46136  stoweidlem20  46142  stoweidlem21  46143  stoweidlem26  46148  stoweidlem44  46166  stoweidlem60  46182  wallispilem3  46189  wallispilem4  46190  wallispilem5  46191  wallispi  46192  wallispi2lem1  46193  wallispi2lem2  46194  stirlinglem1  46196  stirlinglem3  46198  stirlinglem5  46200  stirlinglem6  46201  stirlinglem7  46202  stirlinglem10  46205  stirlinglem11  46206  stirlinglem12  46207  dirker2re  46214  dirkerval2  46216  dirkerre  46217  dirkerper  46218  dirkertrigeqlem1  46220  dirkertrigeqlem2  46221  dirkeritg  46224  dirkercncflem1  46225  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem4  46233  fourierdlem5  46234  fourierdlem6  46235  fourierdlem7  46236  fourierdlem9  46238  fourierdlem10  46239  fourierdlem18  46247  fourierdlem19  46248  fourierdlem20  46249  fourierdlem26  46255  fourierdlem28  46257  fourierdlem30  46259  fourierdlem35  46264  fourierdlem40  46269  fourierdlem41  46270  fourierdlem42  46271  fourierdlem47  46275  fourierdlem48  46276  fourierdlem49  46277  fourierdlem50  46278  fourierdlem51  46279  fourierdlem53  46281  fourierdlem57  46285  fourierdlem59  46287  fourierdlem60  46288  fourierdlem61  46289  fourierdlem63  46291  fourierdlem64  46292  fourierdlem65  46293  fourierdlem66  46294  fourierdlem68  46296  fourierdlem71  46299  fourierdlem72  46300  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem78  46306  fourierdlem79  46307  fourierdlem80  46308  fourierdlem81  46309  fourierdlem82  46310  fourierdlem83  46311  fourierdlem84  46312  fourierdlem87  46315  fourierdlem88  46316  fourierdlem89  46317  fourierdlem90  46318  fourierdlem91  46319  fourierdlem92  46320  fourierdlem93  46321  fourierdlem94  46322  fourierdlem95  46323  fourierdlem97  46325  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem112  46340  fourierdlem113  46341  sqwvfoura  46350  sqwvfourb  46351  fouriersw  46353  qndenserrnbllem  46416  ioorrnopnlem  46426  ioorrnopnxrlem  46428  sge0xaddlem1  46555  sge0xaddlem2  46556  omeiunltfirp  46641  carageniuncllem2  46644  hoidmv1lelem1  46713  hoidmv1lelem2  46714  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hoiqssbllem1  46744  hoiqssbllem2  46745  hoiqssbllem3  46746  hspmbllem2  46749  hspmbllem3  46750  ovolval5lem1  46774  iinhoiicclem  46795  iinhoiicc  46796  iunhoiioolem  46797  iccvonmbllem  46800  vonioolem1  46802  vonioolem2  46803  vonicclem1  46805  vonicclem2  46806  preimaleiinlt  46843  salpreimaltle  46848  smfaddlem1  46885  smfadd  46887  smflimlem3  46895  smflimlem4  46896  smflimlem6  46898  smfmullem1  46913  smfmullem2  46914  smfmullem3  46915  ormkglobd  46997  zm1nn  47426  requad01  47745  requad1  47746  requad2  47747  perfectALTVlem2  47846  nnsum4primesevenALTV  47925  bgoldbtbndlem2  47930  gpgvtxedg0  48187  gpgvtxedg1  48188  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx13starlem2  48196  dignn0flhalflem1  48740  affinecomb1  48827  resum2sqcl  48831  2sphere  48874  line2  48877  itsclc0lem1  48881  itscnhlc0yqe  48884  itsclquadb  48901  2itscp  48906  itscnhlinecirc02plem1  48907  itscnhlinecirc02plem3  48909  itscnhlinecirc02p  48910  inlinecirc02plem  48911  amgmwlem  49927