Theorem mulcl 11239

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

This theorem was proved from axioms:  ax-mulcl 11217

This theorem is referenced by:  mpomulf  11250  0cn  11253  mulrid  11259  mulcli  11268  mulcld  11281  mul31  11428  mul4  11429  mul02  11439  cnegex2  11443  muladd11r  11474  muladd  11695  subdi  11696  submul2  11703  mulsub  11706  recextlem1  11893  recex  11895  muleqadd  11907  mulnzcnf  11909  mulcan1g  11916  divass  11940  divmulass  11945  divmuldiv  11967  divmuleq  11972  divadddiv  11982  conjmul  11984  cju  12262  zneo  12701  cnref1o  13027  modcyc2  13947  muladdmodid  13951  negmod  13957  modaddmulmod  13979  expcl  14120  expclzlem  14124  mulexp  14142  sqcl  14158  subsq  14249  subsq2  14250  binom2sub  14259  mulbinom2  14262  binom3  14263  zesq  14265  bernneq  14268  bernneq2  14269  mulsubdivbinom2  14301  bcval5  14357  reim  15148  imcl  15150  crre  15153  crim  15154  remim  15156  mulre  15160  cjreb  15162  recj  15163  reneg  15164  readd  15165  remullem  15167  remul2  15169  imcj  15171  imneg  15172  imadd  15173  immul2  15176  cjadd  15180  ipcnval  15182  cjmulrcl  15183  cjneg  15186  imval2  15190  cjreim  15199  rennim  15278  cnpart  15279  sqrtneg  15306  sqabsadd  15321  sqabssub  15322  absreimsq  15331  absreim  15332  absmul  15333  sqreulem  15398  sqreu  15399  mulcn2  15632  o1mul  15651  climmul  15669  iseraltlem2  15719  prodf  15923  clim2div  15925  prodfmul  15926  prodfn0  15930  prodfrec  15931  prodfdiv  15932  prodmolem3  15969  prodmolem2a  15970  fprodcl  15988  fprodclf  16028  risefaccl  16051  fallfaccl  16052  bpoly3  16094  fsumcube  16096  efexp  16137  sinf  16160  cosf  16161  tanval2  16169  tanval3  16170  resinval  16171  recosval  16172  efi4p  16173  resin4p  16174  recos4p  16175  resincl  16176  recoscl  16177  sinneg  16182  cosneg  16183  efival  16188  efmival  16189  sinhval  16190  coshval  16191  retanhcl  16195  tanhlt1  16196  tanhbnd  16197  efeul  16198  sinadd  16200  cosadd  16201  sinsub  16204  cossub  16205  subsin  16207  sinmul  16208  cosmul  16209  addcos  16210  subcos  16211  cos2tsin  16215  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  absef  16233  absefib  16234  efieq1re  16235  demoivre  16236  demoivreALT  16237  dvdscmulr  16322  dvdsmulcr  16323  odd2np1lem  16377  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  gcdaddm  16562  modgcd  16569  bezoutlem1  16576  qredeq  16694  eulerthlem2  16819  modprm0  16843  pythagtriplem1  16854  pythagtriplem12  16864  pythagtriplem14  16866  iserodd  16873  gzmulcl  16976  4sqlem11  16993  4sqlem17  16999  cncrng  21401  cncrngOLD  21402  cnfldmulg  21416  cnsubrg  21445  mpomulcn  24891  mulc1cncf  24931  icccvx  24981  pcorevlem  25059  cnlmod  25173  cnstrcvs  25174  cncvs  25178  itgcnlem  25825  itgneg  25839  itgconst  25854  itgadd  25860  iblabs  25864  itgmulc2  25869  dvmulbr  25975  dvmulbrOLD  25976  dvmulf  25980  dvsincos  26019  plymullem1  26253  plymulcl  26260  plysubcl  26261  dgrcolem1  26313  dgrcolem2  26314  plydivlem4  26338  quotlem  26342  quotcl2  26344  quotdgr  26345  aaliou3lem3  26386  efper  26521  sinperlem  26522  sin2kpi  26525  cos2kpi  26526  efimpi  26533  sincosq1eq  26554  pige3ALT  26562  abssinper  26563  sinkpi  26564  coskpi  26565  sineq0  26566  coseq1  26567  tanregt0  26581  efif1olem4  26587  efifo  26589  eff1olem  26590  lognegb  26632  eflogeq  26644  efiarg  26649  tanarg  26661  logf1o2  26692  cxpcl  26716  cxpne0  26719  cxpsqrtlem  26744  cxpsqrt  26745  dvcxp1  26782  dvcncxp1  26785  root1eq1  26798  cxpeq  26800  relogbmul  26820  quad2  26882  quad  26883  dcubic2  26887  dcubic1  26888  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  binom4  26893  dquartlem1  26894  dquartlem2  26895  dquart  26896  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem1  26900  quartlem2  26901  quartlem3  26902  quart  26904  asinlem  26911  asinlem2  26912  asinlem3a  26913  asinlem3  26914  asinf  26915  atandm2  26920  atanf  26923  asinneg  26929  efiasin  26931  sinasin  26932  asinsinlem  26934  asinsin  26935  asinbnd  26942  cosasin  26947  atanneg  26950  atancj  26953  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsublem  26958  atanlogsub  26959  efiatan2  26960  2efiatan  26961  tanatan  26962  cosatan  26964  atantan  26966  atanbndlem  26968  atans2  26974  dvatan  26978  atantayl  26980  atantayl2  26981  leibpilem2  26984  efrlim  27012  efrlimOLD  27013  zetacvg  27058  ftalem7  27122  basellem3  27126  basellem7  27130  basellem8  27131  basellem9  27132  ppiub  27248  dchrmulcl  27293  bposlem9  27336  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  lgsquadlem1  27424  2sqlem2  27462  rpvmasum2  27556  dchrisum0lem1  27560  dchrisum0lem2  27562  mulogsumlem  27575  mulog2sumlem3  27580  log2sumbnd  27588  selberglem1  27589  selberglem2  27590  selberg2  27595  pntlemk  27650  colinearalglem1  28921  colinearalglem2  28922  ax5seglem1  28943  axcontlem2  28980  axcontlem8  28986  numclwwlk3lem1  30401  smcnlem  30716  ipval2  30726  4ipval2  30727  ipidsq  30729  dipcj  30733  cncph  30838  ipasslem2  30851  ipasslem4  30853  ipasslem9  30857  ipasslem11  30859  hhssnv  31283  spansncol  31587  homulass  31821  lnfnmuli  32063  riesz3i  32081  circum  35679  faclim  35746  mpomulnzcnf  36300  sin2h  37617  cos2h  37618  itg2addnclem3  37680  itgaddnc  37687  iblabsnc  37691  iblmulc2nc  37692  itgmulc2nc  37695  ftc1anclem3  37702  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  dvasin  37711  cntotbnd  37803  fac2xp3  42240  rmxluc  42948  rmyluc  42949  jm2.17a  42972  jm2.18  43000  jm3.1lem1  43029  jm3.1lem2  43030  proot1ex  43208  lhe4.4ex1a  44348  expgrowthi  44352  expgrowth  44354  binomcxplemnotnn0  44375  dvsinax  45928  dvasinbx  45935  dvcosax  45941  stoweidlem10  46025  wallispi2lem1  46086  wallispi2  46088  fouriersw  46246  dfodd6  47624  opoeALTV  47670  opeoALTV  47671  2zrngnmrid  48172  m1modmmod  48442  sinh-conventional  49258  amgmwlem  49321