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

Theorem readdcld 10107
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 10057 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  (class class class)co 6690  cr 9973   + caddc 9977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 10035
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  ltadd2  10179  readdcan  10248  addid1  10254  leadd1  10534  le2add  10548  lesub2  10561  lesub3d  10683  supaddc  11028  supadd  11029  cju  11054  div4p1lem1div2  11325  difgtsumgt  11384  eluzmn  11732  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  addlelt  11980  xralrple  12074  xov1plusxeqvd  12356  zltaddlt1le  12362  elincfzoext  12565  fladdz  12666  2tnp1ge0ge0  12670  flhalf  12671  fldiv  12699  modaddmodup  12773  modaddmodlo  12774  addmodlteq  12785  discr1  13040  discr  13041  ccatalpha  13411  2cshw  13605  remim  13901  remullem  13912  sqrlem7  14033  absrele  14092  abstri  14114  abs3lem  14122  amgm2  14153  mulcn2  14370  o1add  14388  o1sub  14390  lo1add  14401  caucvgrlem  14447  iseraltlem2  14457  iseraltlem3  14458  fsumabs  14577  o1fsum  14589  climcndslem2  14626  tanhlt1  14934  eirrlem  14976  ruclem1  15004  ruclem2  15005  ruclem3  15006  ltoddhalfle  15132  bitscmp  15207  sadcaddlem  15226  sadasslem  15239  smuval2  15251  prmreclem4  15670  4sqlem5  15693  4sqlem6  15694  4sqlem12  15707  4sqlem15  15710  4sqlem16  15711  prmgaplem7  15808  prmgaplem8  15809  2expltfac  15846  cshwshashlem2  15850  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  prdsxmetlem  22220  xblss2ps  22253  metustexhalf  22408  nrmmetd  22426  ngptgp  22487  nlmvscnlem2  22536  nlmvscnlem1  22537  nmotri  22590  nghmplusg  22591  blcvx  22648  iccntr  22671  icccmplem2  22673  reconnlem2  22677  metdcnlem  22686  metnrmlem3  22711  cnllycmp  22802  lebnumii  22812  tchcphlem1  23080  ipcnlem2  23089  ipcnlem1  23090  csbren  23228  trirn  23229  minveclem2  23243  minveclem3b  23245  minveclem4  23249  ivthlem2  23267  ovolgelb  23294  ovollb2lem  23302  ovolunlem1a  23310  ovolunlem1  23311  ovolfiniun  23315  ovoliunlem1  23316  ovoliunlem2  23317  ovolshftlem1  23323  ovolscalem1  23327  ovolicopnf  23338  ismbl2  23341  nulmbl2  23350  unmbl  23351  voliunlem2  23365  ioombl1lem2  23373  ioombl1lem4  23375  ioombl1  23376  ioorcl2  23386  uniioombllem1  23395  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  uniioombl  23403  opnmbllem  23415  volcn  23420  itg1addlem4  23511  mbfi1fseqlem4  23530  mbfi1fseqlem6  23532  itg2splitlem  23560  itg2split  23561  itg2monolem3  23564  itg2addlem  23570  ibladdlem  23631  itgaddlem1  23634  itgaddlem2  23635  iblabslem  23639  iblabs  23640  dvferm1lem  23792  dvferm2lem  23794  dvlip2  23803  lhop1lem  23821  lhop1  23822  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcnvre  23827  dvcvx  23828  dvfsumlem3  23836  dvfsumlem4  23837  dvfsum2  23842  ftc1lem4  23847  coemullem  24051  ulmbdd  24197  ulmcn  24198  ulmdvlem1  24199  radcnvle  24219  pserdvlem1  24226  pserdv  24228  abelthlem7  24237  pilem2  24251  pilem3  24252  cosordlem  24322  abslogle  24409  logccv  24454  cxpaddle  24538  ang180lem2  24585  heron  24610  atanlogaddlem  24685  atans2  24703  cxp2limlem  24747  scvxcvx  24757  jensenlem2  24759  amgmlem  24761  logdiflbnd  24766  harmonicbnd4  24782  fsumharmonic  24783  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulmlem6  24805  lgambdd  24808  lgamucov  24809  regamcl  24832  ftalem5  24848  efnnfsumcl  24874  efchtdvds  24930  chtublem  24981  chtub  24982  logfaclbnd  24992  perfectlem2  25000  bcmono  25047  bposlem7  25060  bposlem9  25062  lgsdirprm  25101  gausslemma2dlem1a  25135  2sqlem8  25196  chpchtlim  25213  vmadivsumb  25217  rplogsumlem1  25218  dchrisumlem2  25224  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0re  25247  dchrisum0lem1b  25249  mulog2sumlem1  25268  mulog2sumlem2  25269  logsqvma2  25277  log2sumbnd  25278  selberglem2  25280  selbergb  25283  selberg2b  25286  chpdifbndlem1  25287  chpdifbndlem2  25288  selberg3lem2  25292  selberg3  25293  selberg4lem1  25294  selberg4  25295  pntrsumbnd2  25301  selberg3r  25303  selberg34r  25305  pntsf  25307  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntrlog2bnd  25318  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem2a  25324  pntibndlem2  25325  pntibndlem3  25326  pntlemg  25332  pntlemr  25336  pntlemk  25340  pntlemo  25341  pntlem3  25343  abvcxp  25349  padicabv  25364  ostth2lem2  25368  ostth3  25372  brbtwn2  25830  axsegconlem8  25849  axsegconlem10  25851  axpaschlem  25865  axpasch  25866  axeuclidlem  25887  axcontlem2  25890  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  vacn  27677  smcnlem  27680  ubthlem2  27855  minvecolem2  27859  minvecolem3  27860  minvecolem4  27864  minvecolem5  27865  nmoptrii  29081  hstle  29217  staddi  29233  stadd3i  29235  lt2addrd  29644  nndiffz1  29676  bhmafibid1  29772  fsumrp0cl  29823  pmtrto1cl  29977  fzto1st  29981  psgnfzto1st  29983  1smat1  29998  sqsscirc1  30082  cnre2csqlem  30084  tpr2rico  30086  nexple  30199  dya2iocress  30464  dya2iocbrsiga  30465  dya2icobrsiga  30466  dya2icoseg  30467  dya2iocucvr  30474  sxbrsigalem2  30476  omssubaddlem  30489  fibp1  30591  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsgt1  30700  ballotlemsel1i  30702  plymulx0  30752  breprexplemc  30838  breprexp  30839  logdivsqrle  30856  resconn  31354  faclim  31758  dnizphlfeqhlf  32591  dnibndlem4  32596  dnibndlem6  32598  dnibndlem8  32600  dnibndlem9  32601  dnibndlem10  32602  dnibndlem11  32603  dnibndlem13  32605  dnibnd  32606  knoppcnlem4  32611  unblimceq0lem  32622  unblimceq0  32623  unbdqndv2lem1  32625  poimirlem29  33568  heicant  33574  opnmbllem0  33575  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  mbfposadd  33587  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem1  33598  itgaddnclem2  33599  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  ftc1cnnclem  33613  ftc1anclem4  33618  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirclem5  33634  mettrifi  33683  isbnd3  33713  ssbnd  33717  cntotbnd  33725  heibor1lem  33738  bfplem2  33752  rrnequiv  33764  iccbnd  33769  pellexlem2  37711  pell1qrge1  37751  pell14qrgapw  37757  pellqrexplicit  37758  pellqrex  37760  pellfundge  37763  pellfundgt1  37764  rmspecfund  37791  rmxycomplete  37799  ltrmynn0  37832  jm2.24nn  37843  jm2.24  37847  fzmaxdif  37865  jm2.26lem3  37885  jm3.1lem2  37902  areaquad  38119  imo72b2lem0  38782  hashnzfzclim  38838  binomcxplemnotnn0  38872  zltlesub  39811  lt3addmuld  39829  absnpncan2d  39830  fperiodmullem  39831  lt4addmuld  39834  absnpncan3d  39835  leadd12dd  39845  supxrgelem  39866  supxrge  39867  ltadd12dd  39872  xralrple2  39883  infxr  39896  infleinflem2  39900  xralrple4  39902  xralrple3  39903  xrralrecnnle  39915  eliooshift  40047  iccshift  40062  iooshift  40066  iooiinicc  40087  iooiinioc  40101  fsumnncl  40121  climinf  40156  climsuselem1  40157  sumnnodd  40180  lptre2pt  40190  addlimc  40198  0ellimcdiv  40199  limclner  40201  climleltrp  40226  liminfltlem  40354  fperdvper  40451  dvdivbd  40456  dvbdfbdioolem2  40462  dvbdfbdioo  40463  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvxpaek  40473  dvnmul  40476  iblsplit  40500  iblspltprt  40507  itgspltprt  40513  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  stoweidlem1  40536  stoweidlem11  40546  stoweidlem13  40548  stoweidlem14  40549  stoweidlem20  40555  stoweidlem21  40556  stoweidlem26  40561  stoweidlem44  40579  stoweidlem60  40595  wallispilem3  40602  wallispilem4  40603  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  stirlinglem1  40609  stirlinglem3  40611  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  dirker2re  40627  dirkerval2  40629  dirkerre  40630  dirkerper  40631  dirkertrigeqlem1  40633  dirkertrigeqlem2  40634  dirkeritg  40637  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem4  40646  fourierdlem5  40647  fourierdlem6  40648  fourierdlem7  40649  fourierdlem9  40651  fourierdlem10  40652  fourierdlem18  40660  fourierdlem19  40661  fourierdlem20  40662  fourierdlem26  40668  fourierdlem28  40670  fourierdlem30  40672  fourierdlem35  40677  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem53  40694  fourierdlem57  40698  fourierdlem59  40700  fourierdlem60  40701  fourierdlem61  40702  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem66  40707  fourierdlem68  40709  fourierdlem71  40712  fourierdlem72  40713  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem79  40720  fourierdlem80  40721  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem84  40725  fourierdlem87  40728  fourierdlem88  40729  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem94  40735  fourierdlem95  40736  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  qndenserrnbllem  40832  ioorrnopnlem  40842  ioorrnopnxrlem  40844  sge0xaddlem1  40968  sge0xaddlem2  40969  omeiunltfirp  41054  carageniuncllem2  41057  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  hoiqssbllem1  41157  hoiqssbllem2  41158  hoiqssbllem3  41159  hspmbllem2  41162  hspmbllem3  41163  ovolval5lem1  41187  iinhoiicclem  41208  iinhoiicc  41209  iunhoiioolem  41210  iccvonmbllem  41213  vonioolem1  41215  vonioolem2  41216  vonicclem1  41218  vonicclem2  41219  preimaleiinlt  41252  salpreimaltle  41256  smfaddlem1  41292  smfadd  41294  smflimlem3  41302  smflimlem4  41303  smflimlem6  41305  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321  zm1nn  41641  perfectALTVlem2  41956  nnsum4primesevenALTV  42014  bgoldbtbndlem2  42019  dignn0flhalflem1  42734  amgmwlem  42876
  Copyright terms: Public domain W3C validator