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

Theorem readdcld 10354
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 10304 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 575 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  (class class class)co 6874  cr 10220   + caddc 10224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10282
This theorem depends on definitions:  df-bi 198  df-an 385
This theorem is referenced by:  ltadd2  10426  readdcan  10495  addid1  10501  leadd1  10781  le2add  10795  lesub2  10808  lesub3d  10930  supaddc  11275  supadd  11276  cju  11301  div4p1lem1div2  11554  difgtsumgt  11612  eluzmn  11911  rpnnen1lem5  12037  addlelt  12158  xralrple  12254  xov1plusxeqvd  12541  zltaddlt1le  12547  elincfzoext  12750  fladdz  12850  2tnp1ge0ge0  12854  flhalf  12855  fldiv  12883  modaddmodup  12957  modaddmodlo  12958  addmodlteq  12969  discr1  13223  discr  13224  ccatalpha  13590  2cshw  13783  remim  14080  remullem  14091  sqrlem7  14212  absrele  14271  abstri  14293  abs3lem  14301  amgm2  14332  mulcn2  14549  o1add  14567  o1sub  14569  lo1add  14580  caucvgrlem  14626  iseraltlem2  14636  iseraltlem3  14637  fsumabs  14755  o1fsum  14767  climcndslem2  14804  tanhlt1  15110  eirrlem  15152  ruclem1  15180  ruclem2  15181  ruclem3  15182  ltoddhalfle  15305  bitscmp  15379  sadcaddlem  15398  sadasslem  15411  smuval2  15423  iserodd  15757  prmreclem4  15840  4sqlem5  15863  4sqlem6  15864  4sqlem12  15877  4sqlem15  15880  4sqlem16  15881  prmgaplem7  15978  prmgaplem8  15979  2expltfac  16011  cshwshashlem2  16015  chfacfscmul0  20876  chfacfscmulgsum  20878  chfacfpmmul0  20880  chfacfpmmulgsum  20882  prdsxmetlem  22386  xblss2ps  22419  metustexhalf  22574  nrmmetd  22592  ngptgp  22653  nlmvscnlem2  22702  nlmvscnlem1  22703  nmotri  22756  nghmplusg  22757  blcvx  22814  iccntr  22837  icccmplem2  22839  reconnlem2  22843  metdcnlem  22852  metnrmlem3  22877  cnllycmp  22968  lebnumii  22978  tchcphlem1  23246  ipcnlem2  23255  ipcnlem1  23256  csbren  23394  trirn  23395  minveclem2  23409  minveclem3b  23411  minveclem4  23415  ivthlem2  23433  ovolgelb  23461  ovollb2lem  23469  ovolunlem1a  23477  ovolunlem1  23478  ovolfiniun  23482  ovoliunlem1  23483  ovoliunlem2  23484  ovolshftlem1  23490  ovolscalem1  23494  ovolicopnf  23505  ismbl2  23508  nulmbl2  23517  unmbl  23518  voliunlem2  23532  ioombl1lem2  23540  ioombl1lem4  23542  ioombl1  23543  ioorcl2  23553  uniioombllem1  23562  uniioombllem3  23566  uniioombllem4  23567  uniioombllem5  23568  uniioombl  23570  opnmbllem  23582  volcn  23587  itg1addlem4  23680  mbfi1fseqlem4  23699  mbfi1fseqlem6  23701  itg2splitlem  23729  itg2split  23730  itg2monolem3  23733  itg2addlem  23739  ibladdlem  23800  itgaddlem1  23803  itgaddlem2  23804  iblabslem  23808  iblabs  23809  dvferm1lem  23961  dvferm2lem  23963  dvlip2  23972  lhop1lem  23990  lhop1  23991  lhop  23993  dvcnvrelem1  23994  dvcnvrelem2  23995  dvcnvre  23996  dvcvx  23997  dvfsumlem3  24005  dvfsumlem4  24006  dvfsum2  24011  ftc1lem4  24016  coemullem  24220  ulmbdd  24366  ulmcn  24367  ulmdvlem1  24368  radcnvle  24388  pserdvlem1  24395  pserdv  24397  abelthlem7  24406  pilem2  24420  pilem3  24421  pilem3OLD  24422  cosordlem  24492  abslogle  24578  logccv  24623  cxpaddle  24707  ang180lem2  24754  heron  24779  atanlogaddlem  24854  atans2  24872  cxp2limlem  24916  scvxcvx  24926  jensenlem2  24928  amgmlem  24930  logdiflbnd  24935  harmonicbnd4  24951  fsumharmonic  24952  lgamgulmlem3  24971  lgamgulmlem4  24972  lgamgulmlem5  24973  lgamgulmlem6  24974  lgambdd  24977  lgamucov  24978  regamcl  25001  ftalem5  25017  efnnfsumcl  25043  efchtdvds  25099  chtublem  25150  chtub  25151  logfaclbnd  25161  perfectlem2  25169  bcmono  25216  bposlem7  25229  bposlem9  25231  lgsdirprm  25270  gausslemma2dlem1a  25304  2sqlem8  25365  chpchtlim  25382  vmadivsumb  25386  rplogsumlem1  25387  dchrisumlem2  25393  dchrvmasumlem2  25401  dchrvmasumiflem1  25404  dchrisum0re  25416  dchrisum0lem1b  25418  mulog2sumlem1  25437  mulog2sumlem2  25438  logsqvma2  25446  log2sumbnd  25447  selberglem2  25449  selbergb  25452  selberg2b  25455  chpdifbndlem1  25456  chpdifbndlem2  25457  selberg3lem2  25461  selberg3  25462  selberg4lem1  25463  selberg4  25464  pntrsumbnd2  25470  selberg3r  25472  selberg34r  25474  pntsf  25476  pntrlog2bndlem1  25480  pntrlog2bndlem2  25481  pntrlog2bndlem4  25483  pntrlog2bndlem5  25484  pntrlog2bndlem6  25486  pntrlog2bnd  25487  pntpbnd1a  25488  pntpbnd2  25490  pntibndlem2a  25493  pntibndlem2  25494  pntibndlem3  25495  pntlemg  25501  pntlemr  25505  pntlemk  25509  pntlemo  25510  pntlem3  25512  abvcxp  25518  padicabv  25533  ostth2lem2  25537  ostth3  25541  brbtwn2  25999  axsegconlem8  26018  axsegconlem10  26020  axpaschlem  26034  axpasch  26035  axeuclidlem  26056  axcontlem2  26059  crctcshwlkn0lem3  26933  crctcshwlkn0lem5  26935  vacn  27877  smcnlem  27880  ubthlem2  28055  minvecolem2  28059  minvecolem3  28060  minvecolem4  28064  minvecolem5  28065  nmoptrii  29281  hstle  29417  staddi  29433  stadd3i  29435  lt2addrd  29843  nndiffz1  29875  bhmafibid1  29969  fsumrp0cl  30020  pmtrto1cl  30174  fzto1st  30178  psgnfzto1st  30180  1smat1  30195  sqsscirc1  30279  cnre2csqlem  30281  tpr2rico  30283  nexple  30396  dya2iocress  30661  dya2iocbrsiga  30662  dya2icobrsiga  30663  dya2icoseg  30664  dya2iocucvr  30671  sxbrsigalem2  30673  omssubaddlem  30686  fibp1  30788  ballotlemfc0  30879  ballotlemfcc  30880  ballotlemsgt1  30897  ballotlemsel1i  30899  plymulx0  30949  breprexplemc  31035  breprexp  31036  logdivsqrle  31053  resconn  31551  faclim  31954  dnizphlfeqhlf  32783  dnibndlem4  32788  dnibndlem6  32790  dnibndlem8  32792  dnibndlem9  32793  dnibndlem10  32794  dnibndlem11  32795  dnibndlem13  32797  dnibnd  32798  knoppcnlem4  32803  unblimceq0lem  32814  unblimceq0  32815  unbdqndv2lem1  32817  poimirlem29  33751  heicant  33757  opnmbllem0  33758  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  mbfposadd  33769  itg2addnclem  33773  itg2addnclem3  33775  itg2addnc  33776  itg2gt0cn  33777  ibladdnclem  33778  itgaddnclem1  33780  itgaddnclem2  33781  iblabsnclem  33785  iblabsnc  33786  iblmulc2nc  33787  ftc1cnnclem  33795  ftc1anclem4  33800  ftc1anclem7  33803  ftc1anclem8  33804  ftc1anc  33805  areacirclem5  33816  mettrifi  33864  isbnd3  33894  ssbnd  33898  cntotbnd  33906  heibor1lem  33919  bfplem2  33933  rrnequiv  33945  iccbnd  33950  pellexlem2  37896  pell1qrge1  37936  pell14qrgapw  37942  pellqrexplicit  37943  pellqrex  37945  pellfundge  37948  pellfundgt1  37949  rmspecfund  37975  rmxycomplete  37983  ltrmynn0  38016  jm2.24nn  38027  jm2.24  38031  fzmaxdif  38049  jm2.26lem3  38069  jm3.1lem2  38086  areaquad  38302  imo72b2lem0  38965  hashnzfzclim  39021  binomcxplemnotnn0  39055  zltlesub  39979  lt3addmuld  39996  absnpncan2d  39997  fperiodmullem  39998  lt4addmuld  40001  absnpncan3d  40002  leadd12dd  40012  supxrgelem  40033  supxrge  40034  ltadd12dd  40039  xralrple2  40050  infxr  40063  infleinflem2  40067  xralrple4  40069  xralrple3  40070  xrralrecnnle  40082  eliooshift  40213  iccshift  40225  iooshift  40229  iooiinicc  40249  iooiinioc  40263  fsumnncl  40283  climinf  40318  climsuselem1  40319  sumnnodd  40342  lptre2pt  40352  addlimc  40360  0ellimcdiv  40361  limclner  40363  climleltrp  40388  liminfltlem  40516  fperdvper  40613  dvdivbd  40618  dvbdfbdioolem2  40624  dvbdfbdioo  40625  ioodvbdlimc1lem1  40626  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvxpaek  40635  dvnmul  40638  iblsplit  40661  iblspltprt  40668  itgspltprt  40674  itgiccshift  40675  itgperiod  40676  itgsbtaddcnst  40677  stoweidlem1  40697  stoweidlem11  40707  stoweidlem13  40709  stoweidlem14  40710  stoweidlem20  40716  stoweidlem21  40717  stoweidlem26  40722  stoweidlem44  40740  stoweidlem60  40756  wallispilem3  40763  wallispilem4  40764  wallispilem5  40765  wallispi  40766  wallispi2lem1  40767  wallispi2lem2  40768  stirlinglem1  40770  stirlinglem3  40772  stirlinglem5  40774  stirlinglem6  40775  stirlinglem7  40776  stirlinglem10  40779  stirlinglem11  40780  stirlinglem12  40781  dirker2re  40788  dirkerval2  40790  dirkerre  40791  dirkerper  40792  dirkertrigeqlem1  40794  dirkertrigeqlem2  40795  dirkeritg  40798  dirkercncflem1  40799  dirkercncflem2  40800  dirkercncflem4  40802  fourierdlem4  40807  fourierdlem5  40808  fourierdlem6  40809  fourierdlem7  40810  fourierdlem9  40812  fourierdlem10  40813  fourierdlem18  40821  fourierdlem19  40822  fourierdlem20  40823  fourierdlem26  40829  fourierdlem28  40831  fourierdlem30  40833  fourierdlem35  40838  fourierdlem40  40843  fourierdlem41  40844  fourierdlem42  40845  fourierdlem47  40849  fourierdlem48  40850  fourierdlem49  40851  fourierdlem50  40852  fourierdlem51  40853  fourierdlem53  40855  fourierdlem57  40859  fourierdlem59  40861  fourierdlem60  40862  fourierdlem61  40863  fourierdlem63  40865  fourierdlem64  40866  fourierdlem65  40867  fourierdlem66  40868  fourierdlem68  40870  fourierdlem71  40873  fourierdlem72  40874  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem78  40880  fourierdlem79  40881  fourierdlem80  40882  fourierdlem81  40883  fourierdlem82  40884  fourierdlem83  40885  fourierdlem84  40886  fourierdlem87  40889  fourierdlem88  40890  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem92  40894  fourierdlem93  40895  fourierdlem94  40896  fourierdlem95  40897  fourierdlem97  40899  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fourierdlem112  40914  fourierdlem113  40915  sqwvfoura  40924  sqwvfourb  40925  fouriersw  40927  qndenserrnbllem  40993  ioorrnopnlem  41003  ioorrnopnxrlem  41005  sge0xaddlem1  41129  sge0xaddlem2  41130  omeiunltfirp  41215  carageniuncllem2  41218  hoidmv1lelem1  41287  hoidmv1lelem2  41288  hoidmvlelem1  41291  hoidmvlelem2  41292  hoidmvlelem3  41293  hoidmvlelem4  41294  hoiqssbllem1  41318  hoiqssbllem2  41319  hoiqssbllem3  41320  hspmbllem2  41323  hspmbllem3  41324  ovolval5lem1  41348  iinhoiicclem  41369  iinhoiicc  41370  iunhoiioolem  41371  iccvonmbllem  41374  vonioolem1  41376  vonioolem2  41377  vonicclem1  41379  vonicclem2  41380  preimaleiinlt  41413  salpreimaltle  41417  smfaddlem1  41453  smfadd  41455  smflimlem3  41463  smflimlem4  41464  smflimlem6  41466  smfmullem1  41480  smfmullem2  41481  smfmullem3  41482  zm1nn  41892  perfectALTVlem2  42206  nnsum4primesevenALTV  42264  bgoldbtbndlem2  42269  dignn0flhalflem1  42977  amgmwlem  43119
  Copyright terms: Public domain W3C validator