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

Theorem readdcld 8907
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 8865 . 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 1701  (class class class)co 5900   RRcr 8781    + caddc 8785
This theorem is referenced by:  ltadd2  8969  readdcan  9031  addid1  9037  leadd1  9287  le2add  9301  lesub2  9314  cju  9787  rpnnen1lem5  10393  xralrple  10579  xov1plusxeqvd  10827  fladdz  10997  flhalf  11001  fldiv  11011  discr1  11284  discr  11285  remim  11649  remullem  11660  sqrlem7  11781  absrele  11840  abstri  11861  abs3lem  11869  amgm2  11900  mulcn2  12116  o1add  12134  o1sub  12136  lo1add  12147  caucvgrlem  12192  iseraltlem2  12202  iseraltlem3  12203  fsumabs  12306  o1fsum  12318  climcndslem2  12356  tanhlt1  12487  eirrlem  12529  ruclem1  12556  ruclem2  12557  ruclem3  12558  bitscmp  12676  sadcaddlem  12695  sadasslem  12708  smuval2  12720  prmreclem4  13013  4sqlem5  13036  4sqlem6  13037  4sqlem12  13050  4sqlem15  13053  4sqlem16  13054  2expltfac  13152  prdsxmetlem  17984  nrmmetd  18149  ngptgp  18204  nlmvscnlem2  18248  nlmvscnlem1  18249  nmotri  18300  nghmplusg  18301  blcvx  18356  iccntr  18378  icccmplem2  18380  reconnlem2  18384  metdcnlem  18393  metnrmlem3  18417  cnllycmp  18507  lebnumii  18517  tchcphlem1  18718  ipcnlem2  18724  ipcnlem1  18725  minveclem2  18843  minveclem3b  18845  minveclem4  18849  ivthlem2  18865  ovolgelb  18892  ovollb2lem  18900  ovolunlem1a  18908  ovolunlem1  18909  ovolfiniun  18913  ovoliunlem1  18914  ovoliunlem2  18915  ovolshftlem1  18921  ovolscalem1  18925  ovolicopnf  18936  ismbl2  18939  nulmbl2  18947  unmbl  18948  voliunlem2  18961  ioombl1lem2  18969  ioombl1lem4  18971  ioombl1  18972  ioorcl2  18980  uniioombllem1  18989  uniioombllem3  18993  uniioombllem4  18994  uniioombllem5  18995  uniioombl  18997  opnmbllem  19009  volcn  19014  itg1addlem4  19107  mbfi1fseqlem4  19126  mbfi1fseqlem6  19128  itg2splitlem  19156  itg2split  19157  itg2monolem3  19160  itg2addlem  19166  ibladdlem  19227  itgaddlem1  19230  itgaddlem2  19231  iblabslem  19235  iblabs  19236  dvferm1lem  19384  dvferm2lem  19386  dvlip2  19395  lhop1lem  19413  lhop1  19414  lhop  19416  dvcnvrelem1  19417  dvcnvrelem2  19418  dvcnvre  19419  dvcvx  19420  dvfsumlem3  19428  dvfsumlem4  19429  dvfsum2  19434  ftc1lem4  19439  coemullem  19684  ulmbdd  19828  ulmcn  19829  ulmdvlem1  19830  radcnvle  19849  pserdvlem1  19856  pserdv  19858  abelthlem7  19867  pilem2  19881  pilem3  19882  cosordlem  19946  logccv  20063  cxpaddle  20145  ang180lem2  20161  atanlogaddlem  20262  atans2  20280  cxp2limlem  20323  scvxcvx  20333  jensenlem2  20335  amgmlem  20337  harmonicbnd4  20357  fsumharmonic  20358  ftalem5  20367  efnnfsumcl  20393  efchtdvds  20450  chtublem  20503  chtub  20504  logfaclbnd  20514  perfectlem2  20522  bcmono  20569  bposlem7  20582  bposlem9  20584  lgsdirprm  20621  2sqlem8  20664  vmadivsumb  20685  rplogsumlem1  20686  dchrisumlem2  20692  dchrvmasumlem2  20700  dchrvmasumiflem1  20703  dchrisum0re  20715  dchrisum0lem1b  20717  mulog2sumlem1  20736  mulog2sumlem2  20737  logsqvma2  20745  log2sumbnd  20746  selberglem2  20748  selbergb  20751  selberg2b  20754  chpdifbndlem1  20755  chpdifbndlem2  20756  selberg3lem2  20760  selberg3  20761  selberg4lem1  20762  selberg4  20763  pntrsumbnd2  20769  selberg3r  20771  selberg34r  20773  pntsf  20775  pntrlog2bndlem1  20779  pntrlog2bndlem2  20780  pntrlog2bndlem4  20782  pntrlog2bndlem5  20783  pntrlog2bndlem6  20785  pntrlog2bnd  20786  pntpbnd1a  20787  pntpbnd2  20789  pntibndlem2a  20792  pntibndlem2  20793  pntibndlem3  20794  pntlemg  20800  pntlemr  20804  pntlemk  20808  pntlemo  20809  pntlem3  20811  abvcxp  20817  padicabv  20832  ostth2lem2  20836  ostth3  20840  vacn  21322  smcnlem  21325  ubthlem2  21505  minvecolem2  21509  minvecolem3  21510  minvecolem4  21514  minvecolem5  21515  nmoptrii  22729  hstle  22865  staddi  22881  stadd3i  22883  lt2addrd  23265  sqsscirc1  23375  cnre2csqlem  23377  tpr2rico  23379  metustexhalf  23498  dya2iocress  23798  dya2iocbrsiga  23799  dya2icobrsiga  23800  dya2icoseg  23801  dya2iocucvr  23808  sxbrsigalem2  23810  ballotlemfc0  23924  ballotlemfcc  23925  ballotlemsgt1  23942  ballotlemsel1i  23944  rescon  24061  faclim  24484  brbtwn2  24919  axsegconlem8  24938  axsegconlem10  24940  axpaschlem  24954  axpasch  24955  axeuclidlem  24976  axcontlem2  24979  supaddc  25309  supadd  25310  itg2addnclem  25317  itg2addnc  25319  itg2gt0cn  25320  ibladdnclem  25321  itgaddnclem1  25323  itgaddnclem2  25324  iblabsnclem  25328  iblabsnc  25329  iblmulc2nc  25330  ftc1cnnclem  25338  areacirclem6  25347  csbrn  25611  trirn  25612  mettrifi  25622  isbnd3  25656  ssbnd  25660  cntotbnd  25668  heibor1lem  25681  bfplem2  25695  rrnequiv  25707  iccbnd  25712  pellexlem2  26063  pell1qrge1  26103  pell14qrgapw  26109  pellqrexplicit  26110  pellqrex  26112  pellfundge  26115  pellfundgt1  26116  rmspecfund  26142  rmxycomplete  26150  ltrmynn0  26183  jm2.24nn  26194  jm2.24  26198  fzmaxdif  26216  jm2.26lem3  26242  jm3.1lem2  26259  climinf  26880  climsuselem1  26881  stoweidlem20  26917  stoweidlem21  26918  wallispilem3  26964  wallispilem4  26965  wallispilem5  26966  wallispi  26967  wallispi2lem1  26968  wallispi2lem2  26969  stirlinglem1  26971  stirlinglem3  26973  stirlinglem5  26975  stirlinglem6  26976  stirlinglem7  26977  stirlinglem10  26980  stirlinglem11  26981  stirlinglem12  26982
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 8843
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator