Theorem mulcl 11112

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

This theorem was proved from axioms:  ax-mulcl 11090

This theorem is referenced by:  mpomulf  11123  0cn  11126  mulrid  11132  mulcli  11141  mulcld  11154  mul31  11302  mul4  11303  mul02  11313  cnegex2  11317  muladd11r  11348  muladd  11571  subdi  11572  submul2  11579  mulsub  11582  recextlem1  11769  recex  11771  muleqadd  11783  mulnzcnf  11785  mulcan1g  11792  divass  11816  divmulass  11821  divmuldiv  11843  divmuleq  11848  divadddiv  11858  conjmul  11860  cju  12143  zneo  12578  cnref1o  12905  modcyc2  13830  muladdmodid  13836  negmod  13842  modaddmulmod  13864  expcl  14005  expclzlem  14009  mulexp  14027  sqcl  14044  subsq  14136  subsq2  14137  binom2sub  14146  mulbinom2  14149  binom3  14150  zesq  14152  bernneq  14155  bernneq2  14156  mulsubdivbinom2  14188  bcval5  14244  reim  15035  imcl  15037  crre  15040  crim  15041  remim  15043  mulre  15047  cjreb  15049  recj  15050  reneg  15051  readd  15052  remullem  15054  remul2  15056  imcj  15058  imneg  15059  imadd  15060  immul2  15063  cjadd  15067  ipcnval  15069  cjmulrcl  15070  cjneg  15073  imval2  15077  cjreim  15086  rennim  15165  cnpart  15166  sqrtneg  15193  sqabsadd  15208  sqabssub  15209  absreimsq  15218  absreim  15219  absmul  15220  sqreulem  15286  sqreu  15287  mulcn2  15522  o1mul  15541  climmul  15559  iseraltlem2  15609  prodf  15813  clim2div  15815  prodfmul  15816  prodfn0  15820  prodfrec  15821  prodfdiv  15822  prodmolem3  15859  prodmolem2a  15860  fprodcl  15878  fprodclf  15918  risefaccl  15941  fallfaccl  15942  bpoly3  15984  fsumcube  15986  efexp  16029  sinf  16052  cosf  16053  tanval2  16061  tanval3  16062  resinval  16063  recosval  16064  efi4p  16065  resin4p  16066  recos4p  16067  resincl  16068  recoscl  16069  sinneg  16074  cosneg  16075  efival  16080  efmival  16081  sinhval  16082  coshval  16083  retanhcl  16087  tanhlt1  16088  tanhbnd  16089  efeul  16090  sinadd  16092  cosadd  16093  sinsub  16096  cossub  16097  subsin  16099  sinmul  16100  cosmul  16101  addcos  16102  subcos  16103  cos2tsin  16107  ef01bndlem  16112  sin01bnd  16113  cos01bnd  16114  absef  16125  absefib  16126  efieq1re  16127  demoivre  16128  demoivreALT  16129  dvdscmulr  16214  dvdsmulcr  16215  odd2np1lem  16270  odd2np1  16271  opoe  16293  omoe  16294  opeo  16295  omeo  16296  gcdaddm  16455  modgcd  16462  bezoutlem1  16469  qredeq  16587  eulerthlem2  16712  modprm0  16736  pythagtriplem1  16747  pythagtriplem12  16757  pythagtriplem14  16759  iserodd  16766  gzmulcl  16869  4sqlem11  16886  4sqlem17  16892  cncrng  21314  cncrngOLD  21315  cnfldmulg  21329  cnsubrg  21353  mpomulcn  24775  mulc1cncf  24815  icccvx  24865  pcorevlem  24943  cnlmod  25057  cnstrcvs  25058  cncvs  25062  itgcnlem  25708  itgneg  25722  itgconst  25737  itgadd  25743  iblabs  25747  itgmulc2  25752  dvmulbr  25858  dvmulbrOLD  25859  dvmulf  25863  dvsincos  25902  plymullem1  26136  plymulcl  26143  plysubcl  26144  dgrcolem1  26196  dgrcolem2  26197  plydivlem4  26221  quotlem  26225  quotcl2  26227  quotdgr  26228  aaliou3lem3  26269  efper  26405  sinperlem  26406  sin2kpi  26409  cos2kpi  26410  efimpi  26417  sincosq1eq  26438  pige3ALT  26446  abssinper  26447  sinkpi  26448  coskpi  26449  sineq0  26450  coseq1  26451  tanregt0  26465  efif1olem4  26471  efifo  26473  eff1olem  26474  lognegb  26516  eflogeq  26528  efiarg  26533  tanarg  26545  logf1o2  26576  cxpcl  26600  cxpne0  26603  cxpsqrtlem  26628  cxpsqrt  26629  dvcxp1  26666  dvcncxp1  26669  root1eq1  26682  cxpeq  26684  relogbmul  26704  quad2  26766  quad  26767  dcubic2  26771  dcubic1  26772  dcubic  26773  mcubic  26774  cubic2  26775  cubic  26776  binom4  26777  dquartlem1  26778  dquartlem2  26779  dquart  26780  quart1cl  26781  quart1lem  26782  quart1  26783  quartlem1  26784  quartlem2  26785  quartlem3  26786  quart  26788  asinlem  26795  asinlem2  26796  asinlem3a  26797  asinlem3  26798  asinf  26799  atandm2  26804  atanf  26807  asinneg  26813  efiasin  26815  sinasin  26816  asinsinlem  26818  asinsin  26819  asinbnd  26826  cosasin  26831  atanneg  26834  atancj  26837  efiatan  26839  atanlogaddlem  26840  atanlogadd  26841  atanlogsublem  26842  atanlogsub  26843  efiatan2  26844  2efiatan  26845  tanatan  26846  cosatan  26848  atantan  26850  atanbndlem  26852  atans2  26858  dvatan  26862  atantayl  26864  atantayl2  26865  leibpilem2  26868  efrlim  26896  efrlimOLD  26897  zetacvg  26942  ftalem7  27006  basellem3  27010  basellem7  27014  basellem8  27015  basellem9  27016  ppiub  27132  dchrmulcl  27177  bposlem9  27220  lgsdir  27260  lgsdilem2  27261  lgsdi  27262  lgsne0  27263  lgsquadlem1  27308  2sqlem2  27346  rpvmasum2  27440  dchrisum0lem1  27444  dchrisum0lem2  27446  mulogsumlem  27459  mulog2sumlem3  27464  log2sumbnd  27472  selberglem1  27473  selberglem2  27474  selberg2  27479  pntlemk  27534  colinearalglem1  28870  colinearalglem2  28871  ax5seglem1  28892  axcontlem2  28929  axcontlem8  28935  numclwwlk3lem1  30345  smcnlem  30660  ipval2  30670  4ipval2  30671  ipidsq  30673  dipcj  30677  cncph  30782  ipasslem2  30795  ipasslem4  30797  ipasslem9  30801  ipasslem11  30803  hhssnv  31227  spansncol  31531  homulass  31765  lnfnmuli  32007  riesz3i  32025  circum  35666  faclim  35738  mpomulnzcnf  36292  sin2h  37609  cos2h  37610  itg2addnclem3  37672  itgaddnc  37679  iblabsnc  37683  iblmulc2nc  37684  itgmulc2nc  37687  ftc1anclem3  37694  ftc1anclem6  37697  ftc1anclem7  37698  ftc1anclem8  37699  ftc1anc  37700  dvasin  37703  cntotbnd  37795  rmxluc  42929  rmyluc  42930  jm2.17a  42953  jm2.18  42981  jm3.1lem1  43010  jm3.1lem2  43011  proot1ex  43189  lhe4.4ex1a  44322  expgrowthi  44326  expgrowth  44328  binomcxplemnotnn0  44349  dvsinax  45914  dvasinbx  45921  dvcosax  45927  stoweidlem10  46011  wallispi2lem1  46072  wallispi2  46074  fouriersw  46232  sinnpoly  46895  m1modmmod  47362  dfodd6  47641  opoeALTV  47687  opeoALTV  47688  2zrngnmrid  48260  sinh-conventional  49744  amgmwlem  49807