Theorem mulcl 9899

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

Assertion

Ref	Expression
mulcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 9877	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

This theorem was proved from axioms:  ax-mulcl 9877

This theorem is referenced by:  0cn  9911  mulid1  9916  mulcli  9924  mulcld  9939  mul31  10083  mul4  10084  mul02  10093  cnegex2  10097  muladd11r  10128  muladd  10341  subdi  10342  submul2  10349  mulsub  10352  recextlem1  10536  recex  10538  muleqadd  10550  mulnzcnopr  10552  mulcan1g  10559  divass  10582  divmulass  10587  divmuldiv  10604  divmuleq  10609  divadddiv  10619  conjmul  10621  cju  10893  zneo  11336  cnref1o  11703  modcyc2  12568  muladdmodid  12572  negmod  12577  modaddmulmod  12599  expcl  12740  expclzlem  12746  mulexp  12761  sqcl  12787  subsq  12834  subsq2  12835  binom2sub  12843  mulbinom2  12846  binom3  12847  zesq  12849  bernneq  12852  bernneq2  12853  mulsubdivbinom2  12908  bcval5  12967  reim  13697  imcl  13699  crre  13702  crim  13703  remim  13705  mulre  13709  cjreb  13711  recj  13712  reneg  13713  readd  13714  remullem  13716  remul2  13718  imcj  13720  imneg  13721  imadd  13722  immul2  13725  cjadd  13729  ipcnval  13731  cjmulrcl  13732  cjneg  13735  imval2  13739  cjreim  13748  rennim  13827  cnpart  13828  sqrtneg  13856  sqabsadd  13870  sqabssub  13871  absreimsq  13880  absreim  13881  absmul  13882  sqreulem  13947  sqreu  13948  mulcn2  14174  o1mul  14193  climmul  14211  iseraltlem2  14261  prodf  14458  clim2div  14460  prodfmul  14461  prodfn0  14465  prodfrec  14466  prodfdiv  14467  prodmolem3  14502  prodmolem2a  14503  fprodcl  14521  fprodclf  14562  risefaccl  14585  fallfaccl  14586  bpoly3  14628  fsumcube  14630  efexp  14670  sinf  14693  cosf  14694  tanval2  14702  tanval3  14703  resinval  14704  recosval  14705  efi4p  14706  resin4p  14707  recos4p  14708  resincl  14709  recoscl  14710  sinneg  14715  cosneg  14716  efival  14721  efmival  14722  sinhval  14723  coshval  14724  retanhcl  14728  tanhlt1  14729  tanhbnd  14730  efeul  14731  sinadd  14733  cosadd  14734  sinsub  14737  cossub  14738  subsin  14740  sinmul  14741  cosmul  14742  addcos  14743  subcos  14744  cos2tsin  14748  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  absef  14766  absefib  14767  efieq1re  14768  demoivre  14769  demoivreALT  14770  dvdscmulr  14848  dvdsmulcr  14849  odd2np1lem  14902  odd2np1  14903  opoe  14925  omoe  14926  opeo  14927  omeo  14928  gcdaddm  15084  modgcd  15091  bezoutlem1  15094  qredeq  15209  eulerthlem2  15325  modprm0  15348  pythagtriplem1  15359  pythagtriplem12  15369  pythagtriplem14  15371  iserodd  15378  gzmulcl  15480  4sqlem11  15497  4sqlem17  15503  cncrng  19586  cnfldmulg  19597  cnsubrg  19625  mulc1cncf  22516  icccvx  22557  pcorevlem  22634  cnlmod  22748  cnstrcvs  22749  cncvs  22753  itgcnlem  23362  itgneg  23376  itgconst  23391  itgadd  23397  iblabs  23401  itgmulc2  23406  dvmulbr  23508  dvmulf  23512  dvsincos  23548  plymullem1  23774  plymulcl  23781  plysubcl  23782  dgrcolem1  23833  dgrcolem2  23834  plydivlem4  23855  quotlem  23859  quotcl2  23861  quotdgr  23862  aaliou3lem3  23903  efper  24035  sinperlem  24036  sin2kpi  24039  cos2kpi  24040  efimpi  24047  sincosq1eq  24068  pige3  24073  abssinper  24074  sinkpi  24075  coskpi  24076  sineq0  24077  coseq1  24078  tanregt0  24089  efif1olem4  24095  efifo  24097  eff1olem  24098  lognegb  24140  eflogeq  24152  efiarg  24157  tanarg  24169  logf1o2  24196  cxpcl  24220  cxpne0  24223  cxpsqrtlem  24248  cxpsqrt  24249  dvcxp1  24281  dvcncxp1  24284  root1eq1  24296  cxpeq  24298  relogbmul  24315  quad2  24366  quad  24367  dcubic2  24371  dcubic1  24372  dcubic  24373  mcubic  24374  cubic2  24375  cubic  24376  binom4  24377  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1cl  24381  quart1lem  24382  quart1  24383  quartlem1  24384  quartlem2  24385  quartlem3  24386  quart  24388  asinlem  24395  asinlem2  24396  asinlem3a  24397  asinlem3  24398  asinf  24399  atandm2  24404  atanf  24407  asinneg  24413  efiasin  24415  sinasin  24416  asinsinlem  24418  asinsin  24419  asinbnd  24426  cosasin  24431  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  cosatan  24448  atantan  24450  atanbndlem  24452  atans2  24458  dvatan  24462  atantayl  24464  atantayl2  24465  leibpilem1  24467  leibpilem2  24468  efrlim  24496  zetacvg  24541  ftalem7  24605  basellem3  24609  basellem7  24613  basellem8  24614  basellem9  24615  ppiub  24729  dchrmulcl  24774  bposlem9  24817  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  lgsquadlem1  24905  2sqlem2  24943  rpvmasum2  25001  dchrisum0lem1  25005  dchrisum0lem2  25007  mulogsumlem  25020  mulog2sumlem3  25025  log2sumbnd  25033  selberglem1  25034  selberglem2  25035  selberg2  25040  pntlemk  25095  colinearalglem1  25586  colinearalglem2  25587  ax5seglem1  25608  axcontlem2  25645  axcontlem8  25651  numclwlk3lem3  26600  smcnlem  26936  ipval2  26946  4ipval2  26947  ipidsq  26949  dipcj  26953  cncph  27058  ipasslem2  27071  ipasslem4  27073  ipasslem9  27077  ipasslem11  27079  hhssnv  27505  spansncol  27811  homulass  28045  lnfnmuli  28287  riesz3i  28305  circum  30822  faclim  30885  sin2h  32569  cos2h  32570  itg2addnclem3  32633  itgaddnc  32640  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nc  32648  ftc1anclem3  32657  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  dvasin  32666  cntotbnd  32765  rmxluc  36519  rmyluc  36520  jm2.17a  36545  jm2.18  36573  jm3.1lem1  36602  jm3.1lem2  36603  proot1ex  36798  lhe4.4ex1a  37550  expgrowthi  37554  expgrowth  37556  binomcxplemnotnn0  37577  dvsinax  38801  dvasinbx  38810  dvcosax  38816  stoweidlem10  38903  wallispi2lem1  38964  wallispi2  38966  fouriersw  39124  dfodd6  40088  opoeALTV  40132  opeoALTV  40133  av-numclwlk3lem3  41506  2zrngnmrid  41740  m1modmmod  42110  sinh-conventional  42279  dpfrac1OLD  42313  amgmwlem  42357