Theorem readdcld 11290

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154   + caddc 11158

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

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

This theorem is referenced by:  ltadd2  11365  readdcan  11435  addrid  11441  leadd1  11731  le2add  11745  lesub2  11758  lesub3d  11881  supaddc  12235  supadd  12236  cju  12262  nnne0  12300  div4p1lem1div2  12521  difgtsumgt  12579  eluzmn  12885  rpnnen1lem5  13023  addlelt  13149  xralrple  13247  xov1plusxeqvd  13538  zltaddlt1le  13545  elincfzoext  13762  fladdz  13865  2tnp1ge0ge0  13869  flhalf  13870  fldiv  13900  modaddmodup  13975  modaddmodlo  13976  addmodlteq  13987  discr1  14278  discr  14279  ccatalpha  14631  2cshw  14851  remim  15156  remullem  15167  01sqrexlem7  15287  absrele  15347  abstri  15369  abs3lem  15377  amgm2  15408  bhmafibid1  15504  mulcn2  15632  o1add  15650  o1sub  15652  lo1add  15663  caucvgrlem  15709  iseraltlem2  15719  iseraltlem3  15720  fsumabs  15837  o1fsum  15849  climcndslem2  15886  tanhlt1  16196  eirrlem  16240  ruclem1  16267  ruclem2  16268  ruclem3  16269  ltoddhalfle  16398  bitscmp  16475  sadcaddlem  16494  sadasslem  16507  smuval2  16519  iserodd  16873  prmreclem4  16957  4sqlem5  16980  4sqlem6  16981  4sqlem12  16994  4sqlem15  16997  4sqlem16  16998  prmgaplem7  17095  prmgaplem8  17096  2expltfac  17130  cshwshashlem2  17134  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulgsum  22870  prdsxmetlem  24378  xblss2ps  24411  metustexhalf  24569  nrmmetd  24587  ngptgp  24649  nlmvscnlem2  24706  nlmvscnlem1  24707  nmotri  24760  nghmplusg  24761  blcvx  24819  iccntr  24843  icccmplem2  24845  reconnlem2  24849  metdcnlem  24858  metnrmlem3  24883  cnllycmp  24988  lebnumii  24998  tcphcphlem1  25269  ipcnlem2  25278  ipcnlem1  25279  csbren  25433  trirn  25434  minveclem2  25460  minveclem3b  25462  minveclem4  25466  ivthlem2  25487  ovolgelb  25515  ovollb2lem  25523  ovolunlem1a  25531  ovolunlem1  25532  ovolfiniun  25536  ovoliunlem1  25537  ovoliunlem2  25538  ovolshftlem1  25544  ovolscalem1  25548  ovolicopnf  25559  ismbl2  25562  nulmbl2  25571  unmbl  25572  voliunlem2  25586  ioombl1lem2  25594  ioombl1lem4  25596  ioombl1  25597  ioorcl2  25607  uniioombllem1  25616  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombl  25624  opnmbllem  25636  volcn  25641  itg1addlem4  25734  mbfi1fseqlem4  25753  mbfi1fseqlem6  25755  itg2splitlem  25783  itg2split  25784  itg2monolem3  25787  itg2addlem  25793  ibladdlem  25855  itgaddlem1  25858  itgaddlem2  25859  iblabslem  25863  iblabs  25864  dvferm1lem  26022  dvferm2lem  26024  dvlip2  26034  lhop1lem  26052  lhop1  26053  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  dvcvx  26059  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  ftc1lem4  26080  coemullem  26289  ulmbdd  26441  ulmcn  26442  ulmdvlem1  26443  radcnvle  26463  pserdvlem1  26471  pserdv  26473  abelthlem7  26482  pilem2  26496  pilem3  26497  cosordlem  26572  abslogle  26660  logccv  26705  cxpaddle  26795  ang180lem2  26853  heron  26881  atanlogaddlem  26956  atans2  26974  cxp2limlem  27019  scvxcvx  27029  jensenlem2  27031  amgmlem  27033  logdiflbnd  27038  harmonicbnd4  27054  fsumharmonic  27055  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgambdd  27080  lgamucov  27081  regamcl  27104  ftalem5  27120  efnnfsumcl  27146  efchtdvds  27202  chtublem  27255  chtub  27256  logfaclbnd  27266  perfectlem2  27274  bposlem7  27334  bposlem9  27336  lgsdirprm  27375  gausslemma2dlem1a  27409  2sqlem8  27470  chpchtlim  27523  vmadivsumb  27527  rplogsumlem1  27528  dchrisumlem2  27534  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0re  27557  dchrisum0lem1b  27559  mulog2sumlem1  27578  mulog2sumlem2  27579  logsqvma2  27587  log2sumbnd  27588  selberglem2  27590  selbergb  27593  selberg2b  27596  chpdifbndlem1  27597  chpdifbndlem2  27598  selberg3lem2  27602  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrsumbnd2  27611  selberg3r  27613  selberg34r  27615  pntsf  27617  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem2a  27634  pntibndlem2  27635  pntibndlem3  27636  pntlemg  27642  pntlemr  27646  pntlemk  27650  pntlemo  27651  pntlem3  27653  abvcxp  27659  padicabv  27674  ostth2lem2  27678  ostth3  27682  brbtwn2  28920  axsegconlem8  28939  axsegconlem10  28941  axpaschlem  28955  axpasch  28956  axeuclidlem  28977  axcontlem2  28980  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  vacn  30713  smcnlem  30716  ubthlem2  30890  minvecolem2  30894  minvecolem3  30895  minvecolem4  30899  minvecolem5  30900  nmoptrii  32113  hstle  32249  staddi  32265  stadd3i  32267  lt2addrd  32755  nndiffz1  32788  nexple  32833  wrdt2ind  32938  cshwrnid  32946  fsumrp0cl  33026  pmtrto1cl  33119  fzto1st  33123  psgnfzto1st  33125  1smat1  33803  sqsscirc1  33907  cnre2csqlem  33909  tpr2rico  33911  dya2iocress  34276  dya2iocbrsiga  34277  dya2icobrsiga  34278  dya2icoseg  34279  dya2iocucvr  34286  sxbrsigalem2  34288  omssubaddlem  34301  fibp1  34403  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsgt1  34513  ballotlemsel1i  34515  plymulx0  34562  breprexplemc  34647  breprexp  34648  logdivsqrle  34665  resconn  35251  faclim  35746  dnizphlfeqhlf  36477  dnibndlem4  36482  dnibndlem6  36484  dnibndlem8  36486  dnibndlem9  36487  dnibndlem10  36488  dnibndlem11  36489  dnibndlem13  36491  dnibnd  36492  knoppcnlem4  36497  unblimceq0lem  36507  unblimceq0  36508  unbdqndv2lem1  36510  poimirlem29  37656  heicant  37662  opnmbllem0  37663  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  mbfposadd  37674  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem1  37685  itgaddnclem2  37686  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  ftc1cnnclem  37698  ftc1anclem4  37703  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  areacirclem5  37719  mettrifi  37764  isbnd3  37791  ssbnd  37795  cntotbnd  37803  heibor1lem  37816  bfplem2  37830  rrnequiv  37842  iccbnd  37847  lcmineqlem18  42047  lcmineqlem20  42049  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  posbezout  42101  aks6d1c1  42117  aks6d1c2  42131  2np3bcnp1  42145  2ap1caineq  42146  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  bcle2d  42180  aks6d1c7lem1  42181  metakunt29  42234  2xp3dxp2ge1d  42242  factwoffsmonot  42243  readdridaddlidd  42299  resubeulem1  42405  resubeulem2  42406  resubeu  42407  readdsub  42414  reladdrsub  42415  resubidaddlidlem  42424  renegid2  42443  sn-it0e0  42445  sn-0tie0  42469  sn-addlt0d  42476  sn-addgt0d  42477  cnreeu  42500  dffltz  42644  fltnltalem  42672  fltnlta  42673  3cubeslem1  42695  pellexlem2  42841  pell1qrge1  42881  pell14qrgapw  42887  pellqrexplicit  42888  pellqrex  42890  pellfundge  42893  pellfundgt1  42894  rmspecfund  42920  rmxycomplete  42929  ltrmynn0  42960  jm2.24nn  42971  jm2.24  42975  fzmaxdif  42993  jm2.26lem3  43013  jm3.1lem2  43030  areaquad  43228  sqrtcvallem4  43652  sqrtcvallem5  43653  sqrtcval  43654  imo72b2lem0  44178  hashnzfzclim  44341  binomcxplemnotnn0  44375  zltlesub  45297  lt3addmuld  45313  absnpncan2d  45314  fperiodmullem  45315  lt4addmuld  45318  absnpncan3d  45319  leadd12dd  45328  supxrgelem  45348  supxrge  45349  ltadd12dd  45354  xralrple2  45365  infxr  45378  infleinflem2  45382  xralrple4  45384  xralrple3  45385  xrralrecnnle  45394  eliooshift  45519  iccshift  45531  iooshift  45535  iooiinicc  45555  iooiinioc  45569  fsumnncl  45587  climinf  45621  climsuselem1  45622  sumnnodd  45645  lptre2pt  45655  addlimc  45663  0ellimcdiv  45664  limclner  45666  climleltrp  45691  liminfltlem  45819  fperdvper  45934  dvdivbd  45938  dvbdfbdioolem2  45944  dvbdfbdioo  45945  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvxpaek  45955  dvnmul  45958  iblsplit  45981  iblspltprt  45988  itgspltprt  45994  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem1  46016  stoweidlem11  46026  stoweidlem13  46028  stoweidlem14  46029  stoweidlem20  46035  stoweidlem21  46036  stoweidlem26  46041  stoweidlem44  46059  stoweidlem60  46075  wallispilem3  46082  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem1  46089  stirlinglem3  46091  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  dirker2re  46107  dirkerval2  46109  dirkerre  46110  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkeritg  46117  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem4  46126  fourierdlem5  46127  fourierdlem6  46128  fourierdlem7  46129  fourierdlem9  46131  fourierdlem10  46132  fourierdlem18  46140  fourierdlem19  46141  fourierdlem20  46142  fourierdlem26  46148  fourierdlem28  46150  fourierdlem30  46152  fourierdlem35  46157  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem47  46168  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem53  46174  fourierdlem57  46178  fourierdlem59  46180  fourierdlem60  46181  fourierdlem61  46182  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem66  46187  fourierdlem68  46189  fourierdlem71  46192  fourierdlem72  46193  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem80  46201  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem84  46205  fourierdlem87  46208  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem94  46215  fourierdlem95  46216  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  qndenserrnbllem  46309  ioorrnopnlem  46319  ioorrnopnxrlem  46321  sge0xaddlem1  46448  sge0xaddlem2  46449  omeiunltfirp  46534  carageniuncllem2  46537  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoiqssbllem1  46637  hoiqssbllem2  46638  hoiqssbllem3  46639  hspmbllem2  46642  hspmbllem3  46643  ovolval5lem1  46667  iinhoiicclem  46688  iinhoiicc  46689  iunhoiioolem  46690  iccvonmbllem  46693  vonioolem1  46695  vonioolem2  46696  vonicclem1  46698  vonicclem2  46699  preimaleiinlt  46736  salpreimaltle  46741  smfaddlem1  46778  smfadd  46780  smflimlem3  46788  smflimlem4  46789  smflimlem6  46791  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  ormkglobd  46890  zm1nn  47314  requad01  47608  requad1  47609  requad2  47610  perfectALTVlem2  47709  nnsum4primesevenALTV  47788  bgoldbtbndlem2  47793  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  dignn0flhalflem1  48536  affinecomb1  48623  resum2sqcl  48627  2sphere  48670  line2  48673  itsclc0lem1  48677  itscnhlc0yqe  48680  itsclquadb  48697  2itscp  48702  itscnhlinecirc02plem1  48703  itscnhlinecirc02plem3  48705  itscnhlinecirc02p  48706  inlinecirc02plem  48707  amgmwlem  49321