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

Theorem readdcld 9041
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 8999 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717  (class class class)co 6013   RRcr 8915    + caddc 8919
This theorem is referenced by:  ltadd2  9103  readdcan  9165  addid1  9171  leadd1  9421  le2add  9435  lesub2  9448  cju  9921  rpnnen1lem5  10529  xralrple  10716  xov1plusxeqvd  10966  fladdz  11147  flhalf  11151  fldiv  11161  discr1  11435  discr  11436  remim  11842  remullem  11853  sqrlem7  11974  absrele  12033  abstri  12054  abs3lem  12062  amgm2  12093  mulcn2  12309  o1add  12327  o1sub  12329  lo1add  12340  caucvgrlem  12386  iseraltlem2  12396  iseraltlem3  12397  fsumabs  12500  o1fsum  12512  climcndslem2  12550  tanhlt1  12681  eirrlem  12723  ruclem1  12750  ruclem2  12751  ruclem3  12752  bitscmp  12870  sadcaddlem  12889  sadasslem  12902  smuval2  12914  prmreclem4  13207  4sqlem5  13230  4sqlem6  13231  4sqlem12  13244  4sqlem15  13247  4sqlem16  13248  2expltfac  13346  prdsxmetlem  18299  metustexhalf  18469  nrmmetd  18486  ngptgp  18541  nlmvscnlem2  18585  nlmvscnlem1  18586  nmotri  18637  nghmplusg  18638  blcvx  18693  iccntr  18716  icccmplem2  18718  reconnlem2  18722  metdcnlem  18731  metnrmlem3  18755  cnllycmp  18845  lebnumii  18855  tchcphlem1  19056  ipcnlem2  19062  ipcnlem1  19063  minveclem2  19187  minveclem3b  19189  minveclem4  19193  ivthlem2  19209  ovolgelb  19236  ovollb2lem  19244  ovolunlem1a  19252  ovolunlem1  19253  ovolfiniun  19257  ovoliunlem1  19258  ovoliunlem2  19259  ovolshftlem1  19265  ovolscalem1  19269  ovolicopnf  19280  ismbl2  19283  nulmbl2  19291  unmbl  19292  voliunlem2  19305  ioombl1lem2  19313  ioombl1lem4  19315  ioombl1  19316  ioorcl2  19324  uniioombllem1  19333  uniioombllem3  19337  uniioombllem4  19338  uniioombllem5  19339  uniioombl  19341  opnmbllem  19353  volcn  19358  itg1addlem4  19451  mbfi1fseqlem4  19470  mbfi1fseqlem6  19472  itg2splitlem  19500  itg2split  19501  itg2monolem3  19504  itg2addlem  19510  ibladdlem  19571  itgaddlem1  19574  itgaddlem2  19575  iblabslem  19579  iblabs  19580  dvferm1lem  19728  dvferm2lem  19730  dvlip2  19739  lhop1lem  19757  lhop1  19758  lhop  19760  dvcnvrelem1  19761  dvcnvrelem2  19762  dvcnvre  19763  dvcvx  19764  dvfsumlem3  19772  dvfsumlem4  19773  dvfsum2  19778  ftc1lem4  19783  coemullem  20028  ulmbdd  20174  ulmcn  20175  ulmdvlem1  20176  radcnvle  20196  pserdvlem1  20203  pserdv  20205  abelthlem7  20214  pilem2  20228  pilem3  20229  cosordlem  20293  abslogle  20373  logccv  20414  cxpaddle  20496  ang180lem2  20512  atanlogaddlem  20613  atans2  20631  cxp2limlem  20674  scvxcvx  20684  jensenlem2  20686  amgmlem  20688  logdiflbnd  20693  harmonicbnd4  20709  fsumharmonic  20710  ftalem5  20719  efnnfsumcl  20745  efchtdvds  20802  chtublem  20855  chtub  20856  logfaclbnd  20866  perfectlem2  20874  bcmono  20921  bposlem7  20934  bposlem9  20936  lgsdirprm  20973  2sqlem8  21016  vmadivsumb  21037  rplogsumlem1  21038  dchrisumlem2  21044  dchrvmasumlem2  21052  dchrvmasumiflem1  21055  dchrisum0re  21067  dchrisum0lem1b  21069  mulog2sumlem1  21088  mulog2sumlem2  21089  logsqvma2  21097  log2sumbnd  21098  selberglem2  21100  selbergb  21103  selberg2b  21106  chpdifbndlem1  21107  chpdifbndlem2  21108  selberg3lem2  21112  selberg3  21113  selberg4lem1  21114  selberg4  21115  pntrsumbnd2  21121  selberg3r  21123  selberg34r  21125  pntsf  21127  pntrlog2bndlem1  21131  pntrlog2bndlem2  21132  pntrlog2bndlem4  21134  pntrlog2bndlem5  21135  pntrlog2bndlem6  21137  pntrlog2bnd  21138  pntpbnd1a  21139  pntpbnd2  21141  pntibndlem2a  21144  pntibndlem2  21145  pntibndlem3  21146  pntlemg  21152  pntlemr  21156  pntlemk  21160  pntlemo  21161  pntlem3  21163  abvcxp  21169  padicabv  21184  ostth2lem2  21188  ostth3  21192  vacn  22031  smcnlem  22034  ubthlem2  22214  minvecolem2  22218  minvecolem3  22219  minvecolem4  22223  minvecolem5  22224  nmoptrii  23438  hstle  23574  staddi  23590  stadd3i  23592  lt2addrd  23949  fsumrp0cl  24039  sqsscirc1  24103  cnre2csqlem  24105  tpr2rico  24107  dya2iocress  24411  dya2iocbrsiga  24412  dya2icobrsiga  24413  dya2icoseg  24414  dya2iocucvr  24421  sxbrsigalem2  24423  ballotlemfc0  24522  ballotlemfcc  24523  ballotlemsgt1  24540  ballotlemsel1i  24542  lgamgulmlem3  24587  lgamgulmlem4  24588  lgamgulmlem5  24589  lgamgulmlem6  24590  lgambdd  24593  lgamucov  24594  regamcl  24617  rescon  24705  faclim  25116  brbtwn2  25551  axsegconlem8  25570  axsegconlem10  25572  axpaschlem  25586  axpasch  25587  axeuclidlem  25608  axcontlem2  25611  supaddc  25940  supadd  25941  itg2addnclem  25950  itg2addnc  25952  itg2gt0cn  25953  ibladdnclem  25954  itgaddnclem1  25956  itgaddnclem2  25957  iblabsnclem  25961  iblabsnc  25962  iblmulc2nc  25963  ftc1cnnclem  25971  areacirclem6  25980  csbrn  26140  trirn  26141  mettrifi  26147  isbnd3  26177  ssbnd  26181  cntotbnd  26189  heibor1lem  26202  bfplem2  26216  rrnequiv  26228  iccbnd  26233  pellexlem2  26577  pell1qrge1  26617  pell14qrgapw  26623  pellqrexplicit  26624  pellqrex  26626  pellfundge  26629  pellfundgt1  26630  rmspecfund  26656  rmxycomplete  26664  ltrmynn0  26697  jm2.24nn  26708  jm2.24  26712  fzmaxdif  26730  jm2.26lem3  26756  jm3.1lem2  26773  climinf  27393  climsuselem1  27394  stoweidlem1  27411  stoweidlem11  27421  stoweidlem13  27423  stoweidlem14  27424  stoweidlem20  27430  stoweidlem21  27431  stoweidlem26  27436  stoweidlem44  27454  stoweidlem60  27470  wallispilem3  27477  wallispilem4  27478  wallispilem5  27479  wallispi  27480  wallispi2lem1  27481  wallispi2lem2  27482  stirlinglem1  27484  stirlinglem3  27486  stirlinglem5  27488  stirlinglem6  27489  stirlinglem7  27490  stirlinglem10  27493  stirlinglem11  27494  stirlinglem12  27495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 8977
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator