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

Theorem addcld 8870
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 8835 . 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 1696  (class class class)co 5874   CCcc 8751    + caddc 8756
This theorem is referenced by:  cnegex  9009  addcom  9014  addcomd  9030  negeu  9058  addsubass  9077  subsub2  9091  subsub4  9096  pnpcan  9102  pnncan  9104  addsub4  9106  divdir  9463  cju  9758  cnref1o  10365  xov1plusxeqvd  10796  expaddz  11162  binom3  11238  spllen  11485  crre  11615  remullem  11629  imval2  11652  cjreim2  11662  sqreulem  11859  addcn2  12083  o1add  12103  fsumadd  12227  isumadd  12246  binomlem  12303  efaddlem  12390  ef4p  12409  cosf  12421  tanval2  12429  tanval3  12430  resin4p  12434  recos4p  12435  efival  12448  sinadd  12460  cosadd  12461  tanadd  12463  sadadd2lem2  12657  sadadd2lem  12666  pythagtriplem1  12885  pythagtriplem12  12895  pythagtriplem17  12900  pcbc  12964  mul4sqlem  13016  4sqlem14  13021  vdwlem6  13049  vdwlem9  13052  mulgdirlem  14607  blcvx  18320  tchcphlem1  18681  ovollb2lem  18863  mbfadd  19032  itgcnlem  19160  itgaddlem2  19194  dvmptre  19334  dvsincos  19344  taylthlem2  19769  ptolemy  19880  tanregt0  19917  eff1olem  19926  cosargd  19978  tanarg  19986  logf1o2  20013  efopn  20021  cxpsqrlem  20065  cxpeq  20113  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  pythag  20131  ssscongptld  20138  chordthmlem  20145  chordthmlem2  20146  chordthmlem3  20147  chordthmlem4  20148  chordthmlem5  20149  quad2  20151  dcubic1lem  20155  dcubic2  20156  dcubic1  20157  dcubic  20158  mcubic  20159  cubic2  20160  cubic  20161  binom4  20162  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1cl  20166  quart1lem  20167  quart1  20168  quartlem1  20169  quartlem2  20170  quartlem3  20171  quartlem4  20172  quart  20173  asinlem3  20183  asinf  20184  asinneg  20198  efiasin  20200  asinsinlem  20203  asinsin  20204  asinbnd  20211  ftalem7  20332  basellem3  20336  bposlem9  20547  lgsquad2lem1  20613  dchrvmasumiflem2  20667  mulogsumlem  20696  mulog2sumlem1  20699  mulog2sumlem2  20700  mulog2sumlem3  20701  selberglem1  20710  selberg2  20716  selberg3lem1  20722  selbergr  20733  selberg3r  20734  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntrlog2bnd  20749  4ipval2  21297  4ipval3  21301  dipcj  21306  golem1  22867  ballotlemsima  23090  lt2addrd  23264  cnre2csqima  23310  faclimlem3  24119  faclimlem6  24122  brbtwn2  24605  colinearalglem1  24606  colinearalglem2  24607  axeuclidlem  24662  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  bpoly4  24866  itg2addnc  25005  itgaddnclem2  25010  itgaddnc  25011  dvreasin  25026  areacirclem2  25028  areacirclem5  25032  areacirc  25034  mslb1  25710  2wsms  25711  claddrv  25750  addassv  25759  csbrn  26565  pellexlem2  27018  pellexlem6  27022  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell14qrdich  27057  rmxyneg  27108  rmxyadd  27109  jm2.19lem4  27188  jm2.26lem3  27197  clim1fr1  27830  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem10  27935  stirlinglem11  27936  stirlinglem12  27937  stirlinglem13  27938  stirlinglem15  27940  sigaraf  27946  sigaras  27948  sinhpcosh  28464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addcl 8813
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator