Theorem mulcl 9579

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1804  (class class class)co 6281   CCcc 9493   x. cmul 9500

This theorem was proved from axioms:  ax-mulcl 9557

This theorem is referenced by:  0cn  9591  mulid1  9596  mulcli  9604  mulcld  9619  mul31  9751  mul4  9752  mul02  9761  cnegex2  9765  muladd  9996  subdi  9997  submul2  10004  mulsub  10006  recextlem1  10186  recex  10188  muleqadd  10200  mulnzcnopr  10202  mulcan1g  10209  divass  10232  divmuldiv  10251  divmuleq  10256  divadddiv  10266  conjmul  10268  cju  10539  zneo  10952  cnref1o  11226  modcyc2  12014  modaddmulmod  12035  expcl  12166  expclzlem  12172  mulexp  12187  sqcl  12212  subsq  12257  subsq2  12258  binom2sub  12267  binom3  12269  zesq  12271  bernneq  12274  bernneq2  12275  bcval5  12378  reim  12924  imcl  12926  crre  12929  crim  12930  remim  12932  mulre  12936  cjreb  12938  recj  12939  reneg  12940  readd  12941  remullem  12943  remul2  12945  imcj  12947  imneg  12948  imadd  12949  immul2  12952  cjadd  12956  ipcnval  12958  cjmulrcl  12959  cjneg  12962  imval2  12966  cjreim  12975  rennim  13054  cnpart  13055  sqrtneg  13083  sqabsadd  13097  sqabssub  13098  absreimsq  13107  absreim  13108  absmul  13109  sqreulem  13174  sqreu  13175  mulcn2  13400  o1mul  13419  climmul  13437  iseraltlem2  13487  prodf  13678  clim2div  13680  prodfmul  13681  prodfn0  13685  prodfrec  13686  prodfdiv  13687  prodmolem3  13722  prodmolem2a  13723  fprodcl  13741  efexp  13818  sinf  13841  cosf  13842  tanval2  13850  tanval3  13851  resinval  13852  recosval  13853  efi4p  13854  resin4p  13855  recos4p  13856  resincl  13857  recoscl  13858  sinneg  13863  cosneg  13864  efival  13869  efmival  13870  sinhval  13871  coshval  13872  retanhcl  13876  tanhlt1  13877  tanhbnd  13878  efeul  13879  sinadd  13881  cosadd  13882  sinsub  13885  cossub  13886  subsin  13888  sinmul  13889  cosmul  13890  addcos  13891  subcos  13892  cos2tsin  13896  ef01bndlem  13901  sin01bnd  13902  cos01bnd  13903  absef  13914  absefib  13915  efieq1re  13916  demoivre  13917  demoivreALT  13918  dvdscmulr  13994  dvdsmulcr  13995  odd2np1lem  14027  odd2np1  14028  gcdaddm  14149  modgcd  14156  bezoutlem1  14158  qredeq  14229  eulerthlem2  14294  modprm0  14312  opoe  14317  omoe  14318  opeo  14319  omeo  14320  pythagtriplem1  14322  pythagtriplem12  14332  pythagtriplem14  14334  iserodd  14341  gzmulcl  14438  4sqlem11  14455  4sqlem17  14461  cncrng  18418  cnfldmulg  18429  cnsubrg  18457  mulc1cncf  21387  icccvx  21428  pcorevlem  21504  itgcnlem  22174  itgneg  22188  itgconst  22203  itgadd  22209  iblabs  22213  itgmulc2  22218  dvmulbr  22320  dvmulf  22324  dvsincos  22360  plymullem1  22589  plymulcl  22596  plysubcl  22597  dgrcolem1  22648  dgrcolem2  22649  plydivlem4  22670  quotlem  22674  quotcl2  22676  quotdgr  22677  aaliou3lem3  22718  efper  22850  sinperlem  22851  sin2kpi  22854  cos2kpi  22855  efimpi  22862  sincosq1eq  22883  pige3  22888  abssinper  22889  sinkpi  22890  coskpi  22891  sineq0  22892  coseq1  22893  tanregt0  22904  efif1olem4  22910  efifo  22912  eff1olem  22913  lognegb  22952  eflogeq  22964  efiarg  22970  tanarg  22982  logf1o2  23009  cxpcl  23033  cxpne0  23036  cxpsqrtlem  23061  cxpsqrt  23062  dvcxp1  23094  root1eq1  23107  cxpeq  23109  quad2  23148  quad  23149  dcubic2  23153  dcubic1  23154  dcubic  23155  mcubic  23156  cubic2  23157  cubic  23158  binom4  23159  dquartlem1  23160  dquartlem2  23161  dquart  23162  quart1cl  23163  quart1lem  23164  quart1  23165  quartlem1  23166  quartlem2  23167  quartlem3  23168  quart  23170  asinlem  23177  asinlem2  23178  asinlem3a  23179  asinlem3  23180  asinf  23181  atandm2  23186  atanf  23189  asinneg  23195  efiasin  23197  sinasin  23198  asinsinlem  23200  asinsin  23201  asinbnd  23208  cosasin  23213  atanneg  23216  atancj  23219  efiatan  23221  atanlogaddlem  23222  atanlogadd  23223  atanlogsublem  23224  atanlogsub  23225  efiatan2  23226  2efiatan  23227  tanatan  23228  cosatan  23230  atantan  23232  atanbndlem  23234  atans2  23240  dvatan  23244  atantayl  23246  atantayl2  23247  leibpilem1  23249  leibpilem2  23250  efrlim  23277  ftalem7  23330  basellem3  23334  basellem7  23338  basellem8  23339  basellem9  23340  ppiub  23457  dchrmulcl  23502  bposlem9  23545  lgsdir  23583  lgsdilem2  23584  lgsdi  23585  lgsne0  23586  lgsquadlem1  23607  2sqlem2  23617  rpvmasum2  23675  dchrisum0lem1  23679  dchrisum0lem2  23681  mulogsumlem  23694  mulog2sumlem3  23699  log2sumbnd  23707  selberglem1  23708  selberglem2  23709  selberg2  23714  pntlemk  23769  colinearalglem1  24187  colinearalglem2  24188  ax5seglem1  24209  axcontlem2  24246  axcontlem8  24252  numclwlk3lem3  25051  ablomul  25335  efghgrpOLD  25353  smcnlem  25585  ipval2  25595  4ipval2  25596  4ipval3  25600  ipidsq  25601  dipcj  25605  cncph  25712  ipasslem2  25725  ipasslem4  25727  ipasslem9  25731  ipasslem11  25733  hhssnv  26158  spansncol  26464  homulass  26699  lnfnmuli  26941  riesz3i  26959  zetacvg  28535  circum  29018  risefaccl  29113  fallfaccl  29114  faclim  29147  bpoly3  29796  fsumcube  29798  sin2h  30021  cos2h  30022  dvtanlem  30040  itg2addnclem3  30044  itgaddnc  30051  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nc  30059  ftc1anclem3  30068  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  dvcncxp1  30076  dvasin  30079  cntotbnd  30268  rmxluc  30848  rmyluc  30849  jm2.17a  30874  jm2.18  30906  jm3.1lem1  30935  jm3.1lem2  30936  proot1ex  31137  lhe4.4ex1a  31210  expgrowthi  31214  expgrowth  31216  fprodclf  31549  dvsinax  31662  dvasinbx  31671  dvcosax  31677  stoweidlem10  31746  wallispi2lem1  31807  wallispi2  31809  fouriersw  31968  etransclem46  32017  2zrngnmrid  32583  sinh-conventional  33003  dpfrac1  33036