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

Theorem readdcld 9623
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 9575 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802  (class class class)co 6278   RRcr 9491    + caddc 9495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9553
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ltadd2  9688  readdcan  9754  addid1  9760  leadd1  10023  le2add  10037  lesub2  10050  cju  10535  rpnnen1lem5  11218  xralrple  11410  xov1plusxeqvd  11672  fladdz  11934  flhalf  11938  fldiv  11963  modaddmodup  12026  modaddmodlo  12027  discr1  12278  discr  12279  2cshw  12757  remim  12926  remullem  12937  sqrlem7  13058  absrele  13117  abstri  13139  abs3lem  13147  amgm2  13178  mulcn2  13394  o1add  13412  o1sub  13414  lo1add  13425  caucvgrlem  13471  iseraltlem2  13481  iseraltlem3  13482  fsumabs  13591  o1fsum  13603  climcndslem2  13638  tanhlt1  13769  eirrlem  13811  ruclem1  13838  ruclem2  13839  ruclem3  13840  bitscmp  13962  sadcaddlem  13981  sadasslem  13994  smuval2  14006  prmreclem4  14311  4sqlem5  14334  4sqlem6  14335  4sqlem12  14348  4sqlem15  14351  4sqlem16  14352  2expltfac  14451  cshwshashlem2  14455  chfacfscmul0  19229  chfacfscmulgsum  19231  chfacfpmmul0  19233  chfacfpmmulgsum  19235  prdsxmetlem  20741  xblss2ps  20774  metustexhalfOLD  20936  metustexhalf  20937  nrmmetd  20965  ngptgp  21020  nlmvscnlem2  21064  nlmvscnlem1  21065  nmotri  21116  nghmplusg  21117  blcvx  21173  iccntr  21196  icccmplem2  21198  reconnlem2  21202  metdcnlem  21211  metnrmlem3  21235  cnllycmp  21326  lebnumii  21336  tchcphlem1  21548  ipcnlem2  21554  ipcnlem1  21555  csbren  21696  trirn  21697  minveclem2  21711  minveclem3b  21713  minveclem4  21717  ivthlem2  21734  ovolgelb  21761  ovollb2lem  21769  ovolunlem1a  21777  ovolunlem1  21778  ovolfiniun  21782  ovoliunlem1  21783  ovoliunlem2  21784  ovolshftlem1  21790  ovolscalem1  21794  ovolicopnf  21805  ismbl2  21808  nulmbl2  21817  unmbl  21818  voliunlem2  21831  ioombl1lem2  21839  ioombl1lem4  21841  ioombl1  21842  ioorcl2  21851  uniioombllem1  21860  uniioombllem3  21864  uniioombllem4  21865  uniioombllem5  21866  uniioombl  21868  opnmbllem  21880  volcn  21885  itg1addlem4  21976  mbfi1fseqlem4  21995  mbfi1fseqlem6  21997  itg2splitlem  22025  itg2split  22026  itg2monolem3  22029  itg2addlem  22035  ibladdlem  22096  itgaddlem1  22099  itgaddlem2  22100  iblabslem  22104  iblabs  22105  dvferm1lem  22255  dvferm2lem  22257  dvlip2  22266  lhop1lem  22284  lhop1  22285  lhop  22287  dvcnvrelem1  22288  dvcnvrelem2  22289  dvcnvre  22290  dvcvx  22291  dvfsumlem3  22299  dvfsumlem4  22300  dvfsum2  22305  ftc1lem4  22310  coemullem  22516  ulmbdd  22662  ulmcn  22663  ulmdvlem1  22664  radcnvle  22684  pserdvlem1  22691  pserdv  22693  abelthlem7  22702  pilem2  22716  pilem3  22717  cosordlem  22787  abslogle  22872  logccv  22913  cxpaddle  22995  ang180lem2  23011  heron  23038  atanlogaddlem  23113  atans2  23131  cxp2limlem  23174  scvxcvx  23184  jensenlem2  23186  amgmlem  23188  logdiflbnd  23193  harmonicbnd4  23209  fsumharmonic  23210  ftalem5  23219  efnnfsumcl  23245  efchtdvds  23302  chtublem  23355  chtub  23356  logfaclbnd  23366  perfectlem2  23374  bcmono  23421  bposlem7  23434  bposlem9  23436  lgsdirprm  23473  2sqlem8  23516  chpchtlim  23533  vmadivsumb  23537  rplogsumlem1  23538  dchrisumlem2  23544  dchrvmasumlem2  23552  dchrvmasumiflem1  23555  dchrisum0re  23567  dchrisum0lem1b  23569  mulog2sumlem1  23588  mulog2sumlem2  23589  logsqvma2  23597  log2sumbnd  23598  selberglem2  23600  selbergb  23603  selberg2b  23606  chpdifbndlem1  23607  chpdifbndlem2  23608  selberg3lem2  23612  selberg3  23613  selberg4lem1  23614  selberg4  23615  pntrsumbnd2  23621  selberg3r  23623  selberg34r  23625  pntsf  23627  pntrlog2bndlem1  23631  pntrlog2bndlem2  23632  pntrlog2bndlem4  23634  pntrlog2bndlem5  23635  pntrlog2bndlem6  23637  pntrlog2bnd  23638  pntpbnd1a  23639  pntpbnd2  23641  pntibndlem2a  23644  pntibndlem2  23645  pntibndlem3  23646  pntlemg  23652  pntlemr  23656  pntlemk  23660  pntlemo  23661  pntlem3  23663  abvcxp  23669  padicabv  23684  ostth2lem2  23688  ostth3  23692  brbtwn2  24077  axsegconlem8  24096  axsegconlem10  24098  axpaschlem  24112  axpasch  24113  axeuclidlem  24134  axcontlem2  24137  vacn  25473  smcnlem  25476  ubthlem2  25656  minvecolem2  25660  minvecolem3  25661  minvecolem4  25665  minvecolem5  25666  nmoptrii  26882  hstle  27018  staddi  27034  stadd3i  27036  lt2addrd  27432  nndiffz1  27465  bhmafibid1  27502  fsumrp0cl  27555  sqsscirc1  27760  cnre2csqlem  27762  tpr2rico  27764  nexple  27875  dya2iocress  28115  dya2iocbrsiga  28116  dya2icobrsiga  28117  dya2icoseg  28118  dya2iocucvr  28125  sxbrsigalem2  28127  fibp1  28210  ballotlemfc0  28301  ballotlemfcc  28302  ballotlemsgt1  28319  ballotlemsel1i  28321  eluzmn  28361  plymulx0  28374  lgamgulmlem3  28443  lgamgulmlem4  28444  lgamgulmlem5  28445  lgamgulmlem6  28446  lgambdd  28449  lgamucov  28450  regamcl  28473  rescon  28561  faclim  29143  supaddc  30013  supadd  30014  heicant  30021  opnmbllem0  30022  mblfinlem3  30025  mblfinlem4  30026  ismblfin  30027  mbfposadd  30034  itg2addnclem  30038  itg2addnclem3  30040  itg2addnc  30041  itg2gt0cn  30042  ibladdnclem  30043  itgaddnclem1  30045  itgaddnclem2  30046  iblabsnclem  30050  iblabsnc  30051  iblmulc2nc  30052  ftc1cnnclem  30060  ftc1anclem4  30065  ftc1anclem7  30068  ftc1anclem8  30069  ftc1anc  30070  areacirclem5  30083  mettrifi  30222  isbnd3  30252  ssbnd  30256  cntotbnd  30264  heibor1lem  30277  bfplem2  30291  rrnequiv  30303  iccbnd  30308  pellexlem2  30738  pell1qrge1  30778  pell14qrgapw  30784  pellqrexplicit  30785  pellqrex  30787  pellfundge  30790  pellfundgt1  30791  rmspecfund  30817  rmxycomplete  30825  ltrmynn0  30858  jm2.24nn  30869  jm2.24  30873  fzmaxdif  30891  jm2.26lem3  30915  jm3.1lem2  30932  areaquad  31157  hashnzfzclim  31200  zltlesub  31417  lt3addmuld  31450  absnpncan2d  31451  fperiodmullem  31452  lt4addmuld  31455  absnpncan3d  31456  eliooshift  31477  iccshift  31494  iooshift  31498  climinf  31520  climsuselem1  31521  sumnnodd  31544  lptre2pt  31554  addlimc  31562  0ellimcdiv  31563  limclner  31565  fperdvper  31619  dvdivbd  31624  dvbdfbdioolem2  31630  dvbdfbdioo  31631  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  iblsplit  31655  iblspltprt  31662  itgspltprt  31668  itgiccshift  31669  itgperiod  31670  itgsbtaddcnst  31671  stoweidlem1  31672  stoweidlem11  31682  stoweidlem13  31684  stoweidlem14  31685  stoweidlem20  31691  stoweidlem21  31692  stoweidlem26  31697  stoweidlem44  31715  stoweidlem60  31731  wallispilem3  31738  wallispilem4  31739  wallispilem5  31740  wallispi  31741  wallispi2lem1  31742  wallispi2lem2  31743  stirlinglem1  31745  stirlinglem3  31747  stirlinglem5  31749  stirlinglem6  31750  stirlinglem7  31751  stirlinglem10  31754  stirlinglem11  31755  stirlinglem12  31756  dirker2re  31763  dirkerval2  31765  dirkerre  31766  dirkerper  31767  dirkertrigeqlem1  31769  dirkertrigeqlem2  31770  dirkeritg  31773  dirkercncflem1  31774  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem4  31782  fourierdlem5  31783  fourierdlem6  31784  fourierdlem7  31785  fourierdlem9  31787  fourierdlem10  31788  fourierdlem18  31796  fourierdlem19  31797  fourierdlem20  31798  fourierdlem26  31804  fourierdlem28  31806  fourierdlem30  31808  fourierdlem35  31813  fourierdlem40  31818  fourierdlem41  31819  fourierdlem42  31820  fourierdlem47  31825  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem51  31829  fourierdlem53  31831  fourierdlem57  31835  fourierdlem59  31837  fourierdlem60  31838  fourierdlem61  31839  fourierdlem63  31841  fourierdlem64  31842  fourierdlem65  31843  fourierdlem66  31844  fourierdlem68  31846  fourierdlem71  31849  fourierdlem72  31850  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem78  31856  fourierdlem79  31857  fourierdlem80  31858  fourierdlem81  31859  fourierdlem82  31860  fourierdlem83  31861  fourierdlem84  31862  fourierdlem87  31865  fourierdlem88  31866  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem92  31870  fourierdlem93  31871  fourierdlem94  31872  fourierdlem95  31873  fourierdlem97  31875  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  fourierdlem112  31890  fourierdlem113  31891  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  zm1nn  32163  imo72b2lem0  37634
  Copyright terms: Public domain W3C validator