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

Theorem readdcld 10232
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 10182 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  (class class class)co 6801  cr 10098   + caddc 10102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10160
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  ltadd2  10304  readdcan  10373  addid1  10379  leadd1  10659  le2add  10673  lesub2  10686  lesub3d  10808  supaddc  11153  supadd  11154  cju  11179  div4p1lem1div2  11450  difgtsumgt  11509  eluzmn  11857  rpnnen1lem5  11982  rpnnen1lem5OLD  11988  addlelt  12106  xralrple  12200  xov1plusxeqvd  12482  zltaddlt1le  12488  elincfzoext  12691  fladdz  12791  2tnp1ge0ge0  12795  flhalf  12796  fldiv  12824  modaddmodup  12898  modaddmodlo  12899  addmodlteq  12910  discr1  13165  discr  13166  ccatalpha  13536  2cshw  13730  remim  14027  remullem  14038  sqrlem7  14159  absrele  14218  abstri  14240  abs3lem  14248  amgm2  14279  mulcn2  14496  o1add  14514  o1sub  14516  lo1add  14527  caucvgrlem  14573  iseraltlem2  14583  iseraltlem3  14584  fsumabs  14703  o1fsum  14715  climcndslem2  14752  tanhlt1  15060  eirrlem  15102  ruclem1  15130  ruclem2  15131  ruclem3  15132  ltoddhalfle  15258  bitscmp  15333  sadcaddlem  15352  sadasslem  15365  smuval2  15377  prmreclem4  15796  4sqlem5  15819  4sqlem6  15820  4sqlem12  15833  4sqlem15  15836  4sqlem16  15837  prmgaplem7  15934  prmgaplem8  15935  2expltfac  15972  cshwshashlem2  15976  chfacfscmul0  20836  chfacfscmulgsum  20838  chfacfpmmul0  20840  chfacfpmmulgsum  20842  prdsxmetlem  22345  xblss2ps  22378  metustexhalf  22533  nrmmetd  22551  ngptgp  22612  nlmvscnlem2  22661  nlmvscnlem1  22662  nmotri  22715  nghmplusg  22716  blcvx  22773  iccntr  22796  icccmplem2  22798  reconnlem2  22802  metdcnlem  22811  metnrmlem3  22836  cnllycmp  22927  lebnumii  22937  tchcphlem1  23205  ipcnlem2  23214  ipcnlem1  23215  csbren  23353  trirn  23354  minveclem2  23368  minveclem3b  23370  minveclem4  23374  ivthlem2  23392  ovolgelb  23419  ovollb2lem  23427  ovolunlem1a  23435  ovolunlem1  23436  ovolfiniun  23440  ovoliunlem1  23441  ovoliunlem2  23442  ovolshftlem1  23448  ovolscalem1  23452  ovolicopnf  23463  ismbl2  23466  nulmbl2  23475  unmbl  23476  voliunlem2  23490  ioombl1lem2  23498  ioombl1lem4  23500  ioombl1  23501  ioorcl2  23511  uniioombllem1  23520  uniioombllem3  23524  uniioombllem4  23525  uniioombllem5  23526  uniioombl  23528  opnmbllem  23540  volcn  23545  itg1addlem4  23636  mbfi1fseqlem4  23655  mbfi1fseqlem6  23657  itg2splitlem  23685  itg2split  23686  itg2monolem3  23689  itg2addlem  23695  ibladdlem  23756  itgaddlem1  23759  itgaddlem2  23760  iblabslem  23764  iblabs  23765  dvferm1lem  23917  dvferm2lem  23919  dvlip2  23928  lhop1lem  23946  lhop1  23947  lhop  23949  dvcnvrelem1  23950  dvcnvrelem2  23951  dvcnvre  23952  dvcvx  23953  dvfsumlem3  23961  dvfsumlem4  23962  dvfsum2  23967  ftc1lem4  23972  coemullem  24176  ulmbdd  24322  ulmcn  24323  ulmdvlem1  24324  radcnvle  24344  pserdvlem1  24351  pserdv  24353  abelthlem7  24362  pilem2  24376  pilem3  24377  cosordlem  24447  abslogle  24534  logccv  24579  cxpaddle  24663  ang180lem2  24710  heron  24735  atanlogaddlem  24810  atans2  24828  cxp2limlem  24872  scvxcvx  24882  jensenlem2  24884  amgmlem  24886  logdiflbnd  24891  harmonicbnd4  24907  fsumharmonic  24908  lgamgulmlem3  24927  lgamgulmlem4  24928  lgamgulmlem5  24929  lgamgulmlem6  24930  lgambdd  24933  lgamucov  24934  regamcl  24957  ftalem5  24973  efnnfsumcl  24999  efchtdvds  25055  chtublem  25106  chtub  25107  logfaclbnd  25117  perfectlem2  25125  bcmono  25172  bposlem7  25185  bposlem9  25187  lgsdirprm  25226  gausslemma2dlem1a  25260  2sqlem8  25321  chpchtlim  25338  vmadivsumb  25342  rplogsumlem1  25343  dchrisumlem2  25349  dchrvmasumlem2  25357  dchrvmasumiflem1  25360  dchrisum0re  25372  dchrisum0lem1b  25374  mulog2sumlem1  25393  mulog2sumlem2  25394  logsqvma2  25402  log2sumbnd  25403  selberglem2  25405  selbergb  25408  selberg2b  25411  chpdifbndlem1  25412  chpdifbndlem2  25413  selberg3lem2  25417  selberg3  25418  selberg4lem1  25419  selberg4  25420  pntrsumbnd2  25426  selberg3r  25428  selberg34r  25430  pntsf  25432  pntrlog2bndlem1  25436  pntrlog2bndlem2  25437  pntrlog2bndlem4  25439  pntrlog2bndlem5  25440  pntrlog2bndlem6  25442  pntrlog2bnd  25443  pntpbnd1a  25444  pntpbnd2  25446  pntibndlem2a  25449  pntibndlem2  25450  pntibndlem3  25451  pntlemg  25457  pntlemr  25461  pntlemk  25465  pntlemo  25466  pntlem3  25468  abvcxp  25474  padicabv  25489  ostth2lem2  25493  ostth3  25497  brbtwn2  25955  axsegconlem8  25974  axsegconlem10  25976  axpaschlem  25990  axpasch  25991  axeuclidlem  26012  axcontlem2  26015  crctcshwlkn0lem3  26886  crctcshwlkn0lem5  26888  vacn  27829  smcnlem  27832  ubthlem2  28007  minvecolem2  28011  minvecolem3  28012  minvecolem4  28016  minvecolem5  28017  nmoptrii  29233  hstle  29369  staddi  29385  stadd3i  29387  lt2addrd  29796  nndiffz1  29828  bhmafibid1  29924  fsumrp0cl  29975  pmtrto1cl  30129  fzto1st  30133  psgnfzto1st  30135  1smat1  30150  sqsscirc1  30234  cnre2csqlem  30236  tpr2rico  30238  nexple  30351  dya2iocress  30616  dya2iocbrsiga  30617  dya2icobrsiga  30618  dya2icoseg  30619  dya2iocucvr  30626  sxbrsigalem2  30628  omssubaddlem  30641  fibp1  30743  ballotlemfc0  30834  ballotlemfcc  30835  ballotlemsgt1  30852  ballotlemsel1i  30854  plymulx0  30904  breprexplemc  30990  breprexp  30991  logdivsqrle  31008  resconn  31506  faclim  31910  dnizphlfeqhlf  32743  dnibndlem4  32748  dnibndlem6  32750  dnibndlem8  32752  dnibndlem9  32753  dnibndlem10  32754  dnibndlem11  32755  dnibndlem13  32757  dnibnd  32758  knoppcnlem4  32763  unblimceq0lem  32774  unblimceq0  32775  unbdqndv2lem1  32777  poimirlem29  33720  heicant  33726  opnmbllem0  33727  mblfinlem3  33730  mblfinlem4  33731  ismblfin  33732  mbfposadd  33739  itg2addnclem  33743  itg2addnclem3  33745  itg2addnc  33746  itg2gt0cn  33747  ibladdnclem  33748  itgaddnclem1  33750  itgaddnclem2  33751  iblabsnclem  33755  iblabsnc  33756  iblmulc2nc  33757  ftc1cnnclem  33765  ftc1anclem4  33770  ftc1anclem7  33773  ftc1anclem8  33774  ftc1anc  33775  areacirclem5  33786  mettrifi  33835  isbnd3  33865  ssbnd  33869  cntotbnd  33877  heibor1lem  33890  bfplem2  33904  rrnequiv  33916  iccbnd  33921  pellexlem2  37865  pell1qrge1  37905  pell14qrgapw  37911  pellqrexplicit  37912  pellqrex  37914  pellfundge  37917  pellfundgt1  37918  rmspecfund  37945  rmxycomplete  37953  ltrmynn0  37986  jm2.24nn  37997  jm2.24  38001  fzmaxdif  38019  jm2.26lem3  38039  jm3.1lem2  38056  areaquad  38273  imo72b2lem0  38936  hashnzfzclim  38992  binomcxplemnotnn0  39026  zltlesub  39965  lt3addmuld  39983  absnpncan2d  39984  fperiodmullem  39985  lt4addmuld  39988  absnpncan3d  39989  leadd12dd  39999  supxrgelem  40020  supxrge  40021  ltadd12dd  40026  xralrple2  40037  infxr  40050  infleinflem2  40054  xralrple4  40056  xralrple3  40057  xrralrecnnle  40069  eliooshift  40201  iccshift  40216  iooshift  40220  iooiinicc  40241  iooiinioc  40255  fsumnncl  40275  climinf  40310  climsuselem1  40311  sumnnodd  40334  lptre2pt  40344  addlimc  40352  0ellimcdiv  40353  limclner  40355  climleltrp  40380  liminfltlem  40508  fperdvper  40605  dvdivbd  40610  dvbdfbdioolem2  40616  dvbdfbdioo  40617  ioodvbdlimc1lem1  40618  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvxpaek  40627  dvnmul  40630  iblsplit  40654  iblspltprt  40661  itgspltprt  40667  itgiccshift  40668  itgperiod  40669  itgsbtaddcnst  40670  stoweidlem1  40690  stoweidlem11  40700  stoweidlem13  40702  stoweidlem14  40703  stoweidlem20  40709  stoweidlem21  40710  stoweidlem26  40715  stoweidlem44  40733  stoweidlem60  40749  wallispilem3  40756  wallispilem4  40757  wallispilem5  40758  wallispi  40759  wallispi2lem1  40760  wallispi2lem2  40761  stirlinglem1  40763  stirlinglem3  40765  stirlinglem5  40767  stirlinglem6  40768  stirlinglem7  40769  stirlinglem10  40772  stirlinglem11  40773  stirlinglem12  40774  dirker2re  40781  dirkerval2  40783  dirkerre  40784  dirkerper  40785  dirkertrigeqlem1  40787  dirkertrigeqlem2  40788  dirkeritg  40791  dirkercncflem1  40792  dirkercncflem2  40793  dirkercncflem4  40795  fourierdlem4  40800  fourierdlem5  40801  fourierdlem6  40802  fourierdlem7  40803  fourierdlem9  40805  fourierdlem10  40806  fourierdlem18  40814  fourierdlem19  40815  fourierdlem20  40816  fourierdlem26  40822  fourierdlem28  40824  fourierdlem30  40826  fourierdlem35  40831  fourierdlem40  40836  fourierdlem41  40837  fourierdlem42  40838  fourierdlem47  40842  fourierdlem48  40843  fourierdlem49  40844  fourierdlem50  40845  fourierdlem51  40846  fourierdlem53  40848  fourierdlem57  40852  fourierdlem59  40854  fourierdlem60  40855  fourierdlem61  40856  fourierdlem63  40858  fourierdlem64  40859  fourierdlem65  40860  fourierdlem66  40861  fourierdlem68  40863  fourierdlem71  40866  fourierdlem72  40867  fourierdlem74  40869  fourierdlem75  40870  fourierdlem76  40871  fourierdlem78  40873  fourierdlem79  40874  fourierdlem80  40875  fourierdlem81  40876  fourierdlem82  40877  fourierdlem83  40878  fourierdlem84  40879  fourierdlem87  40882  fourierdlem88  40883  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem92  40887  fourierdlem93  40888  fourierdlem94  40889  fourierdlem95  40890  fourierdlem97  40892  fourierdlem101  40896  fourierdlem103  40898  fourierdlem104  40899  fourierdlem111  40906  fourierdlem112  40907  fourierdlem113  40908  sqwvfoura  40917  sqwvfourb  40918  fouriersw  40920  qndenserrnbllem  40986  ioorrnopnlem  40996  ioorrnopnxrlem  40998  sge0xaddlem1  41122  sge0xaddlem2  41123  omeiunltfirp  41208  carageniuncllem2  41211  hoidmv1lelem1  41280  hoidmv1lelem2  41281  hoidmvlelem1  41284  hoidmvlelem2  41285  hoidmvlelem3  41286  hoidmvlelem4  41287  hoiqssbllem1  41311  hoiqssbllem2  41312  hoiqssbllem3  41313  hspmbllem2  41316  hspmbllem3  41317  ovolval5lem1  41341  iinhoiicclem  41362  iinhoiicc  41363  iunhoiioolem  41364  iccvonmbllem  41367  vonioolem1  41369  vonioolem2  41370  vonicclem1  41372  vonicclem2  41373  preimaleiinlt  41406  salpreimaltle  41410  smfaddlem1  41446  smfadd  41448  smflimlem3  41456  smflimlem4  41457  smflimlem6  41459  smfmullem1  41473  smfmullem2  41474  smfmullem3  41475  zm1nn  41795  perfectALTVlem2  42110  nnsum4primesevenALTV  42168  bgoldbtbndlem2  42173  dignn0flhalflem1  42888  amgmwlem  43030
  Copyright terms: Public domain W3C validator