Theorem readdcld 11262

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126   + caddc 11130

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

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

This theorem is referenced by:  ltadd2  11337  readdcan  11407  addrid  11413  leadd1  11703  le2add  11717  lesub2  11730  lesub3d  11853  le2addd  11854  supaddc  12207  supadd  12208  cju  12234  nnne0  12272  div4p1lem1div2  12494  difgtsumgt  12552  eluzmn  12857  rpnnen1lem5  12995  addlelt  13121  xralrple  13219  xov1plusxeqvd  13513  zltaddlt1le  13520  elincfzoext  13737  fladdz  13840  2tnp1ge0ge0  13844  flhalf  13845  fldiv  13875  modaddmodup  13950  modaddmodlo  13951  addmodlteq  13962  discr1  14255  discr  14256  ccatalpha  14609  2cshw  14829  remim  15134  remullem  15145  01sqrexlem7  15265  absrele  15325  abstri  15347  abs3lem  15355  amgm2  15386  bhmafibid1  15482  mulcn2  15610  o1add  15628  o1sub  15630  lo1add  15641  caucvgrlem  15687  iseraltlem2  15697  iseraltlem3  15698  fsumabs  15815  o1fsum  15827  climcndslem2  15864  tanhlt1  16176  eirrlem  16220  ruclem1  16247  ruclem2  16248  ruclem3  16249  ltoddhalfle  16378  bitscmp  16455  sadcaddlem  16474  sadasslem  16487  smuval2  16499  iserodd  16853  prmreclem4  16937  4sqlem5  16960  4sqlem6  16961  4sqlem12  16974  4sqlem15  16977  4sqlem16  16978  prmgaplem7  17075  prmgaplem8  17076  2expltfac  17110  cshwshashlem2  17114  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmul0  22798  chfacfpmmulgsum  22800  prdsxmetlem  24305  xblss2ps  24338  metustexhalf  24493  nrmmetd  24511  ngptgp  24573  nlmvscnlem2  24622  nlmvscnlem1  24623  nmotri  24676  nghmplusg  24677  blcvx  24735  iccntr  24759  icccmplem2  24761  reconnlem2  24765  metdcnlem  24774  metnrmlem3  24799  cnllycmp  24904  lebnumii  24914  tcphcphlem1  25185  ipcnlem2  25194  ipcnlem1  25195  csbren  25349  trirn  25350  minveclem2  25376  minveclem3b  25378  minveclem4  25382  ivthlem2  25403  ovolgelb  25431  ovollb2lem  25439  ovolunlem1a  25447  ovolunlem1  25448  ovolfiniun  25452  ovoliunlem1  25453  ovoliunlem2  25454  ovolshftlem1  25460  ovolscalem1  25464  ovolicopnf  25475  ismbl2  25478  nulmbl2  25487  unmbl  25488  voliunlem2  25502  ioombl1lem2  25510  ioombl1lem4  25512  ioombl1  25513  ioorcl2  25523  uniioombllem1  25532  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  uniioombl  25540  opnmbllem  25552  volcn  25557  itg1addlem4  25650  mbfi1fseqlem4  25669  mbfi1fseqlem6  25671  itg2splitlem  25699  itg2split  25700  itg2monolem3  25703  itg2addlem  25709  ibladdlem  25771  itgaddlem1  25774  itgaddlem2  25775  iblabslem  25779  iblabs  25780  dvferm1lem  25938  dvferm2lem  25940  dvlip2  25950  lhop1lem  25968  lhop1  25969  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvcvx  25975  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  ftc1lem4  25996  coemullem  26205  ulmbdd  26357  ulmcn  26358  ulmdvlem1  26359  radcnvle  26379  pserdvlem1  26387  pserdv  26389  abelthlem7  26398  pilem2  26412  pilem3  26413  cosordlem  26489  abslogle  26577  logccv  26622  cxpaddle  26712  ang180lem2  26770  heron  26798  atanlogaddlem  26873  atans2  26891  cxp2limlem  26936  scvxcvx  26946  jensenlem2  26948  amgmlem  26950  logdiflbnd  26955  harmonicbnd4  26971  fsumharmonic  26972  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgambdd  26997  lgamucov  26998  regamcl  27021  ftalem5  27037  efnnfsumcl  27063  efchtdvds  27119  chtublem  27172  chtub  27173  logfaclbnd  27183  perfectlem2  27191  bposlem7  27251  bposlem9  27253  lgsdirprm  27292  gausslemma2dlem1a  27326  2sqlem8  27387  chpchtlim  27440  vmadivsumb  27444  rplogsumlem1  27445  dchrisumlem2  27451  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  dchrisum0re  27474  dchrisum0lem1b  27476  mulog2sumlem1  27495  mulog2sumlem2  27496  logsqvma2  27504  log2sumbnd  27505  selberglem2  27507  selbergb  27510  selberg2b  27513  chpdifbndlem1  27514  chpdifbndlem2  27515  selberg3lem2  27519  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrsumbnd2  27528  selberg3r  27530  selberg34r  27532  pntsf  27534  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem2a  27551  pntibndlem2  27552  pntibndlem3  27553  pntlemg  27559  pntlemr  27563  pntlemk  27567  pntlemo  27568  pntlem3  27570  abvcxp  27576  padicabv  27591  ostth2lem2  27595  ostth3  27599  brbtwn2  28830  axsegconlem8  28849  axsegconlem10  28851  axpaschlem  28865  axpasch  28866  axeuclidlem  28887  axcontlem2  28890  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  vacn  30621  smcnlem  30624  ubthlem2  30798  minvecolem2  30802  minvecolem3  30803  minvecolem4  30807  minvecolem5  30808  nmoptrii  32021  hstle  32157  staddi  32173  stadd3i  32175  lt2addrd  32674  nndiffz1  32709  nexple  32769  wrdt2ind  32875  cshwrnid  32883  fsumrp0cl  32962  pmtrto1cl  33056  fzto1st  33060  psgnfzto1st  33062  constrresqrtcl  33757  cos9thpiminplylem1  33762  1smat1  33781  sqsscirc1  33885  cnre2csqlem  33887  tpr2rico  33889  dya2iocress  34252  dya2iocbrsiga  34253  dya2icobrsiga  34254  dya2icoseg  34255  dya2iocucvr  34262  sxbrsigalem2  34264  omssubaddlem  34277  fibp1  34379  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemsgt1  34489  ballotlemsel1i  34491  plymulx0  34525  breprexplemc  34610  breprexp  34611  logdivsqrle  34628  resconn  35214  faclim  35709  dnizphlfeqhlf  36440  dnibndlem4  36445  dnibndlem6  36447  dnibndlem8  36449  dnibndlem9  36450  dnibndlem10  36451  dnibndlem11  36452  dnibndlem13  36454  dnibnd  36455  knoppcnlem4  36460  unblimceq0lem  36470  unblimceq0  36471  unbdqndv2lem1  36473  poimirlem29  37619  heicant  37625  opnmbllem0  37626  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  mbfposadd  37637  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ibladdnclem  37646  itgaddnclem1  37648  itgaddnclem2  37649  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  ftc1cnnclem  37661  ftc1anclem4  37666  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  areacirclem5  37682  mettrifi  37727  isbnd3  37754  ssbnd  37758  cntotbnd  37766  heibor1lem  37779  bfplem2  37793  rrnequiv  37805  iccbnd  37810  lcmineqlem18  42005  lcmineqlem20  42007  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  posbezout  42059  aks6d1c1  42075  aks6d1c2  42089  2np3bcnp1  42103  2ap1caineq  42104  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  bcle2d  42138  aks6d1c7lem1  42139  metakunt29  42192  2xp3dxp2ge1d  42200  factwoffsmonot  42201  readdridaddlidd  42256  resubeulem1  42365  resubeulem2  42366  resubeu  42367  readdsub  42374  reladdrsub  42375  resubidaddlidlem  42384  renegid2  42403  sn-it0e0  42405  sn-0tie0  42429  sn-addlt0d  42436  sn-addgt0d  42437  cnreeu  42460  dffltz  42604  fltnltalem  42632  fltnlta  42633  3cubeslem1  42654  pellexlem2  42800  pell1qrge1  42840  pell14qrgapw  42846  pellqrexplicit  42847  pellqrex  42849  pellfundge  42852  pellfundgt1  42853  rmspecfund  42879  rmxycomplete  42888  ltrmynn0  42919  jm2.24nn  42930  jm2.24  42934  fzmaxdif  42952  jm2.26lem3  42972  jm3.1lem2  42989  areaquad  43187  sqrtcvallem4  43610  sqrtcvallem5  43611  sqrtcval  43612  imo72b2lem0  44136  hashnzfzclim  44294  binomcxplemnotnn0  44328  zltlesub  45262  lt3addmuld  45278  absnpncan2d  45279  fperiodmullem  45280  lt4addmuld  45283  absnpncan3d  45284  supxrgelem  45312  supxrge  45313  ltadd12dd  45318  xralrple2  45329  infxr  45342  infleinflem2  45346  xralrple4  45348  xralrple3  45349  xrralrecnnle  45358  eliooshift  45483  iccshift  45495  iooshift  45499  iooiinicc  45519  iooiinioc  45533  fsumnncl  45549  climinf  45583  climsuselem1  45584  sumnnodd  45607  lptre2pt  45617  addlimc  45625  0ellimcdiv  45626  limclner  45628  climleltrp  45653  liminfltlem  45781  fperdvper  45896  dvdivbd  45900  dvbdfbdioolem2  45906  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvxpaek  45917  dvnmul  45920  iblsplit  45943  iblspltprt  45950  itgspltprt  45956  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem1  45978  stoweidlem11  45988  stoweidlem13  45990  stoweidlem14  45991  stoweidlem20  45997  stoweidlem21  45998  stoweidlem26  46003  stoweidlem44  46021  stoweidlem60  46037  wallispilem3  46044  wallispilem4  46045  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem1  46051  stirlinglem3  46053  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  dirker2re  46069  dirkerval2  46071  dirkerre  46072  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkeritg  46079  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem4  46088  fourierdlem5  46089  fourierdlem6  46090  fourierdlem7  46091  fourierdlem9  46093  fourierdlem10  46094  fourierdlem18  46102  fourierdlem19  46103  fourierdlem20  46104  fourierdlem26  46110  fourierdlem28  46112  fourierdlem30  46114  fourierdlem35  46119  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem47  46130  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem53  46136  fourierdlem57  46140  fourierdlem59  46142  fourierdlem60  46143  fourierdlem61  46144  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem66  46149  fourierdlem68  46151  fourierdlem71  46154  fourierdlem72  46155  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem80  46163  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem87  46170  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem94  46177  fourierdlem95  46178  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  qndenserrnbllem  46271  ioorrnopnlem  46281  ioorrnopnxrlem  46283  sge0xaddlem1  46410  sge0xaddlem2  46411  omeiunltfirp  46496  carageniuncllem2  46499  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoiqssbllem1  46599  hoiqssbllem2  46600  hoiqssbllem3  46601  hspmbllem2  46604  hspmbllem3  46605  ovolval5lem1  46629  iinhoiicclem  46650  iinhoiicc  46651  iunhoiioolem  46652  iccvonmbllem  46655  vonioolem1  46657  vonioolem2  46658  vonicclem1  46660  vonicclem2  46661  preimaleiinlt  46698  salpreimaltle  46703  smfaddlem1  46740  smfadd  46742  smflimlem3  46750  smflimlem4  46751  smflimlem6  46753  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  ormkglobd  46852  zm1nn  47279  requad01  47583  requad1  47584  requad2  47585  perfectALTVlem2  47684  nnsum4primesevenALTV  47763  bgoldbtbndlem2  47768  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  dignn0flhalflem1  48543  affinecomb1  48630  resum2sqcl  48634  2sphere  48677  line2  48680  itsclc0lem1  48684  itscnhlc0yqe  48687  itsclquadb  48704  2itscp  48709  itscnhlinecirc02plem1  48710  itscnhlinecirc02plem3  48712  itscnhlinecirc02p  48713  inlinecirc02plem  48714  amgmwlem  49614