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

Theorem addcld 9107
Description: Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
Assertion
Ref Expression
addcld  |-  ( ph  ->  ( A  +  B
)  e.  CC )

Proof of Theorem addcld
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addcl 9072 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725  (class class class)co 6081   CCcc 8988    + caddc 8993
This theorem is referenced by:  cnegex  9247  addcom  9252  addcomd  9268  negeu  9296  addsubass  9315  subsub2  9329  subsub4  9334  pnpcan  9340  pnncan  9342  addsub4  9344  divdir  9701  cju  9996  cnref1o  10607  xov1plusxeqvd  11041  expaddz  11424  binom3  11500  spllen  11783  crre  11919  remullem  11933  imval2  11956  cjreim2  11966  sqreulem  12163  addcn2  12387  o1add  12407  fsumadd  12532  isumadd  12551  binomlem  12608  efaddlem  12695  ef4p  12714  cosf  12726  tanval2  12734  tanval3  12735  resin4p  12739  recos4p  12740  efival  12753  sinadd  12765  cosadd  12766  tanadd  12768  sadadd2lem2  12962  sadadd2lem  12971  pythagtriplem1  13190  pythagtriplem12  13200  pythagtriplem17  13205  pcbc  13269  mul4sqlem  13321  4sqlem14  13326  vdwlem6  13354  vdwlem9  13357  mulgdirlem  14914  blcvx  18829  tchcphlem1  19192  ovollb2lem  19384  mbfadd  19553  itgcnlem  19681  itgaddlem2  19715  dvmptre  19855  dvsincos  19865  taylthlem2  20290  ptolemy  20404  tanregt0  20441  eff1olem  20450  cosargd  20503  tanarg  20514  logf1o2  20541  efopn  20549  cxpsqrlem  20593  cxpeq  20641  ang180lem1  20651  ang180lem2  20652  ang180lem3  20653  ang180lem4  20654  pythag  20659  ssscongptld  20666  chordthmlem  20673  chordthmlem2  20674  chordthmlem3  20675  chordthmlem4  20676  chordthmlem5  20677  quad2  20679  dcubic1lem  20683  dcubic2  20684  dcubic1  20685  dcubic  20686  mcubic  20687  cubic2  20688  cubic  20689  binom4  20690  dquartlem1  20691  dquartlem2  20692  dquart  20693  quart1cl  20694  quart1lem  20695  quart1  20696  quartlem1  20697  quartlem2  20698  quartlem3  20699  quartlem4  20700  quart  20701  asinlem3  20711  asinf  20712  asinneg  20726  efiasin  20728  asinsinlem  20731  asinsin  20732  asinbnd  20739  atanlogaddlem  20753  ftalem7  20861  basellem3  20865  bposlem9  21076  lgsquad2lem1  21142  dchrvmasumiflem2  21196  mulogsumlem  21225  mulog2sumlem1  21228  mulog2sumlem2  21229  mulog2sumlem3  21230  selberglem1  21239  selberg2  21245  selberg3lem1  21251  selbergr  21262  selberg3r  21263  pntrlog2bndlem1  21271  pntrlog2bndlem2  21272  pntrlog2bndlem5  21275  pntrlog2bndlem6  21277  pntrlog2bnd  21278  4ipval2  22204  4ipval3  22208  dipcj  22213  golem1  23774  lt2addrd  24115  cnre2csqima  24309  ballotlemsima  24773  dmgmaddnn0  24811  dmgmdivn0  24812  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem4  24816  lgamgulmlem5  24817  lgamgulmlem6  24818  lgamgulm2  24820  lgambdd  24821  lgamucov  24822  lgamcvg2  24839  gamcvg  24840  gamcvg2lem  24843  pnpncand  25207  iprodgam  25319  binomfallfaclem2  25356  brbtwn2  25844  colinearalglem1  25845  colinearalglem2  25846  axeuclidlem  25901  axcontlem2  25904  axcontlem7  25909  axcontlem8  25910  bpoly4  26105  fsumcube  26106  itg2addnclem3  26258  itgaddnclem2  26264  itgaddnc  26265  ftc1anclem6  26285  ftc1anclem8  26287  dvreasin  26290  areacirclem1  26292  areacirclem4  26295  areacirc  26297  csbrn  26456  pellexlem2  26893  pellexlem6  26897  pell1234qrreccl  26917  pell1234qrmulcl  26918  pell14qrdich  26932  rmxyneg  26983  rmxyadd  26984  jm2.19lem4  27063  jm2.26lem3  27072  clim1fr1  27703  stoweidlem1  27726  stoweidlem11  27736  stoweidlem13  27738  wallispilem4  27793  wallispilem5  27794  wallispi  27795  wallispi2lem1  27796  wallispi2lem2  27797  wallispi2  27798  stirlinglem1  27799  stirlinglem3  27801  stirlinglem4  27802  stirlinglem5  27803  stirlinglem6  27804  stirlinglem7  27805  stirlinglem10  27808  stirlinglem11  27809  stirlinglem12  27810  stirlinglem13  27811  stirlinglem15  27813  sigaraf  27819  sigaras  27821  cshwidxm  28246  sinhpcosh  28483
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 9050
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator