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

Theorem readdcld 9925
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 9875 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6526  cr 9791   + caddc 9795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9853
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  ltadd2  9992  readdcan  10061  addid1  10067  leadd1  10347  le2add  10361  lesub2  10374  lesub3d  10496  supaddc  10839  supadd  10840  cju  10865  div4p1lem1div2  11136  difgtsumgt  11195  eluzmn  11528  rpnnen1lem5  11652  rpnnen1lem5OLD  11658  addlelt  11776  xralrple  11871  xov1plusxeqvd  12147  zltaddlt1le  12153  elincfzoext  12350  fladdz  12445  2tnp1ge0ge0  12449  flhalf  12450  fldiv  12478  modaddmodup  12552  modaddmodlo  12553  addmodlteq  12564  discr1  12819  discr  12820  ccatalpha  13176  2cshw  13358  remim  13653  remullem  13664  sqrlem7  13785  absrele  13844  abstri  13866  abs3lem  13874  amgm2  13905  mulcn2  14122  o1add  14140  o1sub  14142  lo1add  14153  caucvgrlem  14199  iseraltlem2  14209  iseraltlem3  14210  fsumabs  14322  o1fsum  14334  climcndslem2  14369  tanhlt1  14677  eirrlem  14719  ruclem1  14747  ruclem2  14748  ruclem3  14749  ltoddhalfle  14871  bitscmp  14946  sadcaddlem  14965  sadasslem  14978  smuval2  14990  prmreclem4  15409  4sqlem5  15432  4sqlem6  15433  4sqlem12  15446  4sqlem15  15449  4sqlem16  15450  prmgaplem7  15547  prmgaplem8  15548  2expltfac  15585  cshwshashlem2  15589  chfacfscmul0  20429  chfacfscmulgsum  20431  chfacfpmmul0  20433  chfacfpmmulgsum  20435  prdsxmetlem  21930  xblss2ps  21963  metustexhalf  22118  nrmmetd  22136  ngptgp  22197  nlmvscnlem2  22246  nlmvscnlem1  22247  nmotri  22300  nghmplusg  22301  blcvx  22356  iccntr  22379  icccmplem2  22381  reconnlem2  22385  metdcnlem  22394  metnrmlem3  22419  cnllycmp  22510  lebnumii  22520  tchcphlem1  22786  ipcnlem2  22795  ipcnlem1  22796  csbren  22934  trirn  22935  minveclem2  22949  minveclem3b  22951  minveclem4  22955  ivthlem2  22972  ovolgelb  22999  ovollb2lem  23007  ovolunlem1a  23015  ovolunlem1  23016  ovolfiniun  23020  ovoliunlem1  23021  ovoliunlem2  23022  ovolshftlem1  23028  ovolscalem1  23032  ovolicopnf  23043  ismbl2  23046  nulmbl2  23055  unmbl  23056  voliunlem2  23070  ioombl1lem2  23078  ioombl1lem4  23080  ioombl1  23081  ioorcl2  23090  uniioombllem1  23099  uniioombllem3  23103  uniioombllem4  23104  uniioombllem5  23105  uniioombl  23107  opnmbllem  23119  volcn  23124  itg1addlem4  23216  mbfi1fseqlem4  23235  mbfi1fseqlem6  23237  itg2splitlem  23265  itg2split  23266  itg2monolem3  23269  itg2addlem  23275  ibladdlem  23336  itgaddlem1  23339  itgaddlem2  23340  iblabslem  23344  iblabs  23345  dvferm1lem  23495  dvferm2lem  23497  dvlip2  23506  lhop1lem  23524  lhop1  23525  lhop  23527  dvcnvrelem1  23528  dvcnvrelem2  23529  dvcnvre  23530  dvcvx  23531  dvfsumlem3  23539  dvfsumlem4  23540  dvfsum2  23545  ftc1lem4  23550  coemullem  23754  ulmbdd  23900  ulmcn  23901  ulmdvlem1  23902  radcnvle  23922  pserdvlem1  23929  pserdv  23931  abelthlem7  23940  pilem2  23954  pilem3  23955  cosordlem  24025  abslogle  24112  logccv  24153  cxpaddle  24237  ang180lem2  24284  heron  24309  atanlogaddlem  24384  atans2  24402  cxp2limlem  24446  scvxcvx  24456  jensenlem2  24458  amgmlem  24460  logdiflbnd  24465  harmonicbnd4  24481  fsumharmonic  24482  lgamgulmlem3  24501  lgamgulmlem4  24502  lgamgulmlem5  24503  lgamgulmlem6  24504  lgambdd  24507  lgamucov  24508  regamcl  24531  ftalem5  24547  efnnfsumcl  24573  efchtdvds  24629  chtublem  24680  chtub  24681  logfaclbnd  24691  perfectlem2  24699  bcmono  24746  bposlem7  24759  bposlem9  24761  lgsdirprm  24800  gausslemma2dlem1a  24834  2sqlem8  24895  chpchtlim  24912  vmadivsumb  24916  rplogsumlem1  24917  dchrisumlem2  24923  dchrvmasumlem2  24931  dchrvmasumiflem1  24934  dchrisum0re  24946  dchrisum0lem1b  24948  mulog2sumlem1  24967  mulog2sumlem2  24968  logsqvma2  24976  log2sumbnd  24977  selberglem2  24979  selbergb  24982  selberg2b  24985  chpdifbndlem1  24986  chpdifbndlem2  24987  selberg3lem2  24991  selberg3  24992  selberg4lem1  24993  selberg4  24994  pntrsumbnd2  25000  selberg3r  25002  selberg34r  25004  pntsf  25006  pntrlog2bndlem1  25010  pntrlog2bndlem2  25011  pntrlog2bndlem4  25013  pntrlog2bndlem5  25014  pntrlog2bndlem6  25016  pntrlog2bnd  25017  pntpbnd1a  25018  pntpbnd2  25020  pntibndlem2a  25023  pntibndlem2  25024  pntibndlem3  25025  pntlemg  25031  pntlemr  25035  pntlemk  25039  pntlemo  25040  pntlem3  25042  abvcxp  25048  padicabv  25063  ostth2lem2  25067  ostth3  25071  brbtwn2  25530  axsegconlem8  25549  axsegconlem10  25551  axpaschlem  25565  axpasch  25566  axeuclidlem  25587  axcontlem2  25590  vacn  26726  smcnlem  26729  ubthlem2  26904  minvecolem2  26908  minvecolem3  26909  minvecolem4  26913  minvecolem5  26914  nmoptrii  28130  hstle  28266  staddi  28282  stadd3i  28284  lt2addrd  28696  nndiffz1  28729  bhmafibid1  28768  fsumrp0cl  28819  pmtrto1cl  28973  fzto1st  28977  psgnfzto1st  28979  1smat1  28991  sqsscirc1  29075  cnre2csqlem  29077  tpr2rico  29079  nexple  29192  dya2iocress  29456  dya2iocbrsiga  29457  dya2icobrsiga  29458  dya2icoseg  29459  dya2iocucvr  29466  sxbrsigalem2  29468  omssubaddlem  29481  fibp1  29583  ballotlemfc0  29674  ballotlemfcc  29675  ballotlemsgt1  29692  ballotlemsel1i  29694  plymulx0  29743  rescon  30275  faclim  30678  dnizphlfeqhlf  31429  dnibndlem4  31434  dnibndlem6  31436  dnibndlem8  31438  dnibndlem9  31439  dnibndlem10  31440  dnibndlem11  31441  dnibndlem13  31443  dnibnd  31444  knoppcnlem4  31449  unblimceq0lem  31460  unblimceq0  31461  unbdqndv2lem1  31463  poimirlem29  32391  heicant  32397  opnmbllem0  32398  mblfinlem3  32401  mblfinlem4  32402  ismblfin  32403  mbfposadd  32410  itg2addnclem  32414  itg2addnclem3  32416  itg2addnc  32417  itg2gt0cn  32418  ibladdnclem  32419  itgaddnclem1  32421  itgaddnclem2  32422  iblabsnclem  32426  iblabsnc  32427  iblmulc2nc  32428  ftc1cnnclem  32436  ftc1anclem4  32441  ftc1anclem7  32444  ftc1anclem8  32445  ftc1anc  32446  areacirclem5  32457  mettrifi  32506  isbnd3  32536  ssbnd  32540  cntotbnd  32548  heibor1lem  32561  bfplem2  32575  rrnequiv  32587  iccbnd  32592  pellexlem2  36195  pell1qrge1  36235  pell14qrgapw  36241  pellqrexplicit  36242  pellqrex  36244  pellfundge  36247  pellfundgt1  36248  rmspecfund  36275  rmxycomplete  36283  ltrmynn0  36316  jm2.24nn  36327  jm2.24  36331  fzmaxdif  36349  jm2.26lem3  36369  jm3.1lem2  36386  areaquad  36604  imo72b2lem0  37270  hashnzfzclim  37326  binomcxplemnotnn0  37360  zltlesub  38221  lt3addmuld  38239  absnpncan2d  38240  fperiodmullem  38241  lt4addmuld  38244  absnpncan3d  38245  leadd12dd  38256  supxrgelem  38277  supxrge  38278  ltadd12dd  38283  xralrple2  38294  infxr  38307  infleinflem2  38311  xralrple4  38313  xralrple3  38314  xrralrecnnle  38326  eliooshift  38359  iccshift  38374  iooshift  38378  iooiinicc  38399  iooiinioc  38413  fsumnncl  38421  climinf  38456  climsuselem1  38457  sumnnodd  38480  lptre2pt  38490  addlimc  38498  0ellimcdiv  38499  limclner  38501  climleltrp  38526  fperdvper  38591  dvdivbd  38596  dvbdfbdioolem2  38602  dvbdfbdioo  38603  ioodvbdlimc1lem1  38604  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvxpaek  38613  dvnmul  38616  iblsplit  38641  iblspltprt  38648  itgspltprt  38654  itgiccshift  38655  itgperiod  38656  itgsbtaddcnst  38657  stoweidlem1  38677  stoweidlem11  38687  stoweidlem13  38689  stoweidlem14  38690  stoweidlem20  38696  stoweidlem21  38697  stoweidlem26  38702  stoweidlem44  38720  stoweidlem60  38736  wallispilem3  38743  wallispilem4  38744  wallispilem5  38745  wallispi  38746  wallispi2lem1  38747  wallispi2lem2  38748  stirlinglem1  38750  stirlinglem3  38752  stirlinglem5  38754  stirlinglem6  38755  stirlinglem7  38756  stirlinglem10  38759  stirlinglem11  38760  stirlinglem12  38761  dirker2re  38768  dirkerval2  38770  dirkerre  38771  dirkerper  38772  dirkertrigeqlem1  38774  dirkertrigeqlem2  38775  dirkeritg  38778  dirkercncflem1  38779  dirkercncflem2  38780  dirkercncflem4  38782  fourierdlem4  38787  fourierdlem5  38788  fourierdlem6  38789  fourierdlem7  38790  fourierdlem9  38792  fourierdlem10  38793  fourierdlem18  38801  fourierdlem19  38802  fourierdlem20  38803  fourierdlem26  38809  fourierdlem28  38811  fourierdlem30  38813  fourierdlem35  38818  fourierdlem40  38823  fourierdlem41  38824  fourierdlem42  38825  fourierdlem47  38829  fourierdlem48  38830  fourierdlem49  38831  fourierdlem50  38832  fourierdlem51  38833  fourierdlem53  38835  fourierdlem57  38839  fourierdlem59  38841  fourierdlem60  38842  fourierdlem61  38843  fourierdlem63  38845  fourierdlem64  38846  fourierdlem65  38847  fourierdlem66  38848  fourierdlem68  38850  fourierdlem71  38853  fourierdlem72  38854  fourierdlem74  38856  fourierdlem75  38857  fourierdlem76  38858  fourierdlem78  38860  fourierdlem79  38861  fourierdlem80  38862  fourierdlem81  38863  fourierdlem82  38864  fourierdlem83  38865  fourierdlem84  38866  fourierdlem87  38869  fourierdlem88  38870  fourierdlem89  38871  fourierdlem90  38872  fourierdlem91  38873  fourierdlem92  38874  fourierdlem93  38875  fourierdlem94  38876  fourierdlem95  38877  fourierdlem97  38879  fourierdlem101  38883  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  fourierdlem112  38894  fourierdlem113  38895  sqwvfoura  38904  sqwvfourb  38905  fouriersw  38907  qndenserrnbllem  38973  ioorrnopnlem  38983  ioorrnopnxrlem  38985  sge0xaddlem1  39109  sge0xaddlem2  39110  omeiunltfirp  39192  carageniuncllem2  39195  hoidmv1lelem1  39264  hoidmv1lelem2  39265  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  hoiqssbllem1  39295  hoiqssbllem2  39296  hoiqssbllem3  39297  hspmbllem2  39300  hspmbllem3  39301  ovolval5lem1  39325  iinhoiicclem  39347  iinhoiicc  39348  iunhoiioolem  39349  iccvonmbllem  39352  vonioolem1  39354  vonioolem2  39355  vonicclem1  39357  vonicclem2  39358  preimaleiinlt  39391  salpreimaltle  39395  issmfltle  39405  smfaddlem1  39432  smfadd  39434  smflimlem3  39442  smflimlem4  39443  smflimlem6  39445  smfmullem1  39459  smfmullem2  39460  smfmullem3  39461  perfectALTVlem2  39949  nnsum4primesevenALTV  40001  bgoldbtbndlem2  40006  zm1nn  40154  crctcsh1wlkn0lem3  40996  crctcsh1wlkn0lem5  40998  dignn0flhalflem1  42188  amgmwlem  42299
  Copyright terms: Public domain W3C validator