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

Theorem addcld 8854
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 8819 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740
This theorem is referenced by:  cnegex  8993  addcom  8998  addcomd  9014  negeu  9042  addsubass  9061  subsub2  9075  subsub4  9080  pnpcan  9086  pnncan  9088  addsub4  9090  divdir  9447  cju  9742  cnref1o  10349  xov1plusxeqvd  10780  expaddz  11146  binom3  11222  spllen  11469  crre  11599  remullem  11613  imval2  11636  cjreim2  11646  sqreulem  11843  addcn2  12067  o1add  12087  fsumadd  12211  isumadd  12230  binomlem  12287  efaddlem  12374  ef4p  12393  cosf  12405  tanval2  12413  tanval3  12414  resin4p  12418  recos4p  12419  efival  12432  sinadd  12444  cosadd  12445  tanadd  12447  sadadd2lem2  12641  sadadd2lem  12650  pythagtriplem1  12869  pythagtriplem12  12879  pythagtriplem17  12884  pcbc  12948  mul4sqlem  13000  4sqlem14  13005  vdwlem6  13033  vdwlem9  13036  mulgdirlem  14591  blcvx  18304  tchcphlem1  18665  ovollb2lem  18847  mbfadd  19016  itgcnlem  19144  itgaddlem2  19178  dvmptre  19318  dvsincos  19328  taylthlem2  19753  ptolemy  19864  tanregt0  19901  eff1olem  19910  cosargd  19962  tanarg  19970  logf1o2  19997  efopn  20005  cxpsqrlem  20049  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  pythag  20115  ssscongptld  20122  chordthmlem  20129  chordthmlem2  20130  chordthmlem3  20131  chordthmlem4  20132  chordthmlem5  20133  quad2  20135  dcubic1lem  20139  dcubic2  20140  dcubic1  20141  dcubic  20142  mcubic  20143  cubic2  20144  cubic  20145  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1cl  20150  quart1lem  20151  quart1  20152  quartlem1  20153  quartlem2  20154  quartlem3  20155  quartlem4  20156  quart  20157  asinlem3  20167  asinf  20168  asinneg  20182  efiasin  20184  asinsinlem  20187  asinsin  20188  asinbnd  20195  ftalem7  20316  basellem3  20320  bposlem9  20531  lgsquad2lem1  20597  dchrvmasumiflem2  20651  mulogsumlem  20680  mulog2sumlem1  20683  mulog2sumlem2  20684  mulog2sumlem3  20685  selberglem1  20694  selberg2  20700  selberg3lem1  20706  selbergr  20717  selberg3r  20718  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  4ipval2  21281  4ipval3  21285  dipcj  21290  golem1  22851  ballotlemsima  23074  lt2addrd  23249  cnre2csqima  23295  brbtwn2  24533  colinearalglem1  24534  colinearalglem2  24535  axeuclidlem  24590  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  bpoly4  24794  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  areacirc  24931  mslb1  25607  2wsms  25608  claddrv  25647  addassv  25656  csbrn  26462  pellexlem2  26915  pellexlem6  26919  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrdich  26954  rmxyneg  27005  rmxyadd  27006  jm2.19lem4  27085  jm2.26lem3  27094  clim1fr1  27727  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem15  27837  sigaraf  27843  sigaras  27845  sinhpcosh  28210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 8797
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator