Theorem mulcl 9622

Description: Alias for ax-mulcl 9600, for naming consistency with mulcli 9647. (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 9600	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1870  (class class class)co 6305   CCcc 9536   x. cmul 9543

This theorem was proved from axioms:  ax-mulcl 9600

This theorem is referenced by:  0cn  9634  mulid1  9639  mulcli  9647  mulcld  9662  mul31  9800  mul4  9801  mul02  9810  cnegex2  9814  muladd  10050  subdi  10051  submul2  10058  mulsub  10060  recextlem1  10241  recex  10243  muleqadd  10255  mulnzcnopr  10257  mulcan1g  10264  divass  10287  divmuldiv  10306  divmuleq  10311  divadddiv  10321  conjmul  10323  cju  10605  zneo  11018  cnref1o  11297  modcyc2  12130  muladdmodid  12134  negmod  12135  modaddmulmod  12153  expcl  12287  expclzlem  12293  mulexp  12308  sqcl  12334  subsq  12379  subsq2  12380  binom2sub  12388  binom3  12390  zesq  12392  bernneq  12395  bernneq2  12396  bcval5  12500  reim  13151  imcl  13153  crre  13156  crim  13157  remim  13159  mulre  13163  cjreb  13165  recj  13166  reneg  13167  readd  13168  remullem  13170  remul2  13172  imcj  13174  imneg  13175  imadd  13176  immul2  13179  cjadd  13183  ipcnval  13185  cjmulrcl  13186  cjneg  13189  imval2  13193  cjreim  13202  rennim  13281  cnpart  13282  sqrtneg  13310  sqabsadd  13324  sqabssub  13325  absreimsq  13334  absreim  13335  absmul  13336  sqreulem  13401  sqreu  13402  mulcn2  13637  o1mul  13656  climmul  13674  iseraltlem2  13727  prodf  13921  clim2div  13923  prodfmul  13924  prodfn0  13928  prodfrec  13929  prodfdiv  13930  prodmolem3  13965  prodmolem2a  13966  fprodcl  13984  fprodclf  14024  risefaccl  14046  fallfaccl  14047  bpoly3  14089  fsumcube  14091  efexp  14133  sinf  14156  cosf  14157  tanval2  14165  tanval3  14166  resinval  14167  recosval  14168  efi4p  14169  resin4p  14170  recos4p  14171  resincl  14172  recoscl  14173  sinneg  14178  cosneg  14179  efival  14184  efmival  14185  sinhval  14186  coshval  14187  retanhcl  14191  tanhlt1  14192  tanhbnd  14193  efeul  14194  sinadd  14196  cosadd  14197  sinsub  14200  cossub  14201  subsin  14203  sinmul  14204  cosmul  14205  addcos  14206  subcos  14207  cos2tsin  14211  ef01bndlem  14216  sin01bnd  14217  cos01bnd  14218  absef  14229  absefib  14230  efieq1re  14231  demoivre  14232  demoivreALT  14233  dvdscmulr  14309  dvdsmulcr  14310  odd2np1lem  14342  odd2np1  14343  gcdaddm  14467  modgcd  14474  bezoutlem1  14477  qredeq  14634  eulerthlem2  14699  modprm0  14719  opoe  14724  omoe  14725  opeo  14726  omeo  14727  pythagtriplem1  14729  pythagtriplem12  14739  pythagtriplem14  14741  iserodd  14748  gzmulcl  14845  4sqlem11  14862  4sqlem17OLD  14868  4sqlem17  14874  cncrng  18924  cnfldmulg  18935  cnsubrg  18963  mulc1cncf  21833  icccvx  21874  pcorevlem  21950  itgcnlem  22624  itgneg  22638  itgconst  22653  itgadd  22659  iblabs  22663  itgmulc2  22668  dvmulbr  22770  dvmulf  22774  dvsincos  22810  plymullem1  23036  plymulcl  23043  plysubcl  23044  dgrcolem1  23095  dgrcolem2  23096  plydivlem4  23117  quotlem  23121  quotcl2  23123  quotdgr  23124  aaliou3lem3  23165  efper  23299  sinperlem  23300  sin2kpi  23303  cos2kpi  23304  efimpi  23311  sincosq1eq  23332  pige3  23337  abssinper  23338  sinkpi  23339  coskpi  23340  sineq0  23341  coseq1  23342  tanregt0  23353  efif1olem4  23359  efifo  23361  eff1olem  23362  lognegb  23404  eflogeq  23416  efiarg  23421  tanarg  23433  logf1o2  23460  cxpcl  23484  cxpne0  23487  cxpsqrtlem  23512  cxpsqrt  23513  dvcxp1  23545  dvcncxp1  23548  root1eq1  23560  cxpeq  23562  relogbmul  23579  quad2  23630  quad  23631  dcubic2  23635  dcubic1  23636  dcubic  23637  mcubic  23638  cubic2  23639  cubic  23640  binom4  23641  dquartlem1  23642  dquartlem2  23643  dquart  23644  quart1cl  23645  quart1lem  23646  quart1  23647  quartlem1  23648  quartlem2  23649  quartlem3  23650  quart  23652  asinlem  23659  asinlem2  23660  asinlem3a  23661  asinlem3  23662  asinf  23663  atandm2  23668  atanf  23671  asinneg  23677  efiasin  23679  sinasin  23680  asinsinlem  23682  asinsin  23683  asinbnd  23690  cosasin  23695  atanneg  23698  atancj  23701  efiatan  23703  atanlogaddlem  23704  atanlogadd  23705  atanlogsublem  23706  atanlogsub  23707  efiatan2  23708  2efiatan  23709  tanatan  23710  cosatan  23712  atantan  23714  atanbndlem  23716  atans2  23722  dvatan  23726  atantayl  23728  atantayl2  23729  leibpilem1  23731  leibpilem2  23732  efrlim  23760  zetacvg  23805  ftalem7  23868  basellem3  23872  basellem7  23876  basellem8  23877  basellem9  23878  ppiub  23995  dchrmulcl  24040  bposlem9  24083  lgsdir  24121  lgsdilem2  24122  lgsdi  24123  lgsne0  24124  lgsquadlem1  24145  2sqlem2  24155  rpvmasum2  24213  dchrisum0lem1  24217  dchrisum0lem2  24219  mulogsumlem  24232  mulog2sumlem3  24237  log2sumbnd  24245  selberglem1  24246  selberglem2  24247  selberg2  24252  pntlemk  24307  colinearalglem1  24782  colinearalglem2  24783  ax5seglem1  24804  axcontlem2  24841  axcontlem8  24847  numclwlk3lem3  25646  ablomul  25928  efghgrpOLD  25946  smcnlem  26178  ipval2  26188  4ipval2  26189  4ipval3  26193  ipidsq  26194  dipcj  26198  cncph  26305  ipasslem2  26318  ipasslem4  26320  ipasslem9  26324  ipasslem11  26326  hhssnv  26750  spansncol  27056  homulass  27290  lnfnmuli  27532  riesz3i  27550  circum  30106  faclim  30169  sin2h  31639  cos2h  31640  dvtanlemOLD  31695  itg2addnclem3  31699  itgaddnc  31706  iblabsnc  31710  iblmulc2nc  31711  itgmulc2nc  31714  ftc1anclem3  31723  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  dvasin  31732  cntotbnd  31832  rmxluc  35490  rmyluc  35491  jm2.17a  35516  jm2.18  35549  jm3.1lem1  35578  jm3.1lem2  35579  proot1ex  35777  lhe4.4ex1a  36315  expgrowthi  36319  expgrowth  36321  binomcxplemnotnn0  36342  dvsinax  37355  dvasinbx  37364  dvcosax  37370  stoweidlem10  37439  wallispi2lem1  37502  wallispi2  37504  fouriersw  37663  dfodd6  38157  opoeALTV  38202  opeoALTV  38203  2zrngnmrid  38708  m1modmmod  39085  sinh-conventional  39220  dpfrac1  39253