Theorem readdcld 11169

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

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

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

This theorem depends on definitions:  df-bi 209  df-an 398

This theorem is referenced by:  ltadd2  11245  readdcan  11315  addrid  11321  leadd1  11613  le2add  11627  lesub2  11640  lesub3d  11763  le2addd  11764  supaddc  12118  supadd  12119  cju  12150  nnne0  12206  div4p1lem1div2  12427  difgtsumgt  12485  eluzmn  12790  rpnnen1lem5  12926  addlelt  13053  xralrple  13152  xov1plusxeqvd  13446  zltaddlt1le  13453  elincfzoext  13673  fladdz  13779  2tnp1ge0ge0  13783  flhalf  13784  fldiv  13814  modaddb  13863  modaddmodup  13891  modaddmodlo  13892  addmodlteq  13903  discr1  14196  discr  14197  ccatalpha  14551  2cshw  14770  remim  15074  remullem  15085  01sqrexlem7  15205  absrele  15265  abstri  15288  abs3lem  15296  amgm2  15327  bhmafibid1  15425  mulcn2  15553  o1add  15571  o1sub  15573  lo1add  15584  caucvgrlem  15630  iseraltlem2  15640  iseraltlem3  15641  fsumabs  15759  o1fsum  15771  climcndslem2  15810  tanhlt1  16122  eirrlem  16166  ruclem1  16193  ruclem2  16194  ruclem3  16195  ltoddhalfle  16325  bitscmp  16402  sadcaddlem  16421  sadasslem  16434  smuval2  16446  iserodd  16801  prmreclem4  16885  4sqlem5  16908  4sqlem6  16909  4sqlem12  16922  4sqlem15  16925  4sqlem16  16926  prmgaplem7  17023  prmgaplem8  17024  2expltfac  17058  cshwshashlem2  17062  chfacfscmul0  22845  chfacfscmulgsum  22847  chfacfpmmul0  22849  chfacfpmmulgsum  22851  prdsxmetlem  24355  xblss2ps  24388  metustexhalf  24543  nrmmetd  24561  ngptgp  24623  nlmvscnlem2  24672  nlmvscnlem1  24673  nmotri  24726  nghmplusg  24727  blcvx  24785  iccntr  24809  icccmplem2  24811  reconnlem2  24815  metdcnlem  24824  metnrmlem3  24849  cnllycmp  24945  lebnumii  24955  tcphcphlem1  25224  ipcnlem2  25233  ipcnlem1  25234  csbren  25388  trirn  25389  minveclem2  25415  minveclem3b  25417  minveclem4  25421  ivthlem2  25441  ovolgelb  25469  ovollb2lem  25477  ovolunlem1a  25485  ovolunlem1  25486  ovolfiniun  25490  ovoliunlem1  25491  ovoliunlem2  25492  ovolshftlem1  25498  ovolscalem1  25502  ovolicopnf  25513  ismbl2  25516  nulmbl2  25525  unmbl  25526  voliunlem2  25540  ioombl1lem2  25548  ioombl1lem4  25550  ioombl1  25551  ioorcl2  25561  uniioombllem1  25570  uniioombllem3  25574  uniioombllem4  25575  uniioombllem5  25576  uniioombl  25578  opnmbllem  25590  volcn  25595  itg1addlem4  25688  mbfi1fseqlem4  25707  mbfi1fseqlem6  25709  itg2splitlem  25737  itg2split  25738  itg2monolem3  25741  itg2addlem  25747  ibladdlem  25809  itgaddlem1  25812  itgaddlem2  25813  iblabslem  25817  iblabs  25818  dvferm1lem  25973  dvferm2lem  25975  dvlip2  25984  lhop1lem  26002  lhop1  26003  lhop  26005  dvcnvrelem1  26006  dvcnvrelem2  26007  dvcnvre  26008  dvcvx  26009  dvfsumlem3  26017  dvfsumlem4  26018  dvfsum2  26023  ftc1lem4  26028  coemullem  26237  ulmbdd  26385  ulmcn  26386  ulmdvlem1  26387  radcnvle  26407  pserdvlem1  26414  pserdv  26416  abelthlem7  26425  pilem2  26439  pilem3  26440  cosordlem  26516  abslogle  26604  logccv  26649  cxpaddle  26738  ang180lem2  26796  heron  26824  atanlogaddlem  26899  atans2  26917  cxp2limlem  26961  scvxcvx  26971  jensenlem2  26973  amgmlem  26975  logdiflbnd  26980  harmonicbnd4  26996  fsumharmonic  26997  lgamgulmlem3  27016  lgamgulmlem4  27017  lgamgulmlem5  27018  lgamgulmlem6  27019  lgambdd  27022  lgamucov  27023  regamcl  27046  ftalem5  27062  efnnfsumcl  27088  efchtdvds  27144  chtublem  27196  chtub  27197  logfaclbnd  27207  perfectlem2  27215  bposlem7  27275  bposlem9  27277  lgsdirprm  27316  gausslemma2dlem1a  27350  2sqlem8  27411  chpchtlim  27464  vmadivsumb  27468  rplogsumlem1  27469  dchrisumlem2  27475  dchrvmasumlem2  27483  dchrvmasumiflem1  27486  dchrisum0re  27498  dchrisum0lem1b  27500  mulog2sumlem1  27519  mulog2sumlem2  27520  logsqvma2  27528  log2sumbnd  27529  selberglem2  27531  selbergb  27534  selberg2b  27537  chpdifbndlem1  27538  chpdifbndlem2  27539  selberg3lem2  27543  selberg3  27544  selberg4lem1  27545  selberg4  27546  pntrsumbnd2  27552  selberg3r  27554  selberg34r  27556  pntsf  27558  pntrlog2bndlem1  27562  pntrlog2bndlem2  27563  pntrlog2bndlem4  27565  pntrlog2bndlem5  27566  pntrlog2bndlem6  27568  pntrlog2bnd  27569  pntpbnd1a  27570  pntpbnd2  27572  pntibndlem2a  27575  pntibndlem2  27576  pntibndlem3  27577  pntlemg  27583  pntlemr  27587  pntlemk  27591  pntlemo  27592  pntlem3  27594  abvcxp  27600  padicabv  27615  ostth2lem2  27619  ostth3  27623  brbtwn2  28996  axsegconlem8  29015  axsegconlem10  29017  axpaschlem  29031  axpasch  29032  axeuclidlem  29053  axcontlem2  29056  crctcshwlkn0lem3  29902  crctcshwlkn0lem5  29904  vacn  30787  smcnlem  30790  ubthlem2  30964  minvecolem2  30968  minvecolem3  30969  minvecolem4  30973  minvecolem5  30974  nmoptrii  32187  hstle  32323  staddi  32339  stadd3i  32341  lt2addrd  32846  nndiffz1  32882  nexple  32940  wrdt2ind  33036  cshwrnid  33044  fsumrp0cl  33104  pmtrto1cl  33184  fzto1st  33188  psgnfzto1st  33190  constrresqrtcl  33973  cos9thpiminplylem1  33978  1smat1  34000  sqsscirc1  34104  cnre2csqlem  34106  tpr2rico  34108  dya2iocress  34470  dya2iocbrsiga  34471  dya2icobrsiga  34472  dya2icoseg  34473  dya2iocucvr  34480  sxbrsigalem2  34482  omssubaddlem  34495  fibp1  34597  ballotlemfc0  34689  ballotlemfcc  34690  ballotlemsgt1  34707  ballotlemsel1i  34709  plymulx0  34743  breprexplemc  34828  breprexp  34829  logdivsqrle  34846  resconn  35489  faclim  35989  dnizphlfeqhlf  36797  dnibndlem4  36802  dnibndlem6  36804  dnibndlem8  36806  dnibndlem9  36807  dnibndlem10  36808  dnibndlem11  36809  dnibndlem13  36811  dnibnd  36812  knoppcnlem4  36817  unblimceq0lem  36827  unblimceq0  36828  unbdqndv2lem1  36830  poimirlem29  38031  heicant  38037  opnmbllem0  38038  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  mbfposadd  38049  itg2addnclem  38053  itg2addnclem3  38055  itg2addnc  38056  itg2gt0cn  38057  ibladdnclem  38058  itgaddnclem1  38060  itgaddnclem2  38061  iblabsnclem  38065  iblabsnc  38066  iblmulc2nc  38067  ftc1cnnclem  38073  ftc1anclem4  38078  ftc1anclem7  38081  ftc1anclem8  38082  ftc1anc  38083  areacirclem5  38094  mettrifi  38139  isbnd3  38166  ssbnd  38170  cntotbnd  38178  heibor1lem  38191  bfplem2  38205  rrnequiv  38217  iccbnd  38222  lcmineqlem18  42546  lcmineqlem20  42548  aks4d1p1p3  42569  aks4d1p1p2  42570  aks4d1p1p4  42571  aks4d1p1p6  42573  aks4d1p1p7  42574  aks4d1p1p5  42575  aks4d1p1  42576  posbezout  42600  aks6d1c1  42616  aks6d1c2  42630  2np3bcnp1  42644  2ap1caineq  42645  sticksstones6  42651  sticksstones7  42652  sticksstones10  42655  sticksstones12a  42657  sticksstones12  42658  sticksstones22  42668  bcle2d  42679  aks6d1c7lem1  42680  readdridaddlidd  42756  resubeulem1  42867  resubeulem2  42868  resubeu  42869  readdsub  42876  reladdrsub  42877  resubidaddlidlem  42886  renegid2  42906  sn-it0e0  42908  redivdird  42954  sn-0tie0  42956  sn-addlt0d  42963  sn-addgt0d  42964  cnreeu  42995  dffltz  43099  fltnltalem  43127  fltnlta  43128  3cubeslem1  43148  pellexlem2  43290  pell1qrge1  43330  pell14qrgapw  43336  pellqrexplicit  43337  pellqrex  43339  pellfundge  43342  pellfundgt1  43343  rmspecfund  43369  rmxycomplete  43377  ltrmynn0  43408  jm2.24nn  43419  jm2.24  43423  fzmaxdif  43441  jm2.26lem3  43461  jm3.1lem2  43478  areaquad  43676  sqrtcvallem4  44098  sqrtcvallem5  44099  sqrtcval  44100  imo72b2lem0  44624  hashnzfzclim  44781  binomcxplemnotnn0  44815  zltlesub  45747  lt3addmuld  45763  absnpncan2d  45764  fperiodmullem  45765  lt4addmuld  45768  absnpncan3d  45769  supxrgelem  45796  supxrge  45797  ltadd12dd  45802  xralrple2  45813  infxr  45825  infleinflem2  45829  xralrple4  45831  xralrple3  45832  xrralrecnnle  45841  eliooshift  45965  iccshift  45977  iooshift  45981  iooiinicc  46001  iooiinioc  46015  fsumnncl  46031  climinf  46065  climsuselem1  46066  sumnnodd  46089  lptre2pt  46097  addlimc  46105  0ellimcdiv  46106  limclner  46108  climleltrp  46133  liminfltlem  46261  fperdvper  46376  dvdivbd  46380  dvbdfbdioolem2  46386  dvbdfbdioo  46387  ioodvbdlimc1lem1  46388  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  dvxpaek  46397  dvnmul  46400  iblsplit  46423  iblspltprt  46430  itgspltprt  46436  itgiccshift  46437  itgperiod  46438  itgsbtaddcnst  46439  stoweidlem1  46458  stoweidlem11  46468  stoweidlem13  46470  stoweidlem14  46471  stoweidlem20  46477  stoweidlem21  46478  stoweidlem26  46483  stoweidlem44  46501  stoweidlem60  46517  wallispilem3  46524  wallispilem4  46525  wallispilem5  46526  wallispi  46527  wallispi2lem1  46528  wallispi2lem2  46529  stirlinglem1  46531  stirlinglem3  46533  stirlinglem5  46535  stirlinglem6  46536  stirlinglem7  46537  stirlinglem10  46540  stirlinglem11  46541  stirlinglem12  46542  dirker2re  46549  dirkerval2  46551  dirkerre  46552  dirkerper  46553  dirkertrigeqlem1  46555  dirkertrigeqlem2  46556  dirkeritg  46559  dirkercncflem1  46560  dirkercncflem2  46561  dirkercncflem4  46563  fourierdlem4  46568  fourierdlem5  46569  fourierdlem6  46570  fourierdlem7  46571  fourierdlem9  46573  fourierdlem10  46574  fourierdlem18  46582  fourierdlem19  46583  fourierdlem20  46584  fourierdlem26  46590  fourierdlem28  46592  fourierdlem30  46594  fourierdlem35  46599  fourierdlem40  46604  fourierdlem41  46605  fourierdlem42  46606  fourierdlem47  46610  fourierdlem48  46611  fourierdlem49  46612  fourierdlem50  46613  fourierdlem51  46614  fourierdlem53  46616  fourierdlem57  46620  fourierdlem59  46622  fourierdlem60  46623  fourierdlem61  46624  fourierdlem63  46626  fourierdlem64  46627  fourierdlem65  46628  fourierdlem66  46629  fourierdlem68  46631  fourierdlem71  46634  fourierdlem72  46635  fourierdlem74  46637  fourierdlem75  46638  fourierdlem76  46639  fourierdlem78  46641  fourierdlem79  46642  fourierdlem80  46643  fourierdlem81  46644  fourierdlem82  46645  fourierdlem83  46646  fourierdlem84  46647  fourierdlem87  46650  fourierdlem88  46651  fourierdlem89  46652  fourierdlem90  46653  fourierdlem91  46654  fourierdlem92  46655  fourierdlem93  46656  fourierdlem94  46657  fourierdlem95  46658  fourierdlem97  46660  fourierdlem101  46664  fourierdlem103  46666  fourierdlem104  46667  fourierdlem111  46674  fourierdlem112  46675  fourierdlem113  46676  sqwvfoura  46685  sqwvfourb  46686  fouriersw  46688  qndenserrnbllem  46751  ioorrnopnlem  46761  ioorrnopnxrlem  46763  sge0xaddlem1  46890  sge0xaddlem2  46891  omeiunltfirp  46976  carageniuncllem2  46979  hoidmv1lelem1  47048  hoidmv1lelem2  47049  hoidmvlelem1  47052  hoidmvlelem2  47053  hoidmvlelem3  47054  hoidmvlelem4  47055  hoiqssbllem1  47079  hoiqssbllem2  47080  hoiqssbllem3  47081  hspmbllem2  47084  hspmbllem3  47085  ovolval5lem1  47109  iinhoiicclem  47130  iinhoiicc  47131  iunhoiioolem  47132  iccvonmbllem  47135  vonioolem1  47137  vonioolem2  47138  vonicclem1  47140  vonicclem2  47141  preimaleiinlt  47178  salpreimaltle  47183  smfaddlem1  47220  smfadd  47222  smflimlem3  47230  smflimlem4  47231  smflimlem6  47233  smfmullem1  47248  smfmullem2  47249  smfmullem3  47250  ormkglobd  47334  zm1nn  47779  requad01  48126  requad1  48127  requad2  48128  perfectALTVlem2  48227  nnsum4primesevenALTV  48306  bgoldbtbndlem2  48311  gpgvtxedg0  48568  gpgvtxedg1  48569  gpg5nbgrvtx03starlem2  48574  gpg5nbgrvtx13starlem2  48577  dignn0flhalflem1  49120  affinecomb1  49207  resum2sqcl  49211  2sphere  49254  line2  49257  itsclc0lem1  49261  itscnhlc0yqe  49264  itsclquadb  49281  2itscp  49286  itscnhlinecirc02plem1  49287  itscnhlinecirc02plem3  49289  itscnhlinecirc02p  49290  inlinecirc02plem  49291  amgmwlem  50306