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

Theorem addcl 9028
Description: Alias for ax-addcl 9006, for naming consistency with addcli 9050. Use this theorem instead of ax-addcl 9006 or axaddcl 8982. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 9006 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721  (class class class)co 6040   CCcc 8944    + caddc 8949
This theorem is referenced by:  adddir  9039  0cn  9040  addcli  9050  addcld  9063  muladd11  9192  peano2cn  9194  add4  9237  0cnALT  9251  negeu  9252  pncan  9267  2addsub  9275  addsubeq4  9276  nppcan2  9288  ppncan  9299  muladd  9422  mulsub  9432  recex  9610  muleqadd  9622  conjmul  9687  halfaddsubcl  10156  halfaddsub  10157  uzindOLD  10320  serf  11306  seradd  11320  sersub  11321  binom3  11455  bernneq  11460  revccat  11753  shftlem  11838  shftval2  11845  shftval5  11848  2shfti  11850  crre  11874  crim  11875  cjadd  11901  addcj  11908  sqabsadd  12042  absreimsq  12052  absreim  12053  abstri  12089  sqreulem  12118  sqreu  12119  addcn2  12342  o1add  12362  climadd  12380  clim2ser  12403  clim2ser2  12404  isermulc2  12406  isercolllem3  12415  summolem3  12463  summolem2a  12464  fsumcl  12482  fsummulc2  12522  fsumrelem  12541  binom  12564  isumsplit  12575  efcj  12649  ef4p  12669  tanval3  12690  efi4p  12693  sinadd  12720  cosadd  12721  tanadd  12723  addsin  12726  demoivreALT  12757  opoe  13140  pythagtriplem4  13148  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem16  13159  gzaddcl  13260  cnaddablx  15436  cnaddabl  15437  cncrng  16677  cnperf  18804  dvaddbr  19777  dvaddf  19781  dveflem  19816  plyaddcl  20092  plymulcl  20093  plysubcl  20094  coeaddlem  20120  dgrcolem1  20144  dgrcolem2  20145  quotlem  20170  quotcl2  20172  quotdgr  20173  sinperlem  20341  ptolemy  20357  tangtx  20366  sinkpi  20380  efgh  20396  efif1olem2  20398  logrnaddcl  20425  logneg  20435  logimul  20462  cxpadd  20523  binom4  20643  atanf  20673  atanneg  20700  atancj  20703  efiatan  20705  atanlogaddlem  20706  atanlogadd  20707  atanlogsublem  20708  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  cosatan  20714  cosatanne0  20715  atantan  20716  atanbndlem  20718  atans2  20724  dvatan  20728  atantayl  20730  efrlim  20761  dfef2  20762  ftalem7  20814  prmorcht  20914  bposlem9  21029  lgsquad2lem1  21095  2sqlem2  21101  wlkdvspthlem  21560  gxadd  21816  cncph  22273  hhssnv  22717  hoadddir  23260  superpos  23810  gamcvg2lem  24796  risefacval2  25279  risefaccl  25283  risefallfac  25292  risefacp1  25297  binomfallfac  25308  binomrisefac  25309  bpoly3  26008  stirlinglem5  27694  stirlinglem7  27696
This theorem was proved from axioms:  ax-addcl 9006
  Copyright terms: Public domain W3C validator