Theorem mulcl 10020

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990  (class class class)co 6650   CCcc 9934   x. cmul 9941

This theorem was proved from axioms:  ax-mulcl 9998

This theorem is referenced by:  0cn  10032  mulid1  10037  mulcli  10045  mulcld  10060  mul31  10204  mul4  10205  mul02  10214  cnegex2  10218  muladd11r  10249  muladd  10462  subdi  10463  submul2  10470  mulsub  10473  recextlem1  10657  recex  10659  muleqadd  10671  mulnzcnopr  10673  mulcan1g  10680  divass  10703  divmulass  10708  divmuldiv  10725  divmuleq  10730  divadddiv  10740  conjmul  10742  cju  11016  zneo  11460  cnref1o  11827  modcyc2  12706  muladdmodid  12710  negmod  12715  modaddmulmod  12737  expcl  12878  expclzlem  12884  mulexp  12899  sqcl  12925  subsq  12972  subsq2  12973  binom2sub  12981  mulbinom2  12984  binom3  12985  zesq  12987  bernneq  12990  bernneq2  12991  mulsubdivbinom2  13046  bcval5  13105  reim  13849  imcl  13851  crre  13854  crim  13855  remim  13857  mulre  13861  cjreb  13863  recj  13864  reneg  13865  readd  13866  remullem  13868  remul2  13870  imcj  13872  imneg  13873  imadd  13874  immul2  13877  cjadd  13881  ipcnval  13883  cjmulrcl  13884  cjneg  13887  imval2  13891  cjreim  13900  rennim  13979  cnpart  13980  sqrtneg  14008  sqabsadd  14022  sqabssub  14023  absreimsq  14032  absreim  14033  absmul  14034  sqreulem  14099  sqreu  14100  mulcn2  14326  o1mul  14345  climmul  14363  iseraltlem2  14413  prodf  14619  clim2div  14621  prodfmul  14622  prodfn0  14626  prodfrec  14627  prodfdiv  14628  prodmolem3  14663  prodmolem2a  14664  fprodcl  14682  fprodclf  14723  risefaccl  14746  fallfaccl  14747  bpoly3  14789  fsumcube  14791  efexp  14831  sinf  14854  cosf  14855  tanval2  14863  tanval3  14864  resinval  14865  recosval  14866  efi4p  14867  resin4p  14868  recos4p  14869  resincl  14870  recoscl  14871  sinneg  14876  cosneg  14877  efival  14882  efmival  14883  sinhval  14884  coshval  14885  retanhcl  14889  tanhlt1  14890  tanhbnd  14891  efeul  14892  sinadd  14894  cosadd  14895  sinsub  14898  cossub  14899  subsin  14901  sinmul  14902  cosmul  14903  addcos  14904  subcos  14905  cos2tsin  14909  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  absef  14927  absefib  14928  efieq1re  14929  demoivre  14930  demoivreALT  14931  dvdscmulr  15010  dvdsmulcr  15011  odd2np1lem  15064  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  gcdaddm  15246  modgcd  15253  bezoutlem1  15256  qredeq  15371  eulerthlem2  15487  modprm0  15510  pythagtriplem1  15521  pythagtriplem12  15531  pythagtriplem14  15533  iserodd  15540  gzmulcl  15642  4sqlem11  15659  4sqlem17  15665  cncrng  19767  cnfldmulg  19778  cnsubrg  19806  mulc1cncf  22708  icccvx  22749  pcorevlem  22826  cnlmod  22940  cnstrcvs  22941  cncvs  22945  itgcnlem  23556  itgneg  23570  itgconst  23585  itgadd  23591  iblabs  23595  itgmulc2  23600  dvmulbr  23702  dvmulf  23706  dvsincos  23744  plymullem1  23970  plymulcl  23977  plysubcl  23978  dgrcolem1  24029  dgrcolem2  24030  plydivlem4  24051  quotlem  24055  quotcl2  24057  quotdgr  24058  aaliou3lem3  24099  efper  24231  sinperlem  24232  sin2kpi  24235  cos2kpi  24236  efimpi  24243  sincosq1eq  24264  pige3  24269  abssinper  24270  sinkpi  24271  coskpi  24272  sineq0  24273  coseq1  24274  tanregt0  24285  efif1olem4  24291  efifo  24293  eff1olem  24294  lognegb  24336  eflogeq  24348  efiarg  24353  tanarg  24365  logf1o2  24396  cxpcl  24420  cxpne0  24423  cxpsqrtlem  24448  cxpsqrt  24449  dvcxp1  24481  dvcncxp1  24484  root1eq1  24496  cxpeq  24498  relogbmul  24515  quad2  24566  quad  24567  dcubic2  24571  dcubic1  24572  dcubic  24573  mcubic  24574  cubic2  24575  cubic  24576  binom4  24577  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1cl  24581  quart1lem  24582  quart1  24583  quartlem1  24584  quartlem2  24585  quartlem3  24586  quart  24588  asinlem  24595  asinlem2  24596  asinlem3a  24597  asinlem3  24598  asinf  24599  atandm2  24604  atanf  24607  asinneg  24613  efiasin  24615  sinasin  24616  asinsinlem  24618  asinsin  24619  asinbnd  24626  cosasin  24631  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  cosatan  24648  atantan  24650  atanbndlem  24652  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  leibpilem1  24667  leibpilem2  24668  efrlim  24696  zetacvg  24741  ftalem7  24805  basellem3  24809  basellem7  24813  basellem8  24814  basellem9  24815  ppiub  24929  dchrmulcl  24974  bposlem9  25017  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  lgsquadlem1  25105  2sqlem2  25143  rpvmasum2  25201  dchrisum0lem1  25205  dchrisum0lem2  25207  mulogsumlem  25220  mulog2sumlem3  25225  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  selberg2  25240  pntlemk  25295  colinearalglem1  25786  colinearalglem2  25787  ax5seglem1  25808  axcontlem2  25845  axcontlem8  25851  numclwlk3lem3  27206  smcnlem  27552  ipval2  27562  4ipval2  27563  ipidsq  27565  dipcj  27569  cncph  27674  ipasslem2  27687  ipasslem4  27689  ipasslem9  27693  ipasslem11  27695  hhssnv  28121  spansncol  28427  homulass  28661  lnfnmuli  28903  riesz3i  28921  dpfrac1OLD  29600  circum  31568  faclim  31632  sin2h  33399  cos2h  33400  itg2addnclem3  33463  itgaddnc  33470  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nc  33478  ftc1anclem3  33487  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  dvasin  33496  cntotbnd  33595  rmxluc  37501  rmyluc  37502  jm2.17a  37527  jm2.18  37555  jm3.1lem1  37584  jm3.1lem2  37585  proot1ex  37779  lhe4.4ex1a  38528  expgrowthi  38532  expgrowth  38534  binomcxplemnotnn0  38555  dvsinax  40127  dvasinbx  40135  dvcosax  40141  stoweidlem10  40227  wallispi2lem1  40288  wallispi2  40290  fouriersw  40448  dfodd6  41550  opoeALTV  41594  opeoALTV  41595  2zrngnmrid  41950  m1modmmod  42316  sinh-conventional  42480  amgmwlem  42548