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

Theorem addcl 10003
Description: Alias for ax-addcl 9981, for naming consistency with addcli 10029. Use this theorem instead of ax-addcl 9981 or axaddcl 9957. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Proof of Theorem addcl
StepHypRef Expression
1 ax-addcl 9981 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1988  (class class class)co 6635  cc 9919   + caddc 9924
This theorem was proved from axioms:  ax-addcl 9981
This theorem is referenced by:  adddir  10016  0cn  10017  addcli  10029  addcld  10044  muladd11  10191  peano2cn  10193  muladd11r  10234  add4  10241  0cnALT  10255  negeu  10256  pncan  10272  2addsub  10280  addsubeq4  10281  nppcan2  10297  ppncan  10308  muladd  10447  mulsub  10458  recex  10644  muleqadd  10656  conjmul  10727  halfaddsubcl  11249  halfaddsub  11250  serf  12812  seradd  12826  sersub  12827  binom3  12968  bernneq  12973  lswccatn0lsw  13356  revccat  13496  2cshwcshw  13552  shftlem  13789  shftval2  13796  shftval5  13799  2shfti  13801  crre  13835  crim  13836  cjadd  13862  addcj  13869  sqabsadd  14003  absreimsq  14013  absreim  14014  abstri  14051  sqreulem  14080  sqreu  14081  addcn2  14305  o1add  14325  climadd  14343  clim2ser  14366  clim2ser2  14367  isermulc2  14369  isercolllem3  14378  summolem3  14426  summolem2a  14427  fsumcl  14445  fsummulc2  14497  fsumrelem  14520  binom  14543  isumsplit  14553  risefacval2  14722  risefaccl  14727  risefallfac  14736  risefacp1  14741  binomfallfac  14753  binomrisefac  14754  bpoly3  14770  efcj  14803  ef4p  14824  tanval3  14845  efi4p  14848  sinadd  14875  cosadd  14876  tanadd  14878  addsin  14881  demoivreALT  14912  opoe  15068  pythagtriplem4  15505  pythagtriplem12  15512  pythagtriplem14  15514  pythagtriplem16  15516  gzaddcl  15622  cnaddablx  18252  cnaddabl  18253  cncrng  19748  cnperf  22604  cnlmod  22921  cnstrcvs  22922  cncvs  22926  dvaddbr  23682  dvaddf  23686  dveflem  23723  plyaddcl  23957  plymulcl  23958  plysubcl  23959  coeaddlem  23986  dgrcolem1  24010  dgrcolem2  24011  quotlem  24036  quotcl2  24038  quotdgr  24039  sinperlem  24213  ptolemy  24229  tangtx  24238  sinkpi  24252  efif1olem2  24270  logrnaddcl  24302  logneg  24315  logimul  24341  cxpadd  24406  binom4  24558  atanf  24588  atanneg  24615  atancj  24618  efiatan  24620  atanlogaddlem  24621  atanlogadd  24622  atanlogsublem  24623  atanlogsub  24624  efiatan2  24625  2efiatan  24626  tanatan  24627  cosatan  24629  cosatanne0  24630  atantan  24631  atanbndlem  24633  atans2  24639  dvatan  24643  atantayl  24645  efrlim  24677  dfef2  24678  gamcvg2lem  24766  ftalem7  24786  prmorcht  24885  bposlem9  24998  lgsquad2lem1  25090  2sqlem2  25124  wwlksext2clwwlk  26904  cncph  27644  hhssnv  28091  hoadddir  28633  superpos  29183  knoppcnlem8  32465  cos2h  33371  tan2h  33372  ftc1anclem3  33458  ftc1anclem7  33462  ftc1anclem8  33463  ftc1anc  33464  fsumsermpt  39611  stirlinglem5  40058  stirlinglem7  40060  cnapbmcpd  41073  fmtnodvds  41221  opoeALTV  41359  mogoldbblem  41394
  Copyright terms: Public domain W3C validator