Theorem mulcl 9572

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767  (class class class)co 6282   CCcc 9486   x. cmul 9493

This theorem was proved from axioms:  ax-mulcl 9550

This theorem is referenced by:  0cn  9584  mulid1  9589  mulcli  9597  mulcld  9612  mul31  9743  mul4  9744  mul02  9753  cnegex2  9757  muladd  9985  subdi  9986  submul2  9993  mulsub  9995  recextlem1  10175  recex  10177  muleqadd  10189  mulnzcnopr  10191  mulcan1g  10198  divass  10221  divmuldiv  10240  divmuleq  10245  divadddiv  10255  conjmul  10257  cju  10528  zneo  10939  cnref1o  11211  modcyc2  11995  modaddmulmod  12016  expcl  12147  expclzlem  12153  mulexp  12167  sqcl  12192  subsq  12237  subsq2  12238  binom2sub  12247  binom3  12249  zesq  12251  bernneq  12254  bernneq2  12255  bcval5  12358  reim  12899  imcl  12901  crre  12904  crim  12905  remim  12907  mulre  12911  cjreb  12913  recj  12914  reneg  12915  readd  12916  remullem  12918  remul2  12920  imcj  12922  imneg  12923  imadd  12924  immul2  12927  cjadd  12931  ipcnval  12933  cjmulrcl  12934  cjneg  12937  imval2  12941  cjreim  12950  rennim  13029  cnpart  13030  sqrtneg  13058  sqabsadd  13072  sqabssub  13073  absreimsq  13082  absreim  13083  absmul  13084  sqreulem  13148  sqreu  13149  mulcn2  13374  o1mul  13393  climmul  13411  iseraltlem2  13461  efexp  13690  sinf  13713  cosf  13714  tanval2  13722  tanval3  13723  resinval  13724  recosval  13725  efi4p  13726  resin4p  13727  recos4p  13728  resincl  13729  recoscl  13730  sinneg  13735  cosneg  13736  efival  13741  efmival  13742  sinhval  13743  coshval  13744  retanhcl  13748  tanhlt1  13749  tanhbnd  13750  efeul  13751  sinadd  13753  cosadd  13754  sinsub  13757  cossub  13758  subsin  13760  sinmul  13761  cosmul  13762  addcos  13763  subcos  13764  cos2tsin  13768  ef01bndlem  13773  sin01bnd  13774  cos01bnd  13775  absef  13786  absefib  13787  efieq1re  13788  demoivre  13789  demoivreALT  13790  dvdscmulr  13866  dvdsmulcr  13867  odd2np1lem  13897  odd2np1  13898  gcdaddm  14019  modgcd  14026  bezoutlem1  14028  qredeq  14099  eulerthlem2  14164  modprm0  14182  opoe  14187  omoe  14188  opeo  14189  omeo  14190  pythagtriplem1  14192  pythagtriplem12  14202  pythagtriplem14  14204  iserodd  14211  gzmulcl  14308  4sqlem11  14325  4sqlem17  14331  cncrng  18207  cnfldmulg  18218  cnsubrg  18243  mulc1cncf  21141  icccvx  21182  pcorevlem  21258  itgcnlem  21928  itgneg  21942  itgconst  21957  itgadd  21963  iblabs  21967  itgmulc2  21972  dvmulbr  22074  dvmulf  22078  dvsincos  22114  plymullem1  22343  plymulcl  22350  plysubcl  22351  dgrcolem1  22401  dgrcolem2  22402  plydivlem4  22423  quotlem  22427  quotcl2  22429  quotdgr  22430  aaliou3lem3  22471  efper  22602  sinperlem  22603  sin2kpi  22606  cos2kpi  22607  efimpi  22614  sincosq1eq  22635  pige3  22640  abssinper  22641  sinkpi  22642  coskpi  22643  sineq0  22644  coseq1  22645  tanregt0  22656  efgh  22658  efif1olem4  22662  efifo  22664  eff1olem  22665  lognegb  22699  eflogeq  22711  efiarg  22717  tanarg  22729  logf1o2  22756  cxpcl  22780  cxpne0  22783  cxpsqrtlem  22808  cxpsqrt  22809  dvcxp1  22841  root1eq1  22854  cxpeq  22856  quad2  22895  quad  22896  dcubic2  22900  dcubic1  22901  dcubic  22902  mcubic  22903  cubic2  22904  cubic  22905  binom4  22906  dquartlem1  22907  dquartlem2  22908  dquart  22909  quart1cl  22910  quart1lem  22911  quart1  22912  quartlem1  22913  quartlem2  22914  quartlem3  22915  quart  22917  asinlem  22924  asinlem2  22925  asinlem3a  22926  asinlem3  22927  asinf  22928  atandm2  22933  atanf  22936  asinneg  22942  efiasin  22944  sinasin  22945  asinsinlem  22947  asinsin  22948  asinbnd  22955  cosasin  22960  atanneg  22963  atancj  22966  efiatan  22968  atanlogaddlem  22969  atanlogadd  22970  atanlogsublem  22971  atanlogsub  22972  efiatan2  22973  2efiatan  22974  tanatan  22975  cosatan  22977  atantan  22979  atanbndlem  22981  atans2  22987  dvatan  22991  atantayl  22993  atantayl2  22994  leibpilem1  22996  leibpilem2  22997  efrlim  23024  ftalem7  23077  basellem3  23081  basellem7  23085  basellem8  23086  basellem9  23087  ppiub  23204  dchrmulcl  23249  bposlem9  23292  lgsdir  23330  lgsdilem2  23331  lgsdi  23332  lgsne0  23333  lgsquadlem1  23354  2sqlem2  23364  rpvmasum2  23422  dchrisum0lem1  23426  dchrisum0lem2  23428  mulogsumlem  23441  mulog2sumlem3  23446  log2sumbnd  23454  selberglem1  23455  selberglem2  23456  selberg2  23461  pntlemk  23516  colinearalglem1  23882  colinearalglem2  23883  ax5seglem1  23904  axcontlem2  23941  axcontlem8  23947  numclwlk3lem3  24747  ablomul  25030  efghgrp  25048  smcnlem  25280  ipval2  25290  4ipval2  25291  4ipval3  25295  ipidsq  25296  dipcj  25300  cncph  25407  ipasslem2  25420  ipasslem4  25422  ipasslem9  25426  ipasslem11  25428  hhssnv  25853  spansncol  26159  homulass  26394  lnfnmuli  26636  riesz3i  26654  zetacvg  28194  circum  28512  prodf  28595  clim2div  28597  prodfmul  28598  prodfn0  28602  prodfrec  28603  prodfdiv  28604  prodmolem3  28639  prodmolem2a  28640  fprodcl  28658  risefaccl  28711  fallfaccl  28712  faclim  28745  bpoly3  29394  fsumcube  29396  sin2h  29620  cos2h  29621  dvtanlem  29639  itg2addnclem3  29643  itgaddnc  29650  iblabsnc  29654  iblmulc2nc  29655  itgmulc2nc  29658  ftc1anclem3  29667  ftc1anclem6  29670  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  dvcncxp1  29675  dvasin  29678  cntotbnd  29893  rmxluc  30474  rmyluc  30475  jm2.17a  30500  jm2.18  30534  jm3.1lem1  30563  jm3.1lem2  30564  proot1ex  30766  lhe4.4ex1a  30834  expgrowthi  30838  expgrowth  30840  coskpi2  31202  cosknegpi  31205  dvsinax  31241  dvmptdiv  31247  dvasinbx  31250  dvdivbd  31253  dvcosax  31256  itgsincmulx  31292  stoweidlem10  31310  wallispi2lem1  31371  wallispi2  31373  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem2  31399  dirkertrigeqlem3  31400  dirkertrigeq  31401  dirkeritg  31402  dirkercncflem2  31404  fourierdlem42  31449  fourierdlem48  31455  fourierdlem57  31464  fourierdlem62  31469  fourierdlem65  31472  fourierdlem73  31480  fourierdlem103  31510  fourierdlem104  31511  fourierswlem  31531  fouriersw  31532  sinh-conventional  32214  dpfrac1  32247