Theorem readdcld 11163

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7353  ℝcr 11027   + caddc 11031

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

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

This theorem is referenced by:  ltadd2  11238  readdcan  11308  addrid  11314  leadd1  11606  le2add  11620  lesub2  11633  lesub3d  11756  le2addd  11757  supaddc  12110  supadd  12111  cju  12142  nnne0  12180  div4p1lem1div2  12397  difgtsumgt  12455  eluzmn  12760  rpnnen1lem5  12900  addlelt  13027  xralrple  13125  xov1plusxeqvd  13419  zltaddlt1le  13426  elincfzoext  13644  fladdz  13747  2tnp1ge0ge0  13751  flhalf  13752  fldiv  13782  modaddb  13831  modaddmodup  13859  modaddmodlo  13860  addmodlteq  13871  discr1  14164  discr  14165  ccatalpha  14518  2cshw  14737  remim  15042  remullem  15053  01sqrexlem7  15173  absrele  15233  abstri  15256  abs3lem  15264  amgm2  15295  bhmafibid1  15393  mulcn2  15521  o1add  15539  o1sub  15541  lo1add  15552  caucvgrlem  15598  iseraltlem2  15608  iseraltlem3  15609  fsumabs  15726  o1fsum  15738  climcndslem2  15775  tanhlt1  16087  eirrlem  16131  ruclem1  16158  ruclem2  16159  ruclem3  16160  ltoddhalfle  16290  bitscmp  16367  sadcaddlem  16386  sadasslem  16399  smuval2  16411  iserodd  16765  prmreclem4  16849  4sqlem5  16872  4sqlem6  16873  4sqlem12  16886  4sqlem15  16889  4sqlem16  16890  prmgaplem7  16987  prmgaplem8  16988  2expltfac  17022  cshwshashlem2  17026  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmul0  22765  chfacfpmmulgsum  22767  prdsxmetlem  24272  xblss2ps  24305  metustexhalf  24460  nrmmetd  24478  ngptgp  24540  nlmvscnlem2  24589  nlmvscnlem1  24590  nmotri  24643  nghmplusg  24644  blcvx  24702  iccntr  24726  icccmplem2  24728  reconnlem2  24732  metdcnlem  24741  metnrmlem3  24766  cnllycmp  24871  lebnumii  24881  tcphcphlem1  25151  ipcnlem2  25160  ipcnlem1  25161  csbren  25315  trirn  25316  minveclem2  25342  minveclem3b  25344  minveclem4  25348  ivthlem2  25369  ovolgelb  25397  ovollb2lem  25405  ovolunlem1a  25413  ovolunlem1  25414  ovolfiniun  25418  ovoliunlem1  25419  ovoliunlem2  25420  ovolshftlem1  25426  ovolscalem1  25430  ovolicopnf  25441  ismbl2  25444  nulmbl2  25453  unmbl  25454  voliunlem2  25468  ioombl1lem2  25476  ioombl1lem4  25478  ioombl1  25479  ioorcl2  25489  uniioombllem1  25498  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombl  25506  opnmbllem  25518  volcn  25523  itg1addlem4  25616  mbfi1fseqlem4  25635  mbfi1fseqlem6  25637  itg2splitlem  25665  itg2split  25666  itg2monolem3  25669  itg2addlem  25675  ibladdlem  25737  itgaddlem1  25740  itgaddlem2  25741  iblabslem  25745  iblabs  25746  dvferm1lem  25904  dvferm2lem  25906  dvlip2  25916  lhop1lem  25934  lhop1  25935  lhop  25937  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcnvre  25940  dvcvx  25941  dvfsumlem3  25951  dvfsumlem4  25952  dvfsum2  25957  ftc1lem4  25962  coemullem  26171  ulmbdd  26323  ulmcn  26324  ulmdvlem1  26325  radcnvle  26345  pserdvlem1  26353  pserdv  26355  abelthlem7  26364  pilem2  26378  pilem3  26379  cosordlem  26455  abslogle  26543  logccv  26588  cxpaddle  26678  ang180lem2  26736  heron  26764  atanlogaddlem  26839  atans2  26857  cxp2limlem  26902  scvxcvx  26912  jensenlem2  26914  amgmlem  26916  logdiflbnd  26921  harmonicbnd4  26937  fsumharmonic  26938  lgamgulmlem3  26957  lgamgulmlem4  26958  lgamgulmlem5  26959  lgamgulmlem6  26960  lgambdd  26963  lgamucov  26964  regamcl  26987  ftalem5  27003  efnnfsumcl  27029  efchtdvds  27085  chtublem  27138  chtub  27139  logfaclbnd  27149  perfectlem2  27157  bposlem7  27217  bposlem9  27219  lgsdirprm  27258  gausslemma2dlem1a  27292  2sqlem8  27353  chpchtlim  27406  vmadivsumb  27410  rplogsumlem1  27411  dchrisumlem2  27417  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  dchrisum0re  27440  dchrisum0lem1b  27442  mulog2sumlem1  27461  mulog2sumlem2  27462  logsqvma2  27470  log2sumbnd  27471  selberglem2  27473  selbergb  27476  selberg2b  27479  chpdifbndlem1  27480  chpdifbndlem2  27481  selberg3lem2  27485  selberg3  27486  selberg4lem1  27487  selberg4  27488  pntrsumbnd2  27494  selberg3r  27496  selberg34r  27498  pntsf  27500  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntrlog2bnd  27511  pntpbnd1a  27512  pntpbnd2  27514  pntibndlem2a  27517  pntibndlem2  27518  pntibndlem3  27519  pntlemg  27525  pntlemr  27529  pntlemk  27533  pntlemo  27534  pntlem3  27536  abvcxp  27542  padicabv  27557  ostth2lem2  27561  ostth3  27565  brbtwn2  28868  axsegconlem8  28887  axsegconlem10  28889  axpaschlem  28903  axpasch  28904  axeuclidlem  28925  axcontlem2  28928  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  vacn  30656  smcnlem  30659  ubthlem2  30833  minvecolem2  30837  minvecolem3  30838  minvecolem4  30842  minvecolem5  30843  nmoptrii  32056  hstle  32192  staddi  32208  stadd3i  32210  lt2addrd  32707  nndiffz1  32742  nexple  32802  wrdt2ind  32908  cshwrnid  32916  fsumrp0cl  32988  pmtrto1cl  33054  fzto1st  33058  psgnfzto1st  33060  constrresqrtcl  33743  cos9thpiminplylem1  33748  1smat1  33770  sqsscirc1  33874  cnre2csqlem  33876  tpr2rico  33878  dya2iocress  34241  dya2iocbrsiga  34242  dya2icobrsiga  34243  dya2icoseg  34244  dya2iocucvr  34251  sxbrsigalem2  34253  omssubaddlem  34266  fibp1  34368  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemsgt1  34478  ballotlemsel1i  34480  plymulx0  34514  breprexplemc  34599  breprexp  34600  logdivsqrle  34617  resconn  35218  faclim  35718  dnizphlfeqhlf  36449  dnibndlem4  36454  dnibndlem6  36456  dnibndlem8  36458  dnibndlem9  36459  dnibndlem10  36460  dnibndlem11  36461  dnibndlem13  36463  dnibnd  36464  knoppcnlem4  36469  unblimceq0lem  36479  unblimceq0  36480  unbdqndv2lem1  36482  poimirlem29  37628  heicant  37634  opnmbllem0  37635  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  mbfposadd  37646  itg2addnclem  37650  itg2addnclem3  37652  itg2addnc  37653  itg2gt0cn  37654  ibladdnclem  37655  itgaddnclem1  37657  itgaddnclem2  37658  iblabsnclem  37662  iblabsnc  37663  iblmulc2nc  37664  ftc1cnnclem  37670  ftc1anclem4  37675  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  areacirclem5  37691  mettrifi  37736  isbnd3  37763  ssbnd  37767  cntotbnd  37775  heibor1lem  37788  bfplem2  37802  rrnequiv  37814  iccbnd  37819  lcmineqlem18  42019  lcmineqlem20  42021  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  posbezout  42073  aks6d1c1  42089  aks6d1c2  42103  2np3bcnp1  42117  2ap1caineq  42118  sticksstones6  42124  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  bcle2d  42152  aks6d1c7lem1  42153  readdridaddlidd  42231  resubeulem1  42348  resubeulem2  42349  resubeu  42350  readdsub  42357  reladdrsub  42358  resubidaddlidlem  42367  renegid2  42387  sn-it0e0  42389  sn-0tie0  42424  sn-addlt0d  42431  sn-addgt0d  42432  cnreeu  42463  dffltz  42607  fltnltalem  42635  fltnlta  42636  3cubeslem1  42657  pellexlem2  42803  pell1qrge1  42843  pell14qrgapw  42849  pellqrexplicit  42850  pellqrex  42852  pellfundge  42855  pellfundgt1  42856  rmspecfund  42882  rmxycomplete  42890  ltrmynn0  42921  jm2.24nn  42932  jm2.24  42936  fzmaxdif  42954  jm2.26lem3  42974  jm3.1lem2  42991  areaquad  43189  sqrtcvallem4  43612  sqrtcvallem5  43613  sqrtcval  43614  imo72b2lem0  44138  hashnzfzclim  44295  binomcxplemnotnn0  44329  zltlesub  45267  lt3addmuld  45283  absnpncan2d  45284  fperiodmullem  45285  lt4addmuld  45288  absnpncan3d  45289  supxrgelem  45317  supxrge  45318  ltadd12dd  45323  xralrple2  45334  infxr  45347  infleinflem2  45351  xralrple4  45353  xralrple3  45354  xrralrecnnle  45363  eliooshift  45488  iccshift  45500  iooshift  45504  iooiinicc  45524  iooiinioc  45538  fsumnncl  45554  climinf  45588  climsuselem1  45589  sumnnodd  45612  lptre2pt  45622  addlimc  45630  0ellimcdiv  45631  limclner  45633  climleltrp  45658  liminfltlem  45786  fperdvper  45901  dvdivbd  45905  dvbdfbdioolem2  45911  dvbdfbdioo  45912  ioodvbdlimc1lem1  45913  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvxpaek  45922  dvnmul  45925  iblsplit  45948  iblspltprt  45955  itgspltprt  45961  itgiccshift  45962  itgperiod  45963  itgsbtaddcnst  45964  stoweidlem1  45983  stoweidlem11  45993  stoweidlem13  45995  stoweidlem14  45996  stoweidlem20  46002  stoweidlem21  46003  stoweidlem26  46008  stoweidlem44  46026  stoweidlem60  46042  wallispilem3  46049  wallispilem4  46050  wallispilem5  46051  wallispi  46052  wallispi2lem1  46053  wallispi2lem2  46054  stirlinglem1  46056  stirlinglem3  46058  stirlinglem5  46060  stirlinglem6  46061  stirlinglem7  46062  stirlinglem10  46065  stirlinglem11  46066  stirlinglem12  46067  dirker2re  46074  dirkerval2  46076  dirkerre  46077  dirkerper  46078  dirkertrigeqlem1  46080  dirkertrigeqlem2  46081  dirkeritg  46084  dirkercncflem1  46085  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem4  46093  fourierdlem5  46094  fourierdlem6  46095  fourierdlem7  46096  fourierdlem9  46098  fourierdlem10  46099  fourierdlem18  46107  fourierdlem19  46108  fourierdlem20  46109  fourierdlem26  46115  fourierdlem28  46117  fourierdlem30  46119  fourierdlem35  46124  fourierdlem40  46129  fourierdlem41  46130  fourierdlem42  46131  fourierdlem47  46135  fourierdlem48  46136  fourierdlem49  46137  fourierdlem50  46138  fourierdlem51  46139  fourierdlem53  46141  fourierdlem57  46145  fourierdlem59  46147  fourierdlem60  46148  fourierdlem61  46149  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem66  46154  fourierdlem68  46156  fourierdlem71  46159  fourierdlem72  46160  fourierdlem74  46162  fourierdlem75  46163  fourierdlem76  46164  fourierdlem78  46166  fourierdlem79  46167  fourierdlem80  46168  fourierdlem81  46169  fourierdlem82  46170  fourierdlem83  46171  fourierdlem84  46172  fourierdlem87  46175  fourierdlem88  46176  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem92  46180  fourierdlem93  46181  fourierdlem94  46182  fourierdlem95  46183  fourierdlem97  46185  fourierdlem101  46189  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  fourierdlem112  46200  fourierdlem113  46201  sqwvfoura  46210  sqwvfourb  46211  fouriersw  46213  qndenserrnbllem  46276  ioorrnopnlem  46286  ioorrnopnxrlem  46288  sge0xaddlem1  46415  sge0xaddlem2  46416  omeiunltfirp  46501  carageniuncllem2  46504  hoidmv1lelem1  46573  hoidmv1lelem2  46574  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hoiqssbllem1  46604  hoiqssbllem2  46605  hoiqssbllem3  46606  hspmbllem2  46609  hspmbllem3  46610  ovolval5lem1  46634  iinhoiicclem  46655  iinhoiicc  46656  iunhoiioolem  46657  iccvonmbllem  46660  vonioolem1  46662  vonioolem2  46663  vonicclem1  46665  vonicclem2  46666  preimaleiinlt  46703  salpreimaltle  46708  smfaddlem1  46745  smfadd  46747  smflimlem3  46755  smflimlem4  46756  smflimlem6  46758  smfmullem1  46773  smfmullem2  46774  smfmullem3  46775  ormkglobd  46857  zm1nn  47287  requad01  47606  requad1  47607  requad2  47608  perfectALTVlem2  47707  nnsum4primesevenALTV  47786  bgoldbtbndlem2  47791  gpgvtxedg0  48048  gpgvtxedg1  48049  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx13starlem2  48057  dignn0flhalflem1  48601  affinecomb1  48688  resum2sqcl  48692  2sphere  48735  line2  48738  itsclc0lem1  48742  itscnhlc0yqe  48745  itsclquadb  48762  2itscp  48767  itscnhlinecirc02plem1  48768  itscnhlinecirc02plem3  48770  itscnhlinecirc02p  48771  inlinecirc02plem  48772  amgmwlem  49788