Theorem mulcl 11154

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

This theorem was proved from axioms:  ax-mulcl 11132

This theorem is referenced by:  mpomulf  11165  0cn  11168  mulrid  11176  mulcli  11186  mulcld  11199  mul31  11347  mul4  11348  mul02  11358  cnegex2  11362  muladd11r  11393  muladd  11616  subdi  11617  submul2  11624  mulsub  11627  recextlem1  11814  recex  11816  muleqadd  11828  mulnzcnf  11830  mulcan1g  11837  divass  11860  divmulass  11865  divmuldiv  11888  divmuleq  11893  divadddiv  11903  conjmul  11905  cju  12188  zneo  12653  cnref1o  12983  modcyc2  13914  muladdmodid  13920  negmod  13926  modaddmulmod  13948  expcl  14089  expclzlem  14093  mulexp  14111  sqcl  14128  subsq  14220  subsq2  14221  binom2sub  14230  mulbinom2  14233  binom3  14234  zesq  14236  bernneq  14239  bernneq2  14240  mulsubdivbinom2  14272  bcval5  14328  reim  15119  imcl  15121  crre  15124  crim  15125  remim  15127  mulre  15131  cjreb  15133  recj  15134  reneg  15135  readd  15136  remullem  15138  remul2  15140  imcj  15142  imneg  15143  imadd  15144  immul2  15147  cjadd  15151  ipcnval  15153  cjmulrcl  15154  cjneg  15157  imval2  15161  cjreim  15170  rennim  15249  cnpart  15250  sqrtneg  15277  sqabsadd  15292  sqabssub  15293  absreimsq  15302  absreim  15303  absmul  15304  sqreulem  15370  sqreu  15371  mulcn2  15606  o1mul  15625  climmul  15643  iseraltlem2  15693  prodf  15900  clim2div  15902  prodfmul  15903  prodfn0  15907  prodfrec  15908  prodfdiv  15909  prodmolem3  15946  prodmolem2a  15947  fprodcl  15965  fprodclf  16005  risefaccl  16028  fallfaccl  16029  bpoly3  16071  fsumcube  16073  efexp  16116  sinf  16139  cosf  16140  tanval2  16148  tanval3  16149  resinval  16150  recosval  16151  efi4p  16152  resin4p  16153  recos4p  16154  resincl  16155  recoscl  16156  sinneg  16161  cosneg  16162  efival  16167  efmival  16168  sinhval  16169  coshval  16170  retanhcl  16174  tanhlt1  16175  tanhbnd  16176  efeul  16177  sinadd  16179  cosadd  16180  sinsub  16183  cossub  16184  subsin  16186  sinmul  16187  cosmul  16188  addcos  16189  subcos  16190  cos2tsin  16194  ef01bndlem  16199  sin01bnd  16200  cos01bnd  16201  absef  16212  absefib  16213  efieq1re  16214  demoivre  16215  demoivreALT  16216  dvdscmulr  16301  dvdsmulcr  16302  odd2np1lem  16357  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  gcdaddm  16542  modgcd  16549  bezoutlem1  16556  qredeq  16674  eulerthlem2  16800  modprm0  16824  pythagtriplem1  16835  pythagtriplem12  16845  pythagtriplem14  16847  iserodd  16854  gzmulcl  16957  4sqlem11  16974  4sqlem17  16980  cncrng  21425  cnfldmulg  21436  cnsubrg  21459  mpomulcn  24909  mulc1cncf  24947  icccvx  24992  pcorevlem  25068  cnlmod  25182  cnstrcvs  25183  cncvs  25187  itgcnlem  25832  itgneg  25846  itgconst  25861  itgadd  25867  iblabs  25871  itgmulc2  25876  dvmulbr  25981  dvmulf  25985  dvsincos  26023  plymullem1  26254  plymulcl  26261  plysubcl  26262  dgrcolem1  26313  dgrcolem2  26314  plydivlem4  26337  quotlem  26341  quotcl2  26343  quotdgr  26344  aaliou3lem3  26385  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  26797  cxpeq  26799  relogbmul  26819  quad2  26881  quad  26882  dcubic2  26886  dcubic1  26887  dcubic  26888  mcubic  26889  cubic2  26890  cubic  26891  binom4  26892  dquartlem1  26893  dquartlem2  26894  dquart  26895  quart1cl  26896  quart1lem  26897  quart1  26898  quartlem1  26899  quartlem2  26900  quartlem3  26901  quart  26903  asinlem  26910  asinlem2  26911  asinlem3a  26912  asinlem3  26913  asinf  26914  atandm2  26919  atanf  26922  asinneg  26928  efiasin  26930  sinasin  26931  asinsinlem  26933  asinsin  26934  asinbnd  26941  cosasin  26946  atanneg  26949  atancj  26952  efiatan  26954  atanlogaddlem  26955  atanlogadd  26956  atanlogsublem  26957  atanlogsub  26958  efiatan2  26959  2efiatan  26960  tanatan  26961  cosatan  26963  atantan  26965  atanbndlem  26967  atans2  26973  dvatan  26977  atantayl  26979  atantayl2  26980  leibpilem2  26983  efrlim  27011  zetacvg  27056  ftalem7  27120  basellem3  27124  basellem7  27128  basellem8  27129  basellem9  27130  ppiub  27245  dchrmulcl  27290  bposlem9  27333  lgsdir  27373  lgsdilem2  27374  lgsdi  27375  lgsne0  27376  lgsquadlem1  27421  2sqlem2  27459  rpvmasum2  27553  dchrisum0lem1  27557  dchrisum0lem2  27559  mulogsumlem  27572  mulog2sumlem3  27577  log2sumbnd  27585  selberglem1  27586  selberglem2  27587  selberg2  27592  pntlemk  27647  colinearalglem1  29053  colinearalglem2  29054  ax5seglem1  29075  axcontlem2  29112  axcontlem8  29118  numclwwlk3lem1  30530  smcnlem  30846  ipval2  30856  4ipval2  30857  ipidsq  30859  dipcj  30863  cncph  30968  ipasslem2  30981  ipasslem4  30983  ipasslem9  30987  ipasslem11  30989  hhssnv  31413  spansncol  31717  homulass  31951  lnfnmuli  32193  riesz3i  32211  circum  35988  faclim  36060  mpomulnzcnf  36623  sin2h  38073  cos2h  38074  itg2addnclem3  38136  itgaddnc  38143  iblabsnc  38147  iblmulc2nc  38148  itgmulc2nc  38151  ftc1anclem3  38158  ftc1anclem6  38161  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  dvasin  38167  cntotbnd  38259  rmxluc  43477  rmyluc  43478  jm2.17a  43501  jm2.18  43529  jm3.1lem1  43558  jm3.1lem2  43559  proot1ex  43737  lhe4.4ex1a  44869  expgrowthi  44873  expgrowth  44875  binomcxplemnotnn0  44896  dvsinax  46451  dvasinbx  46458  dvcosax  46464  stoweidlem10  46548  wallispi2lem1  46609  wallispi2  46611  fouriersw  46769  sinnpoly  47449  m1modmmod  47922  dfodd6  48223  opoeALTV  48269  opeoALTV  48270  2zrngnmrid  48842  sinh-conventional  50324  amgmwlem  50387