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

Theorem readdcld 8862
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 8820 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684  (class class class)co 5858   RRcr 8736    + caddc 8740
This theorem is referenced by:  ltadd2  8924  readdcan  8986  addid1  8992  leadd1  9242  le2add  9256  lesub2  9269  cju  9742  rpnnen1lem5  10346  xralrple  10532  xov1plusxeqvd  10780  fladdz  10950  flhalf  10954  fldiv  10964  discr1  11237  discr  11238  remim  11602  remullem  11613  sqrlem7  11734  absrele  11793  abstri  11814  abs3lem  11822  amgm2  11853  mulcn2  12069  o1add  12087  o1sub  12089  lo1add  12100  caucvgrlem  12145  iseraltlem2  12155  iseraltlem3  12156  fsumabs  12259  o1fsum  12271  climcndslem2  12309  tanhlt1  12440  eirrlem  12482  ruclem1  12509  ruclem2  12510  ruclem3  12511  bitscmp  12629  sadcaddlem  12648  sadasslem  12661  smuval2  12673  prmreclem4  12966  4sqlem5  12989  4sqlem6  12990  4sqlem12  13003  4sqlem15  13006  4sqlem16  13007  2expltfac  13105  prdsxmetlem  17932  nrmmetd  18097  ngptgp  18152  nlmvscnlem2  18196  nlmvscnlem1  18197  nmotri  18248  nghmplusg  18249  blcvx  18304  iccntr  18326  icccmplem2  18328  reconnlem2  18332  metdcnlem  18341  metnrmlem3  18365  cnllycmp  18454  lebnumii  18464  tchcphlem1  18665  ipcnlem2  18671  ipcnlem1  18672  minveclem2  18790  minveclem3b  18792  minveclem4  18796  ivthlem2  18812  ovolgelb  18839  ovollb2lem  18847  ovolunlem1a  18855  ovolunlem1  18856  ovolfiniun  18860  ovoliunlem1  18861  ovoliunlem2  18862  ovolshftlem1  18868  ovolscalem1  18872  ovolicopnf  18883  ismbl2  18886  nulmbl2  18894  unmbl  18895  voliunlem2  18908  ioombl1lem2  18916  ioombl1lem4  18918  ioombl1  18919  ioorcl2  18927  uniioombllem1  18936  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  uniioombl  18944  opnmbllem  18956  volcn  18961  itg1addlem4  19054  mbfi1fseqlem4  19073  mbfi1fseqlem6  19075  itg2splitlem  19103  itg2split  19104  itg2monolem3  19107  itg2addlem  19113  ibladdlem  19174  itgaddlem1  19177  itgaddlem2  19178  iblabslem  19182  iblabs  19183  dvferm1lem  19331  dvferm2lem  19333  dvlip2  19342  lhop1lem  19360  lhop1  19361  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  dvcvx  19367  dvfsumlem3  19375  dvfsumlem4  19376  dvfsum2  19381  ftc1lem4  19386  coemullem  19631  ulmbdd  19775  ulmcn  19776  ulmdvlem1  19777  radcnvle  19796  pserdvlem1  19803  pserdv  19805  abelthlem7  19814  pilem2  19828  pilem3  19829  cosordlem  19893  logccv  20010  cxpaddle  20092  ang180lem2  20108  atanlogaddlem  20209  atans2  20227  cxp2limlem  20270  scvxcvx  20280  jensenlem2  20282  amgmlem  20284  harmonicbnd4  20304  fsumharmonic  20305  ftalem5  20314  efnnfsumcl  20340  efchtdvds  20397  chtublem  20450  chtub  20451  logfaclbnd  20461  perfectlem2  20469  bcmono  20516  bposlem7  20529  bposlem9  20531  lgsdirprm  20568  2sqlem8  20611  vmadivsumb  20632  rplogsumlem1  20633  dchrisumlem2  20639  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0re  20662  dchrisum0lem1b  20664  mulog2sumlem1  20683  mulog2sumlem2  20684  logsqvma2  20692  log2sumbnd  20693  selberglem2  20695  selbergb  20698  selberg2b  20701  chpdifbndlem1  20702  chpdifbndlem2  20703  selberg3lem2  20707  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrsumbnd2  20716  selberg3r  20718  selberg34r  20720  pntsf  20722  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem2a  20739  pntibndlem2  20740  pntibndlem3  20741  pntlemg  20747  pntlemr  20751  pntlemk  20755  pntlemo  20756  pntlem3  20758  abvcxp  20764  padicabv  20779  ostth2lem2  20783  ostth3  20787  vacn  21267  smcnlem  21270  ubthlem2  21450  minvecolem2  21454  minvecolem3  21455  minvecolem4  21459  minvecolem5  21460  nmoptrii  22674  hstle  22810  staddi  22826  stadd3i  22828  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsgt1  23069  ballotlemsel1i  23071  lt2addrd  23249  sqsscirc1  23292  cnre2csqlem  23294  cnre2csqima  23295  tpr2rico  23296  dya2iocress  23577  dya2iocbrsiga  23578  dya2iocseg  23579  rescon  23777  brbtwn2  24533  axsegconlem8  24552  axsegconlem10  24554  axpaschlem  24568  axpasch  24569  axeuclidlem  24590  axcontlem2  24593  areacirclem6  24930  altretop  25600  mslb1  25607  csbrn  26462  trirn  26463  mettrifi  26473  isbnd3  26508  ssbnd  26512  cntotbnd  26520  heibor1lem  26533  bfplem2  26547  rrnequiv  26559  iccbnd  26564  pellexlem2  26915  pell1qrge1  26955  pell14qrgapw  26961  pellqrexplicit  26962  pellqrex  26964  pellfundge  26967  pellfundgt1  26968  rmspecfund  26994  rmxycomplete  27002  ltrmynn0  27035  jm2.24nn  27046  jm2.24  27050  fzmaxdif  27068  jm2.26lem3  27094  jm3.1lem2  27111  climinf  27732  climsuselem1  27733  stoweidlem20  27769  stoweidlem21  27770  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem1  27823  stirlinglem3  27825  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 8798
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator