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

Theorem readdcld 9657
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 9609 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 671 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1891  (class class class)co 6276   RRcr 9525    + caddc 9529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9587
This theorem depends on definitions:  df-bi 190  df-an 377
This theorem is referenced by:  ltadd2  9725  readdcan  9794  addid1  9800  leadd1  10071  le2add  10085  lesub2  10098  lesub3d  10220  supaddc  10563  supadd  10564  cju  10594  rpnnen1lem5  11284  xralrple  11488  xov1plusxeqvd  11769  elincfzoext  11965  fladdz  12052  flhalf  12056  fldiv  12081  modaddmodup  12147  modaddmodlo  12148  discr1  12402  discr  12403  2cshw  12911  remim  13191  remullem  13202  sqrlem7  13323  absrele  13382  abstri  13404  abs3lem  13412  amgm2  13443  mulcn2  13670  o1add  13688  o1sub  13690  lo1add  13701  caucvgrlem  13747  caucvgrlemOLD  13748  iseraltlem2  13760  iseraltlem3  13761  fsumabs  13872  o1fsum  13884  climcndslem2  13919  tanhlt1  14225  eirrlem  14267  ruclem1  14294  ruclem2  14295  ruclem3  14296  bitscmp  14423  sadcaddlem  14442  sadasslem  14455  smuval2  14467  prmreclem4  14874  4sqlem5  14897  4sqlem6  14898  4sqlem12  14911  4sqlem15OLD  14914  4sqlem16OLD  14915  4sqlem15  14920  4sqlem16  14921  prmgaplem7  15038  prmgaplem8  15039  2expltfac  15074  cshwshashlem2  15078  chfacfscmul0  19893  chfacfscmulgsum  19895  chfacfpmmul0  19897  chfacfpmmulgsum  19899  prdsxmetlem  21394  xblss2ps  21427  metustexhalf  21582  nrmmetd  21600  ngptgp  21655  nlmvscnlem2  21699  nlmvscnlem1  21700  nmotri  21771  nghmplusg  21772  blcvx  21827  iccntr  21850  icccmplem2  21852  reconnlem2  21856  metdcnlem  21865  metnrmlem3  21889  metnrmlem3OLD  21904  cnllycmp  21995  lebnumii  22008  tchcphlem1  22220  ipcnlem2  22226  ipcnlem1  22227  csbren  22364  trirn  22365  minveclem2  22379  minveclem3b  22381  minveclem4  22385  minveclem2OLD  22391  minveclem3bOLD  22393  minveclem4OLD  22397  ivthlem2  22414  ovolgelb  22444  ovollb2lem  22452  ovolunlem1a  22460  ovolunlem1  22461  ovolfiniun  22465  ovoliunlem1  22466  ovoliunlem2  22467  ovolshftlem1  22473  ovolscalem1  22477  ovolicopnf  22489  ismbl2  22492  nulmbl2  22501  unmbl  22502  voliunlem2  22516  ioombl1lem2  22524  ioombl1lem4  22526  ioombl1  22527  ioorcl2  22536  uniioombllem1  22550  uniioombllem3  22555  uniioombllem4  22556  uniioombllem5  22557  uniioombl  22559  opnmbllem  22571  volcn  22576  itg1addlem4  22669  mbfi1fseqlem4  22688  mbfi1fseqlem6  22690  itg2splitlem  22718  itg2split  22719  itg2monolem3  22722  itg2addlem  22728  ibladdlem  22789  itgaddlem1  22792  itgaddlem2  22793  iblabslem  22797  iblabs  22798  dvferm1lem  22948  dvferm2lem  22950  dvlip2  22959  lhop1lem  22977  lhop1  22978  lhop  22980  dvcnvrelem1  22981  dvcnvrelem2  22982  dvcnvre  22983  dvcvx  22984  dvfsumlem3  22992  dvfsumlem4  22993  dvfsum2  22998  ftc1lem4  23003  coemullem  23216  ulmbdd  23365  ulmcn  23366  ulmdvlem1  23367  radcnvle  23387  pserdvlem1  23394  pserdv  23396  abelthlem7  23405  pilem2  23419  pilem2OLD  23420  pilem3  23421  pilem3OLD  23422  cosordlem  23492  abslogle  23579  logccv  23620  cxpaddle  23704  ang180lem2  23751  heron  23776  atanlogaddlem  23851  atans2  23869  cxp2limlem  23913  scvxcvx  23923  jensenlem2  23925  amgmlem  23927  logdiflbnd  23932  harmonicbnd4  23948  fsumharmonic  23949  lgamgulmlem3  23968  lgamgulmlem4  23969  lgamgulmlem5  23970  lgamgulmlem6  23971  lgambdd  23974  lgamucov  23975  regamcl  23998  ftalem5  24013  ftalem5OLD  24015  efnnfsumcl  24041  efchtdvds  24098  chtublem  24151  chtub  24152  logfaclbnd  24162  perfectlem2  24170  bcmono  24217  bposlem7  24230  bposlem9  24232  lgsdirprm  24269  2sqlem8  24312  chpchtlim  24329  vmadivsumb  24333  rplogsumlem1  24334  dchrisumlem2  24340  dchrvmasumlem2  24348  dchrvmasumiflem1  24351  dchrisum0re  24363  dchrisum0lem1b  24365  mulog2sumlem1  24384  mulog2sumlem2  24385  logsqvma2  24393  log2sumbnd  24394  selberglem2  24396  selbergb  24399  selberg2b  24402  chpdifbndlem1  24403  chpdifbndlem2  24404  selberg3lem2  24408  selberg3  24409  selberg4lem1  24410  selberg4  24411  pntrsumbnd2  24417  selberg3r  24419  selberg34r  24421  pntsf  24423  pntrlog2bndlem1  24427  pntrlog2bndlem2  24428  pntrlog2bndlem4  24430  pntrlog2bndlem5  24431  pntrlog2bndlem6  24433  pntrlog2bnd  24434  pntpbnd1a  24435  pntpbnd2  24437  pntibndlem2a  24440  pntibndlem2  24441  pntibndlem3  24442  pntlemg  24448  pntlemr  24452  pntlemk  24456  pntlemo  24457  pntlem3  24459  abvcxp  24465  padicabv  24480  ostth2lem2  24484  ostth3  24488  brbtwn2  24947  axsegconlem8  24966  axsegconlem10  24968  axpaschlem  24982  axpasch  24983  axeuclidlem  25004  axcontlem2  25007  vacn  26342  smcnlem  26345  ubthlem2  26525  minvecolem2  26529  minvecolem3  26530  minvecolem4  26534  minvecolem5  26535  minvecolem2OLD  26539  minvecolem3OLD  26540  minvecolem4OLD  26544  minvecolem5OLD  26545  nmoptrii  27759  hstle  27895  staddi  27911  stadd3i  27913  lt2addrd  28334  nndiffz1  28374  bhmafibid1  28413  fsumrp0cl  28465  pmtrto1cl  28619  fzto1st  28623  psgnfzto1st  28625  1smat1  28637  sqsscirc1  28721  cnre2csqlem  28723  tpr2rico  28725  nexple  28838  dya2iocress  29102  dya2iocbrsiga  29103  dya2icobrsiga  29104  dya2icoseg  29105  dya2iocucvr  29112  sxbrsigalem2  29114  omssubaddlem  29133  omssubaddlemOLD  29137  fibp1  29240  ballotlemfc0  29331  ballotlemfcc  29332  ballotlemsgt1  29349  ballotlemsel1i  29351  ballotlemsgt1OLD  29387  ballotlemsel1iOLD  29389  eluzmn  29429  plymulx0  29442  rescon  29975  faclim  30388  poimirlem29  31971  heicant  31977  opnmbllem0  31978  mblfinlem3  31981  mblfinlem4  31982  ismblfin  31983  mbfposadd  31990  itg2addnclem  31995  itg2addnclem3  31997  itg2addnc  31998  itg2gt0cn  31999  ibladdnclem  32000  itgaddnclem1  32002  itgaddnclem2  32003  iblabsnclem  32007  iblabsnc  32008  iblmulc2nc  32009  ftc1cnnclem  32017  ftc1anclem4  32022  ftc1anclem7  32025  ftc1anclem8  32026  ftc1anc  32027  areacirclem5  32038  mettrifi  32088  isbnd3  32118  ssbnd  32122  cntotbnd  32130  heibor1lem  32143  bfplem2  32157  rrnequiv  32169  iccbnd  32174  pellexlem2  35676  pell1qrge1  35718  pell14qrgapw  35724  pellqrexplicit  35725  pellqrex  35728  pellfundge  35732  pellfundgt1  35733  rmspecfund  35759  rmxycomplete  35767  ltrmynn0  35800  jm2.24nn  35811  jm2.24  35815  fzmaxdif  35833  jm2.26lem3  35858  jm3.1lem2  35875  areaquad  36103  imo72b2lem0  36610  hashnzfzclim  36672  binomcxplemnotnn0  36706  zltlesub  37526  lt3addmuld  37550  absnpncan2d  37551  fperiodmullem  37552  lt4addmuld  37555  absnpncan3d  37556  leadd12dd  37569  supxrgelem  37591  supxrge  37592  ltadd12dd  37597  xralrple2  37608  infxr  37622  infleinflem2  37626  eliooshift  37645  iccshift  37660  iooshift  37664  fsumnncl  37691  climinf  37726  climinfOLD  37727  climsuselem1  37728  sumnnodd  37752  lptre2pt  37762  addlimc  37771  0ellimcdiv  37772  limclner  37774  fperdvper  37832  dvdivbd  37837  dvbdfbdioolem2  37843  dvbdfbdioo  37844  ioodvbdlimc1lem1  37845  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem1OLD  37847  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  dvxpaek  37857  dvnmul  37860  iblsplit  37885  iblspltprt  37892  itgspltprt  37898  itgiccshift  37899  itgperiod  37900  itgsbtaddcnst  37901  stoweidlem1  37918  stoweidlem11  37928  stoweidlem13  37930  stoweidlem14  37931  stoweidlem20  37937  stoweidlem21  37938  stoweidlem26  37943  stoweidlem44  37962  stoweidlem60  37978  wallispilem3  37986  wallispilem4  37987  wallispilem5  37988  wallispi  37989  wallispi2lem1  37990  wallispi2lem2  37991  stirlinglem1  37993  stirlinglem3  37995  stirlinglem5  37997  stirlinglem6  37998  stirlinglem7  37999  stirlinglem10  38002  stirlinglem11  38003  stirlinglem12  38004  dirker2re  38011  dirkerval2  38013  dirkerre  38014  dirkerper  38015  dirkertrigeqlem1  38017  dirkertrigeqlem2  38018  dirkeritg  38021  dirkercncflem1  38022  dirkercncflem2  38023  dirkercncflem4  38025  fourierdlem4  38030  fourierdlem5  38031  fourierdlem6  38032  fourierdlem7  38033  fourierdlem9  38035  fourierdlem10  38036  fourierdlem18  38044  fourierdlem19  38045  fourierdlem20  38046  fourierdlem26  38052  fourierdlem28  38054  fourierdlem30  38056  fourierdlem35  38062  fourierdlem40  38067  fourierdlem41  38068  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem47  38074  fourierdlem48  38075  fourierdlem49  38076  fourierdlem50  38077  fourierdlem51  38078  fourierdlem53  38080  fourierdlem57  38084  fourierdlem59  38086  fourierdlem60  38087  fourierdlem61  38088  fourierdlem63  38090  fourierdlem64  38091  fourierdlem65  38092  fourierdlem66  38093  fourierdlem68  38095  fourierdlem71  38098  fourierdlem72  38099  fourierdlem74  38101  fourierdlem75  38102  fourierdlem76  38103  fourierdlem78  38105  fourierdlem79  38106  fourierdlem80  38107  fourierdlem81  38108  fourierdlem82  38109  fourierdlem83  38110  fourierdlem84  38111  fourierdlem87  38114  fourierdlem88  38115  fourierdlem89  38116  fourierdlem90  38117  fourierdlem91  38118  fourierdlem92  38119  fourierdlem93  38120  fourierdlem94  38121  fourierdlem95  38122  fourierdlem97  38124  fourierdlem101  38128  fourierdlem103  38130  fourierdlem104  38131  fourierdlem111  38138  fourierdlem112  38139  fourierdlem113  38140  sqwvfoura  38149  sqwvfourb  38150  fouriersw  38152  qndenserrnbllem  38220  sge0xaddlem1  38334  sge0xaddlem2  38335  omeiunltfirp  38404  carageniuncllem2  38407  hoidmv1lelem1  38476  hoidmv1lelem2  38477  hoidmvlelem1  38480  hoidmvlelem2  38481  hoidmvlelem3  38482  hoidmvlelem4  38483  hoiqssbllem1  38507  hoiqssbllem2  38508  hoiqssbllem3  38509  hspmbllem2  38512  hspmbllem3  38513  ovolval5lem1  38537  perfectALTVlem2  38935  evengpoap3  38985  nnsum4primesevenALTV  38987  bgoldbtbndlem2  38992  zm1nn  39143  dignn0flhalflem1  40751
  Copyright terms: Public domain W3C validator