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

Theorem readdcld 8864
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 8822 . 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 1686  (class class class)co 5860   RRcr 8738    + caddc 8742
This theorem is referenced by:  ltadd2  8926  readdcan  8988  addid1  8994  leadd1  9244  le2add  9258  lesub2  9271  cju  9744  rpnnen1lem5  10348  xralrple  10534  xov1plusxeqvd  10782  fladdz  10952  flhalf  10956  fldiv  10966  discr1  11239  discr  11240  remim  11604  remullem  11615  sqrlem7  11736  absrele  11795  abstri  11816  abs3lem  11824  amgm2  11855  mulcn2  12071  o1add  12089  o1sub  12091  lo1add  12102  caucvgrlem  12147  iseraltlem2  12157  iseraltlem3  12158  fsumabs  12261  o1fsum  12273  climcndslem2  12311  tanhlt1  12442  eirrlem  12484  ruclem1  12511  ruclem2  12512  ruclem3  12513  bitscmp  12631  sadcaddlem  12650  sadasslem  12663  smuval2  12675  prmreclem4  12968  4sqlem5  12991  4sqlem6  12992  4sqlem12  13005  4sqlem15  13008  4sqlem16  13009  2expltfac  13107  prdsxmetlem  17934  nrmmetd  18099  ngptgp  18154  nlmvscnlem2  18198  nlmvscnlem1  18199  nmotri  18250  nghmplusg  18251  blcvx  18306  iccntr  18328  icccmplem2  18330  reconnlem2  18334  metdcnlem  18343  metnrmlem3  18367  cnllycmp  18456  lebnumii  18466  tchcphlem1  18667  ipcnlem2  18673  ipcnlem1  18674  minveclem2  18792  minveclem3b  18794  minveclem4  18798  ivthlem2  18814  ovolgelb  18841  ovollb2lem  18849  ovolunlem1a  18857  ovolunlem1  18858  ovolfiniun  18862  ovoliunlem1  18863  ovoliunlem2  18864  ovolshftlem1  18870  ovolscalem1  18874  ovolicopnf  18885  ismbl2  18888  nulmbl2  18896  unmbl  18897  voliunlem2  18910  ioombl1lem2  18918  ioombl1lem4  18920  ioombl1  18921  ioorcl2  18929  uniioombllem1  18938  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  uniioombl  18946  opnmbllem  18958  volcn  18963  itg1addlem4  19056  mbfi1fseqlem4  19075  mbfi1fseqlem6  19077  itg2splitlem  19105  itg2split  19106  itg2monolem3  19109  itg2addlem  19115  ibladdlem  19176  itgaddlem1  19179  itgaddlem2  19180  iblabslem  19184  iblabs  19185  dvferm1lem  19333  dvferm2lem  19335  dvlip2  19344  lhop1lem  19362  lhop1  19363  lhop  19365  dvcnvrelem1  19366  dvcnvrelem2  19367  dvcnvre  19368  dvcvx  19369  dvfsumlem3  19377  dvfsumlem4  19378  dvfsum2  19383  ftc1lem4  19388  coemullem  19633  ulmbdd  19777  ulmcn  19778  ulmdvlem1  19779  radcnvle  19798  pserdvlem1  19805  pserdv  19807  abelthlem7  19816  pilem2  19830  pilem3  19831  cosordlem  19895  logccv  20012  cxpaddle  20094  ang180lem2  20110  atanlogaddlem  20211  atans2  20229  cxp2limlem  20272  scvxcvx  20282  jensenlem2  20284  amgmlem  20286  harmonicbnd4  20306  fsumharmonic  20307  ftalem5  20316  efnnfsumcl  20342  efchtdvds  20399  chtublem  20452  chtub  20453  logfaclbnd  20463  perfectlem2  20471  bcmono  20518  bposlem7  20531  bposlem9  20533  lgsdirprm  20570  2sqlem8  20613  vmadivsumb  20634  rplogsumlem1  20635  dchrisumlem2  20641  dchrvmasumlem2  20649  dchrvmasumiflem1  20652  dchrisum0re  20664  dchrisum0lem1b  20666  mulog2sumlem1  20685  mulog2sumlem2  20686  logsqvma2  20694  log2sumbnd  20695  selberglem2  20697  selbergb  20700  selberg2b  20703  chpdifbndlem1  20704  chpdifbndlem2  20705  selberg3lem2  20709  selberg3  20710  selberg4lem1  20711  selberg4  20712  pntrsumbnd2  20718  selberg3r  20720  selberg34r  20722  pntsf  20724  pntrlog2bndlem1  20728  pntrlog2bndlem2  20729  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntrlog2bndlem6  20734  pntrlog2bnd  20735  pntpbnd1a  20736  pntpbnd2  20738  pntibndlem2a  20741  pntibndlem2  20742  pntibndlem3  20743  pntlemg  20749  pntlemr  20753  pntlemk  20757  pntlemo  20758  pntlem3  20760  abvcxp  20766  padicabv  20781  ostth2lem2  20785  ostth3  20789  vacn  21269  smcnlem  21272  ubthlem2  21452  minvecolem2  21456  minvecolem3  21457  minvecolem4  21461  minvecolem5  21462  nmoptrii  22676  hstle  22812  staddi  22828  stadd3i  22830  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemsgt1  23071  ballotlemsel1i  23073  lt2addrd  23251  sqsscirc1  23294  cnre2csqlem  23296  cnre2csqima  23297  tpr2rico  23298  dya2iocress  23579  dya2iocbrsiga  23580  dya2iocseg  23581  rescon  23779  brbtwn2  24535  axsegconlem8  24554  axsegconlem10  24556  axpaschlem  24570  axpasch  24571  axeuclidlem  24592  axcontlem2  24595  supaddc  24927  supadd  24928  itg2addnclem  24933  itg2addnc  24935  areacirclem6  24941  altretop  25611  mslb1  25618  csbrn  26473  trirn  26474  mettrifi  26484  isbnd3  26519  ssbnd  26523  cntotbnd  26531  heibor1lem  26544  bfplem2  26558  rrnequiv  26570  iccbnd  26575  pellexlem2  26926  pell1qrge1  26966  pell14qrgapw  26972  pellqrexplicit  26973  pellqrex  26975  pellfundge  26978  pellfundgt1  26979  rmspecfund  27005  rmxycomplete  27013  ltrmynn0  27046  jm2.24nn  27057  jm2.24  27061  fzmaxdif  27079  jm2.26lem3  27105  jm3.1lem2  27122  climinf  27743  climsuselem1  27744  stoweidlem20  27780  stoweidlem21  27781  wallispilem3  27827  wallispilem4  27828  wallispilem5  27829  wallispi  27830  wallispi2lem1  27831  wallispi2lem2  27832  stirlinglem1  27834  stirlinglem3  27836  stirlinglem5  27838  stirlinglem6  27839  stirlinglem7  27840  stirlinglem10  27843  stirlinglem11  27844  stirlinglem12  27845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 8800
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator