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

Theorem readdcld 9104
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 9062 . 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 1725  (class class class)co 6072   RRcr 8978    + caddc 8982
This theorem is referenced by:  ltadd2  9166  readdcan  9229  addid1  9235  leadd1  9485  le2add  9499  lesub2  9512  cju  9985  rpnnen1lem5  10593  xralrple  10780  xov1plusxeqvd  11030  fladdz  11215  flhalf  11219  fldiv  11229  discr1  11503  discr  11504  remim  11910  remullem  11921  sqrlem7  12042  absrele  12101  abstri  12122  abs3lem  12130  amgm2  12161  mulcn2  12377  o1add  12395  o1sub  12397  lo1add  12408  caucvgrlem  12454  iseraltlem2  12464  iseraltlem3  12465  fsumabs  12568  o1fsum  12580  climcndslem2  12618  tanhlt1  12749  eirrlem  12791  ruclem1  12818  ruclem2  12819  ruclem3  12820  bitscmp  12938  sadcaddlem  12957  sadasslem  12970  smuval2  12982  prmreclem4  13275  4sqlem5  13298  4sqlem6  13299  4sqlem12  13312  4sqlem15  13315  4sqlem16  13316  2expltfac  13414  prdsxmetlem  18386  xblss2ps  18419  metustexhalfOLD  18581  metustexhalf  18582  nrmmetd  18610  ngptgp  18665  nlmvscnlem2  18709  nlmvscnlem1  18710  nmotri  18761  nghmplusg  18762  blcvx  18817  iccntr  18840  icccmplem2  18842  reconnlem2  18846  metdcnlem  18855  metnrmlem3  18879  cnllycmp  18969  lebnumii  18979  tchcphlem1  19180  ipcnlem2  19186  ipcnlem1  19187  minveclem2  19315  minveclem3b  19317  minveclem4  19321  ivthlem2  19337  ovolgelb  19364  ovollb2lem  19372  ovolunlem1a  19380  ovolunlem1  19381  ovolfiniun  19385  ovoliunlem1  19386  ovoliunlem2  19387  ovolshftlem1  19393  ovolscalem1  19397  ovolicopnf  19408  ismbl2  19411  nulmbl2  19419  unmbl  19420  voliunlem2  19433  ioombl1lem2  19441  ioombl1lem4  19443  ioombl1  19444  ioorcl2  19452  uniioombllem1  19461  uniioombllem3  19465  uniioombllem4  19466  uniioombllem5  19467  uniioombl  19469  opnmbllem  19481  volcn  19486  itg1addlem4  19579  mbfi1fseqlem4  19598  mbfi1fseqlem6  19600  itg2splitlem  19628  itg2split  19629  itg2monolem3  19632  itg2addlem  19638  ibladdlem  19699  itgaddlem1  19702  itgaddlem2  19703  iblabslem  19707  iblabs  19708  dvferm1lem  19856  dvferm2lem  19858  dvlip2  19867  lhop1lem  19885  lhop1  19886  lhop  19888  dvcnvrelem1  19889  dvcnvrelem2  19890  dvcnvre  19891  dvcvx  19892  dvfsumlem3  19900  dvfsumlem4  19901  dvfsum2  19906  ftc1lem4  19911  coemullem  20156  ulmbdd  20302  ulmcn  20303  ulmdvlem1  20304  radcnvle  20324  pserdvlem1  20331  pserdv  20333  abelthlem7  20342  pilem2  20356  pilem3  20357  cosordlem  20421  abslogle  20501  logccv  20542  cxpaddle  20624  ang180lem2  20640  atanlogaddlem  20741  atans2  20759  cxp2limlem  20802  scvxcvx  20812  jensenlem2  20814  amgmlem  20816  logdiflbnd  20821  harmonicbnd4  20837  fsumharmonic  20838  ftalem5  20847  efnnfsumcl  20873  efchtdvds  20930  chtublem  20983  chtub  20984  logfaclbnd  20994  perfectlem2  21002  bcmono  21049  bposlem7  21062  bposlem9  21064  lgsdirprm  21101  2sqlem8  21144  vmadivsumb  21165  rplogsumlem1  21166  dchrisumlem2  21172  dchrvmasumlem2  21180  dchrvmasumiflem1  21183  dchrisum0re  21195  dchrisum0lem1b  21197  mulog2sumlem1  21216  mulog2sumlem2  21217  logsqvma2  21225  log2sumbnd  21226  selberglem2  21228  selbergb  21231  selberg2b  21234  chpdifbndlem1  21235  chpdifbndlem2  21236  selberg3lem2  21240  selberg3  21241  selberg4lem1  21242  selberg4  21243  pntrsumbnd2  21249  selberg3r  21251  selberg34r  21253  pntsf  21255  pntrlog2bndlem1  21259  pntrlog2bndlem2  21260  pntrlog2bndlem4  21262  pntrlog2bndlem5  21263  pntrlog2bndlem6  21265  pntrlog2bnd  21266  pntpbnd1a  21267  pntpbnd2  21269  pntibndlem2a  21272  pntibndlem2  21273  pntibndlem3  21274  pntlemg  21280  pntlemr  21284  pntlemk  21288  pntlemo  21289  pntlem3  21291  abvcxp  21297  padicabv  21312  ostth2lem2  21316  ostth3  21320  vacn  22178  smcnlem  22181  ubthlem2  22361  minvecolem2  22365  minvecolem3  22366  minvecolem4  22370  minvecolem5  22371  nmoptrii  23585  hstle  23721  staddi  23737  stadd3i  23739  lt2addrd  24103  fsumrp0cl  24205  sqsscirc1  24294  cnre2csqlem  24296  tpr2rico  24298  dya2iocress  24612  dya2iocbrsiga  24613  dya2icobrsiga  24614  dya2icoseg  24615  dya2iocucvr  24622  sxbrsigalem2  24624  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemsgt1  24756  ballotlemsel1i  24758  lgamgulmlem3  24803  lgamgulmlem4  24804  lgamgulmlem5  24805  lgamgulmlem6  24806  lgambdd  24809  lgamucov  24810  regamcl  24833  rescon  24921  faclim  25354  brbtwn2  25792  axsegconlem8  25811  axsegconlem10  25813  axpaschlem  25827  axpasch  25828  axeuclidlem  25849  axcontlem2  25852  supaddc  26184  supadd  26185  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  mbfposadd  26200  itg2addnclem  26202  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  ibladdnclem  26207  itgaddnclem1  26209  itgaddnclem2  26210  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  ftc1cnnclem  26224  areacirclem6  26233  csbrn  26393  trirn  26394  mettrifi  26400  isbnd3  26430  ssbnd  26434  cntotbnd  26442  heibor1lem  26455  bfplem2  26469  rrnequiv  26481  iccbnd  26486  pellexlem2  26830  pell1qrge1  26870  pell14qrgapw  26876  pellqrexplicit  26877  pellqrex  26879  pellfundge  26882  pellfundgt1  26883  rmspecfund  26909  rmxycomplete  26917  ltrmynn0  26950  jm2.24nn  26961  jm2.24  26965  fzmaxdif  26983  jm2.26lem3  27009  jm3.1lem2  27026  climinf  27646  climsuselem1  27647  stoweidlem1  27664  stoweidlem11  27674  stoweidlem13  27676  stoweidlem14  27677  stoweidlem20  27683  stoweidlem21  27684  stoweidlem26  27689  stoweidlem44  27707  stoweidlem60  27723  wallispilem3  27730  wallispilem4  27731  wallispilem5  27732  wallispi  27733  wallispi2lem1  27734  wallispi2lem2  27735  stirlinglem1  27737  stirlinglem3  27739  stirlinglem5  27741  stirlinglem6  27742  stirlinglem7  27743  stirlinglem10  27746  stirlinglem11  27747  stirlinglem12  27748  shwrdssizelem4a  28169
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addrcl 9040
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator