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

Theorem readdcld 9677
Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
readdcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
readdcld  |-  ( ph  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcld
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 readdcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 readdcl 9629 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872  (class class class)co 6305   RRcr 9545    + caddc 9549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9607
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  ltadd2  9745  readdcan  9814  addid1  9820  leadd1  10089  le2add  10103  lesub2  10116  lesub3d  10238  supaddc  10581  supadd  10582  cju  10612  rpnnen1lem5  11301  xralrple  11505  xov1plusxeqvd  11785  elincfzoext  11978  fladdz  12064  flhalf  12068  fldiv  12093  modaddmodup  12159  modaddmodlo  12160  discr1  12414  discr  12415  2cshw  12914  remim  13180  remullem  13191  sqrlem7  13312  absrele  13371  abstri  13393  abs3lem  13401  amgm2  13432  mulcn2  13658  o1add  13676  o1sub  13678  lo1add  13689  caucvgrlem  13735  caucvgrlemOLD  13736  iseraltlem2  13748  iseraltlem3  13749  fsumabs  13860  o1fsum  13872  climcndslem2  13907  tanhlt1  14213  eirrlem  14255  ruclem1  14282  ruclem2  14283  ruclem3  14284  bitscmp  14411  sadcaddlem  14430  sadasslem  14443  smuval2  14455  prmreclem4  14862  4sqlem5  14885  4sqlem6  14886  4sqlem12  14899  4sqlem15OLD  14902  4sqlem16OLD  14903  4sqlem15  14908  4sqlem16  14909  prmgaplem7  15026  prmgaplem8  15027  2expltfac  15062  cshwshashlem2  15066  chfacfscmul0  19880  chfacfscmulgsum  19882  chfacfpmmul0  19884  chfacfpmmulgsum  19886  prdsxmetlem  21381  xblss2ps  21414  metustexhalf  21569  nrmmetd  21587  ngptgp  21642  nlmvscnlem2  21686  nlmvscnlem1  21687  nmotri  21758  nghmplusg  21759  blcvx  21814  iccntr  21837  icccmplem2  21839  reconnlem2  21843  metdcnlem  21852  metnrmlem3  21876  metnrmlem3OLD  21891  cnllycmp  21982  lebnumii  21995  tchcphlem1  22207  ipcnlem2  22213  ipcnlem1  22214  csbren  22351  trirn  22352  minveclem2  22366  minveclem3b  22368  minveclem4  22372  minveclem2OLD  22378  minveclem3bOLD  22380  minveclem4OLD  22384  ivthlem2  22401  ovolgelb  22431  ovollb2lem  22439  ovolunlem1a  22447  ovolunlem1  22448  ovolfiniun  22452  ovoliunlem1  22453  ovoliunlem2  22454  ovolshftlem1  22460  ovolscalem1  22464  ovolicopnf  22476  ismbl2  22479  nulmbl2  22488  unmbl  22489  voliunlem2  22502  ioombl1lem2  22510  ioombl1lem4  22512  ioombl1  22513  ioorcl2  22522  uniioombllem1  22536  uniioombllem3  22541  uniioombllem4  22542  uniioombllem5  22543  uniioombl  22545  opnmbllem  22557  volcn  22562  itg1addlem4  22655  mbfi1fseqlem4  22674  mbfi1fseqlem6  22676  itg2splitlem  22704  itg2split  22705  itg2monolem3  22708  itg2addlem  22714  ibladdlem  22775  itgaddlem1  22778  itgaddlem2  22779  iblabslem  22783  iblabs  22784  dvferm1lem  22934  dvferm2lem  22936  dvlip2  22945  lhop1lem  22963  lhop1  22964  lhop  22966  dvcnvrelem1  22967  dvcnvrelem2  22968  dvcnvre  22969  dvcvx  22970  dvfsumlem3  22978  dvfsumlem4  22979  dvfsum2  22984  ftc1lem4  22989  coemullem  23202  ulmbdd  23351  ulmcn  23352  ulmdvlem1  23353  radcnvle  23373  pserdvlem1  23380  pserdv  23382  abelthlem7  23391  pilem2  23405  pilem2OLD  23406  pilem3  23407  pilem3OLD  23408  cosordlem  23478  abslogle  23565  logccv  23606  cxpaddle  23690  ang180lem2  23737  heron  23762  atanlogaddlem  23837  atans2  23855  cxp2limlem  23899  scvxcvx  23909  jensenlem2  23911  amgmlem  23913  logdiflbnd  23918  harmonicbnd4  23934  fsumharmonic  23935  lgamgulmlem3  23954  lgamgulmlem4  23955  lgamgulmlem5  23956  lgamgulmlem6  23957  lgambdd  23960  lgamucov  23961  regamcl  23984  ftalem5  23999  ftalem5OLD  24001  efnnfsumcl  24027  efchtdvds  24084  chtublem  24137  chtub  24138  logfaclbnd  24148  perfectlem2  24156  bcmono  24203  bposlem7  24216  bposlem9  24218  lgsdirprm  24255  2sqlem8  24298  chpchtlim  24315  vmadivsumb  24319  rplogsumlem1  24320  dchrisumlem2  24326  dchrvmasumlem2  24334  dchrvmasumiflem1  24337  dchrisum0re  24349  dchrisum0lem1b  24351  mulog2sumlem1  24370  mulog2sumlem2  24371  logsqvma2  24379  log2sumbnd  24380  selberglem2  24382  selbergb  24385  selberg2b  24388  chpdifbndlem1  24389  chpdifbndlem2  24390  selberg3lem2  24394  selberg3  24395  selberg4lem1  24396  selberg4  24397  pntrsumbnd2  24403  selberg3r  24405  selberg34r  24407  pntsf  24409  pntrlog2bndlem1  24413  pntrlog2bndlem2  24414  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  pntrlog2bndlem6  24419  pntrlog2bnd  24420  pntpbnd1a  24421  pntpbnd2  24423  pntibndlem2a  24426  pntibndlem2  24427  pntibndlem3  24428  pntlemg  24434  pntlemr  24438  pntlemk  24442  pntlemo  24443  pntlem3  24445  abvcxp  24451  padicabv  24466  ostth2lem2  24470  ostth3  24474  brbtwn2  24933  axsegconlem8  24952  axsegconlem10  24954  axpaschlem  24968  axpasch  24969  axeuclidlem  24990  axcontlem2  24993  vacn  26328  smcnlem  26331  ubthlem2  26511  minvecolem2  26515  minvecolem3  26516  minvecolem4  26520  minvecolem5  26521  minvecolem2OLD  26525  minvecolem3OLD  26526  minvecolem4OLD  26530  minvecolem5OLD  26531  nmoptrii  27745  hstle  27881  staddi  27897  stadd3i  27899  lt2addrd  28332  nndiffz1  28372  bhmafibid1  28412  fsumrp0cl  28465  pmtrto1cl  28620  fzto1st  28624  psgnfzto1st  28626  1smat1  28638  sqsscirc1  28722  cnre2csqlem  28724  tpr2rico  28726  nexple  28839  dya2iocress  29104  dya2iocbrsiga  29105  dya2icobrsiga  29106  dya2icoseg  29107  dya2iocucvr  29114  sxbrsigalem2  29116  omssubaddlem  29135  omssubaddlemOLD  29139  fibp1  29242  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemsgt1  29351  ballotlemsel1i  29353  ballotlemsgt1OLD  29389  ballotlemsel1iOLD  29391  eluzmn  29431  plymulx0  29444  rescon  29977  faclim  30389  poimirlem29  31933  heicant  31939  opnmbllem0  31940  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  mbfposadd  31952  itg2addnclem  31957  itg2addnclem3  31959  itg2addnc  31960  itg2gt0cn  31961  ibladdnclem  31962  itgaddnclem1  31964  itgaddnclem2  31965  iblabsnclem  31969  iblabsnc  31970  iblmulc2nc  31971  ftc1cnnclem  31979  ftc1anclem4  31984  ftc1anclem7  31987  ftc1anclem8  31988  ftc1anc  31989  areacirclem5  32000  mettrifi  32050  isbnd3  32080  ssbnd  32084  cntotbnd  32092  heibor1lem  32105  bfplem2  32119  rrnequiv  32131  iccbnd  32136  pellexlem2  35644  pell1qrge1  35686  pell14qrgapw  35692  pellqrexplicit  35693  pellqrex  35696  pellfundge  35700  pellfundgt1  35701  rmspecfund  35727  rmxycomplete  35735  ltrmynn0  35768  jm2.24nn  35779  jm2.24  35783  fzmaxdif  35801  jm2.26lem3  35826  jm3.1lem2  35843  areaquad  36071  imo72b2lem0  36578  hashnzfzclim  36641  binomcxplemnotnn0  36675  zltlesub  37449  lt3addmuld  37473  absnpncan2d  37474  fperiodmullem  37475  lt4addmuld  37478  absnpncan3d  37479  leadd12dd  37492  supxrgelem  37514  supxrge  37515  ltadd12dd  37520  xralrple2  37531  eliooshift  37553  iccshift  37568  iooshift  37572  fsumnncl  37591  climinf  37624  climinfOLD  37625  climsuselem1  37626  sumnnodd  37650  lptre2pt  37660  addlimc  37669  0ellimcdiv  37670  limclner  37672  fperdvper  37730  dvdivbd  37735  dvbdfbdioolem2  37741  dvbdfbdioo  37742  ioodvbdlimc1lem1  37743  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem1OLD  37745  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvxpaek  37755  dvnmul  37758  iblsplit  37783  iblspltprt  37790  itgspltprt  37796  itgiccshift  37797  itgperiod  37798  itgsbtaddcnst  37799  stoweidlem1  37801  stoweidlem11  37811  stoweidlem13  37813  stoweidlem14  37814  stoweidlem20  37820  stoweidlem21  37821  stoweidlem26  37826  stoweidlem44  37845  stoweidlem60  37861  wallispilem3  37869  wallispilem4  37870  wallispilem5  37871  wallispi  37872  wallispi2lem1  37873  wallispi2lem2  37874  stirlinglem1  37876  stirlinglem3  37878  stirlinglem5  37880  stirlinglem6  37881  stirlinglem7  37882  stirlinglem10  37885  stirlinglem11  37886  stirlinglem12  37887  dirker2re  37894  dirkerval2  37896  dirkerre  37897  dirkerper  37898  dirkertrigeqlem1  37900  dirkertrigeqlem2  37901  dirkeritg  37904  dirkercncflem1  37905  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem4  37913  fourierdlem5  37914  fourierdlem6  37915  fourierdlem7  37916  fourierdlem9  37918  fourierdlem10  37919  fourierdlem18  37927  fourierdlem19  37928  fourierdlem20  37929  fourierdlem26  37935  fourierdlem28  37937  fourierdlem30  37939  fourierdlem35  37945  fourierdlem40  37950  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem47  37957  fourierdlem48  37958  fourierdlem49  37959  fourierdlem50  37960  fourierdlem51  37961  fourierdlem53  37963  fourierdlem57  37967  fourierdlem59  37969  fourierdlem60  37970  fourierdlem61  37971  fourierdlem63  37973  fourierdlem64  37974  fourierdlem65  37975  fourierdlem66  37976  fourierdlem68  37978  fourierdlem71  37981  fourierdlem72  37982  fourierdlem74  37984  fourierdlem75  37985  fourierdlem76  37986  fourierdlem78  37988  fourierdlem79  37989  fourierdlem80  37990  fourierdlem81  37991  fourierdlem82  37992  fourierdlem83  37993  fourierdlem84  37994  fourierdlem87  37997  fourierdlem88  37998  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem92  38002  fourierdlem93  38003  fourierdlem94  38004  fourierdlem95  38005  fourierdlem97  38007  fourierdlem101  38011  fourierdlem103  38013  fourierdlem104  38014  fourierdlem111  38021  fourierdlem112  38022  fourierdlem113  38023  sqwvfoura  38032  sqwvfourb  38033  fouriersw  38035  sge0xaddlem1  38183  sge0xaddlem2  38184  omeiunltfirp  38248  carageniuncllem2  38251  hoidmv1lelem1  38317  hoidmv1lelem2  38318  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  hoidmvlelem4  38324  perfectALTVlem2  38714  evengpoap3  38764  nnsum4primesevenALTV  38766  bgoldbtbndlem2  38771  zm1nn  38903  dignn0flhalflem1  40048
  Copyright terms: Public domain W3C validator