Theorem mulcl 9362

Description: Alias for ax-mulcl 9340, for naming consistency with mulcli 9387. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulcl	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 9340	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1761  (class class class)co 6090   CCcc 9276   x. cmul 9283

This theorem was proved from axioms:  ax-mulcl 9340

This theorem is referenced by:  0cn  9374  mulid1  9379  mulcli  9387  mulcld  9402  mul31  9533  mul4  9534  mul02  9543  cnegex2  9547  muladd  9773  subdi  9774  submul2  9781  mulsub  9783  recextlem1  9962  recex  9964  muleqadd  9976  mulnzcnopr  9978  mulcan1g  9985  divass  10008  divmuldiv  10027  divmuleq  10032  divadddiv  10042  conjmul  10044  cju  10314  zneo  10720  cnref1o  10982  modcyc2  11740  modaddmulmod  11761  expcl  11879  expclzlem  11885  mulexp  11899  sqcl  11924  subsq  11969  subsq2  11970  binom2sub  11979  binom3  11981  zesq  11983  bernneq  11986  bernneq2  11987  bcval5  12090  reim  12594  imcl  12596  crre  12599  crim  12600  remim  12602  mulre  12606  cjreb  12608  recj  12609  reneg  12610  readd  12611  remullem  12613  remul2  12615  imcj  12617  imneg  12618  imadd  12619  immul2  12622  cjadd  12626  ipcnval  12628  cjmulrcl  12629  cjneg  12632  imval2  12636  cjreim  12645  rennim  12724  cnpart  12725  sqrneg  12753  sqabsadd  12767  sqabssub  12768  absreimsq  12777  absreim  12778  absmul  12779  sqreulem  12843  sqreu  12844  mulcn2  13069  o1mul  13088  climmul  13106  iseraltlem2  13156  efexp  13381  sinf  13404  cosf  13405  tanval2  13413  tanval3  13414  resinval  13415  recosval  13416  efi4p  13417  resin4p  13418  recos4p  13419  resincl  13420  recoscl  13421  sinneg  13426  cosneg  13427  efival  13432  efmival  13433  sinhval  13434  coshval  13435  retanhcl  13439  tanhlt1  13440  tanhbnd  13441  efeul  13442  sinadd  13444  cosadd  13445  sinsub  13448  cossub  13449  subsin  13451  sinmul  13452  cosmul  13453  addcos  13454  subcos  13455  cos2tsin  13459  ef01bndlem  13464  sin01bnd  13465  cos01bnd  13466  absef  13477  absefib  13478  efieq1re  13479  demoivre  13480  demoivreALT  13481  dvdscmulr  13557  dvdsmulcr  13558  odd2np1lem  13587  odd2np1  13588  gcdaddm  13709  modgcd  13716  bezoutlem1  13718  qredeq  13788  eulerthlem2  13853  modprm0  13869  opoe  13874  omoe  13875  opeo  13876  omeo  13877  pythagtriplem1  13879  pythagtriplem12  13889  pythagtriplem14  13891  iserodd  13898  gzmulcl  13995  4sqlem11  14012  4sqlem17  14018  cncrng  17796  cnfldmulg  17807  cnsubrg  17832  mulc1cncf  20440  icccvx  20481  pcorevlem  20557  itgcnlem  21226  itgneg  21240  itgconst  21255  itgadd  21261  iblabs  21265  itgmulc2  21270  dvmulbr  21372  dvmulf  21376  dvsincos  21412  plymullem1  21641  plymulcl  21648  plysubcl  21649  dgrcolem1  21699  dgrcolem2  21700  plydivlem4  21721  quotlem  21725  quotcl2  21727  quotdgr  21728  aaliou3lem3  21769  efper  21900  sinperlem  21901  sin2kpi  21904  cos2kpi  21905  efimpi  21912  sincosq1eq  21933  pige3  21938  abssinper  21939  sinkpi  21940  coskpi  21941  sineq0  21942  coseq1  21943  tanregt0  21954  efgh  21956  efif1olem4  21960  efifo  21962  eff1olem  21963  lognegb  21997  eflogeq  22009  efiarg  22015  tanarg  22027  logf1o2  22054  cxpcl  22078  cxpne0  22081  cxpsqrlem  22106  cxpsqr  22107  dvcxp1  22139  root1eq1  22152  cxpeq  22154  quad2  22193  quad  22194  dcubic2  22198  dcubic1  22199  dcubic  22200  mcubic  22201  cubic2  22202  cubic  22203  binom4  22204  dquartlem1  22205  dquartlem2  22206  dquart  22207  quart1cl  22208  quart1lem  22209  quart1  22210  quartlem1  22211  quartlem2  22212  quartlem3  22213  quart  22215  asinlem  22222  asinlem2  22223  asinlem3a  22224  asinlem3  22225  asinf  22226  atandm2  22231  atanf  22234  asinneg  22240  efiasin  22242  sinasin  22243  asinsinlem  22245  asinsin  22246  asinbnd  22253  cosasin  22258  atanneg  22261  atancj  22264  efiatan  22266  atanlogaddlem  22267  atanlogadd  22268  atanlogsublem  22269  atanlogsub  22270  efiatan2  22271  2efiatan  22272  tanatan  22273  cosatan  22275  atantan  22277  atanbndlem  22279  atans2  22285  dvatan  22289  atantayl  22291  atantayl2  22292  leibpilem1  22294  leibpilem2  22295  efrlim  22322  ftalem7  22375  basellem3  22379  basellem7  22383  basellem8  22384  basellem9  22385  ppiub  22502  dchrmulcl  22547  bposlem9  22590  lgsdir  22628  lgsdilem2  22629  lgsdi  22630  lgsne0  22631  lgsquadlem1  22652  2sqlem2  22662  rpvmasum2  22720  dchrisum0lem1  22724  dchrisum0lem2  22726  mulogsumlem  22739  mulog2sumlem3  22744  log2sumbnd  22752  selberglem1  22753  selberglem2  22754  selberg2  22759  pntlemk  22814  colinearalglem1  23087  colinearalglem2  23088  ax5seglem1  23109  axcontlem2  23146  axcontlem8  23152  ablomul  23777  efghgrp  23795  smcnlem  24027  ipval2  24037  4ipval2  24038  4ipval3  24042  ipidsq  24043  dipcj  24047  cncph  24154  ipasslem2  24167  ipasslem4  24169  ipasslem9  24173  ipasslem11  24175  hhssnv  24600  spansncol  24906  homulass  25141  lnfnmuli  25383  riesz3i  25401  zetacvg  26931  circum  27248  prodf  27331  clim2div  27333  prodfmul  27334  prodfn0  27338  prodfrec  27339  prodfdiv  27340  prodmolem3  27375  prodmolem2a  27376  fprodcl  27394  risefaccl  27447  fallfaccl  27448  faclim  27481  bpoly3  28130  fsumcube  28132  sin2h  28347  cos2h  28348  dvtanlem  28366  itg2addnclem3  28370  itgaddnc  28377  iblabsnc  28381  iblmulc2nc  28382  itgmulc2nc  28385  ftc1anclem3  28394  ftc1anclem6  28397  ftc1anclem7  28398  ftc1anclem8  28399  ftc1anc  28400  dvcncxp1  28402  dvasin  28405  cntotbnd  28620  rmxluc  29202  rmyluc  29203  jm2.17a  29228  jm2.18  29262  jm3.1lem1  29291  jm3.1lem2  29292  proot1ex  29494  lhe4.4ex1a  29528  expgrowthi  29532  expgrowth  29534  stoweidlem10  29730  wallispi2lem1  29791  wallispi2  29793  numclwlk3lem3  30591  sinh-conventional  30915  dpfrac1  30948