MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  readdcld Structured version   Visualization version   GIF version

Theorem readdcld 9948
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
StepHypRef Expression
1 recnd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 readdcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 readdcl 9898 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 691 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  (class class class)co 6549  cr 9814   + caddc 9818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9876
This theorem depends on definitions:  df-bi 196  df-an 385
This theorem is referenced by:  ltadd2  10020  readdcan  10089  addid1  10095  leadd1  10375  le2add  10389  lesub2  10402  lesub3d  10524  supaddc  10867  supadd  10868  cju  10893  div4p1lem1div2  11164  difgtsumgt  11223  eluzmn  11570  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  addlelt  11818  xralrple  11910  xov1plusxeqvd  12189  zltaddlt1le  12195  elincfzoext  12393  fladdz  12488  2tnp1ge0ge0  12492  flhalf  12493  fldiv  12521  modaddmodup  12595  modaddmodlo  12596  addmodlteq  12607  discr1  12862  discr  12863  ccatalpha  13228  2cshw  13410  remim  13705  remullem  13716  sqrlem7  13837  absrele  13896  abstri  13918  abs3lem  13926  amgm2  13957  mulcn2  14174  o1add  14192  o1sub  14194  lo1add  14205  caucvgrlem  14251  iseraltlem2  14261  iseraltlem3  14262  fsumabs  14374  o1fsum  14386  climcndslem2  14421  tanhlt1  14729  eirrlem  14771  ruclem1  14799  ruclem2  14800  ruclem3  14801  ltoddhalfle  14923  bitscmp  14998  sadcaddlem  15017  sadasslem  15030  smuval2  15042  prmreclem4  15461  4sqlem5  15484  4sqlem6  15485  4sqlem12  15498  4sqlem15  15501  4sqlem16  15502  prmgaplem7  15599  prmgaplem8  15600  2expltfac  15637  cshwshashlem2  15641  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  prdsxmetlem  21983  xblss2ps  22016  metustexhalf  22171  nrmmetd  22189  ngptgp  22250  nlmvscnlem2  22299  nlmvscnlem1  22300  nmotri  22353  nghmplusg  22354  blcvx  22409  iccntr  22432  icccmplem2  22434  reconnlem2  22438  metdcnlem  22447  metnrmlem3  22472  cnllycmp  22563  lebnumii  22573  tchcphlem1  22842  ipcnlem2  22851  ipcnlem1  22852  csbren  22990  trirn  22991  minveclem2  23005  minveclem3b  23007  minveclem4  23011  ivthlem2  23028  ovolgelb  23055  ovollb2lem  23063  ovolunlem1a  23071  ovolunlem1  23072  ovolfiniun  23076  ovoliunlem1  23077  ovoliunlem2  23078  ovolshftlem1  23084  ovolscalem1  23088  ovolicopnf  23099  ismbl2  23102  nulmbl2  23111  unmbl  23112  voliunlem2  23126  ioombl1lem2  23134  ioombl1lem4  23136  ioombl1  23137  ioorcl2  23146  uniioombllem1  23155  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  opnmbllem  23175  volcn  23180  itg1addlem4  23272  mbfi1fseqlem4  23291  mbfi1fseqlem6  23293  itg2splitlem  23321  itg2split  23322  itg2monolem3  23325  itg2addlem  23331  ibladdlem  23392  itgaddlem1  23395  itgaddlem2  23396  iblabslem  23400  iblabs  23401  dvferm1lem  23551  dvferm2lem  23553  dvlip2  23562  lhop1lem  23580  lhop1  23581  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvcvx  23587  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  ftc1lem4  23606  coemullem  23810  ulmbdd  23956  ulmcn  23957  ulmdvlem1  23958  radcnvle  23978  pserdvlem1  23985  pserdv  23987  abelthlem7  23996  pilem2  24010  pilem3  24011  cosordlem  24081  abslogle  24168  logccv  24209  cxpaddle  24293  ang180lem2  24340  heron  24365  atanlogaddlem  24440  atans2  24458  cxp2limlem  24502  scvxcvx  24512  jensenlem2  24514  amgmlem  24516  logdiflbnd  24521  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgambdd  24563  lgamucov  24564  regamcl  24587  ftalem5  24603  efnnfsumcl  24629  efchtdvds  24685  chtublem  24736  chtub  24737  logfaclbnd  24747  perfectlem2  24755  bcmono  24802  bposlem7  24815  bposlem9  24817  lgsdirprm  24856  gausslemma2dlem1a  24890  2sqlem8  24951  chpchtlim  24968  vmadivsumb  24972  rplogsumlem1  24973  dchrisumlem2  24979  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0re  25002  dchrisum0lem1b  25004  mulog2sumlem1  25023  mulog2sumlem2  25024  logsqvma2  25032  log2sumbnd  25033  selberglem2  25035  selbergb  25038  selberg2b  25041  chpdifbndlem1  25042  chpdifbndlem2  25043  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrsumbnd2  25056  selberg3r  25058  selberg34r  25060  pntsf  25062  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem2a  25079  pntibndlem2  25080  pntibndlem3  25081  pntlemg  25087  pntlemr  25091  pntlemk  25095  pntlemo  25096  pntlem3  25098  abvcxp  25104  padicabv  25119  ostth2lem2  25123  ostth3  25127  brbtwn2  25585  axsegconlem8  25604  axsegconlem10  25606  axpaschlem  25620  axpasch  25621  axeuclidlem  25642  axcontlem2  25645  vacn  26933  smcnlem  26936  ubthlem2  27111  minvecolem2  27115  minvecolem3  27116  minvecolem4  27120  minvecolem5  27121  nmoptrii  28337  hstle  28473  staddi  28489  stadd3i  28491  lt2addrd  28903  nndiffz1  28936  bhmafibid1  28975  fsumrp0cl  29026  pmtrto1cl  29180  fzto1st  29184  psgnfzto1st  29186  1smat1  29198  sqsscirc1  29282  cnre2csqlem  29284  tpr2rico  29286  nexple  29399  dya2iocress  29663  dya2iocbrsiga  29664  dya2icobrsiga  29665  dya2icoseg  29666  dya2iocucvr  29673  sxbrsigalem2  29675  omssubaddlem  29688  fibp1  29790  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsgt1  29899  ballotlemsel1i  29901  plymulx0  29950  rescon  30482  faclim  30885  dnizphlfeqhlf  31636  dnibndlem4  31641  dnibndlem6  31643  dnibndlem8  31645  dnibndlem9  31646  dnibndlem10  31647  dnibndlem11  31648  dnibndlem13  31650  dnibnd  31651  knoppcnlem4  31656  unblimceq0lem  31667  unblimceq0  31668  unbdqndv2lem1  31670  poimirlem29  32608  heicant  32614  opnmbllem0  32615  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  mbfposadd  32627  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem1  32638  itgaddnclem2  32639  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  ftc1cnnclem  32653  ftc1anclem4  32658  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem5  32674  mettrifi  32723  isbnd3  32753  ssbnd  32757  cntotbnd  32765  heibor1lem  32778  bfplem2  32792  rrnequiv  32804  iccbnd  32809  pellexlem2  36412  pell1qrge1  36452  pell14qrgapw  36458  pellqrexplicit  36459  pellqrex  36461  pellfundge  36464  pellfundgt1  36465  rmspecfund  36492  rmxycomplete  36500  ltrmynn0  36533  jm2.24nn  36544  jm2.24  36548  fzmaxdif  36566  jm2.26lem3  36586  jm3.1lem2  36603  areaquad  36821  imo72b2lem0  37487  hashnzfzclim  37543  binomcxplemnotnn0  37577  zltlesub  38438  lt3addmuld  38456  absnpncan2d  38457  fperiodmullem  38458  lt4addmuld  38461  absnpncan3d  38462  leadd12dd  38473  supxrgelem  38494  supxrge  38495  ltadd12dd  38500  xralrple2  38511  infxr  38524  infleinflem2  38528  xralrple4  38530  xralrple3  38531  xrralrecnnle  38543  eliooshift  38576  iccshift  38591  iooshift  38595  iooiinicc  38616  iooiinioc  38630  fsumnncl  38638  climinf  38673  climsuselem1  38674  sumnnodd  38697  lptre2pt  38707  addlimc  38715  0ellimcdiv  38716  limclner  38718  climleltrp  38743  fperdvper  38808  dvdivbd  38813  dvbdfbdioolem2  38819  dvbdfbdioo  38820  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvxpaek  38830  dvnmul  38833  iblsplit  38858  iblspltprt  38865  itgspltprt  38871  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  stoweidlem14  38907  stoweidlem20  38913  stoweidlem21  38914  stoweidlem26  38919  stoweidlem44  38937  stoweidlem60  38953  wallispilem3  38960  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem1  38967  stirlinglem3  38969  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  dirker2re  38985  dirkerval2  38987  dirkerre  38988  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkeritg  38995  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem5  39005  fourierdlem6  39006  fourierdlem7  39007  fourierdlem9  39009  fourierdlem10  39010  fourierdlem18  39018  fourierdlem19  39019  fourierdlem20  39020  fourierdlem26  39026  fourierdlem28  39028  fourierdlem30  39030  fourierdlem35  39035  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem53  39052  fourierdlem57  39056  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem66  39065  fourierdlem68  39067  fourierdlem71  39070  fourierdlem72  39071  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem87  39086  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem94  39093  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  qndenserrnbllem  39190  ioorrnopnlem  39200  ioorrnopnxrlem  39202  sge0xaddlem1  39326  sge0xaddlem2  39327  omeiunltfirp  39409  carageniuncllem2  39412  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoiqssbllem1  39512  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem2  39517  hspmbllem3  39518  ovolval5lem1  39542  iinhoiicclem  39564  iinhoiicc  39565  iunhoiioolem  39566  iccvonmbllem  39569  vonioolem1  39571  vonioolem2  39572  vonicclem1  39574  vonicclem2  39575  preimaleiinlt  39608  salpreimaltle  39612  issmfltle  39622  smfaddlem1  39649  smfadd  39651  smflimlem3  39659  smflimlem4  39660  smflimlem6  39662  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  perfectALTVlem2  40165  nnsum4primesevenALTV  40217  bgoldbtbndlem2  40222  zm1nn  40348  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  dignn0flhalflem1  42207  amgmwlem  42357
  Copyright terms: Public domain W3C validator