Theorem mulcl 11191

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105   · cmul 11112

This theorem was proved from axioms:  ax-mulcl 11169

This theorem is referenced by:  0cn  11203  mulrid  11209  mulcli  11218  mulcld  11231  mul31  11378  mul4  11379  mul02  11389  cnegex2  11393  muladd11r  11424  muladd  11643  subdi  11644  submul2  11651  mulsub  11654  recextlem1  11841  recex  11843  muleqadd  11855  mulnzcnopr  11857  mulcan1g  11864  divass  11887  divmulass  11892  divmuldiv  11911  divmuleq  11916  divadddiv  11926  conjmul  11928  cju  12205  zneo  12642  cnref1o  12966  modcyc2  13869  muladdmodid  13873  negmod  13878  modaddmulmod  13900  expcl  14042  expclzlem  14046  mulexp  14064  sqcl  14080  subsq  14171  subsq2  14172  binom2sub  14180  mulbinom2  14183  binom3  14184  zesq  14186  bernneq  14189  bernneq2  14190  mulsubdivbinom2  14219  bcval5  14275  reim  15053  imcl  15055  crre  15058  crim  15059  remim  15061  mulre  15065  cjreb  15067  recj  15068  reneg  15069  readd  15070  remullem  15072  remul2  15074  imcj  15076  imneg  15077  imadd  15078  immul2  15081  cjadd  15085  ipcnval  15087  cjmulrcl  15088  cjneg  15091  imval2  15095  cjreim  15104  rennim  15183  cnpart  15184  sqrtneg  15211  sqabsadd  15226  sqabssub  15227  absreimsq  15236  absreim  15237  absmul  15238  sqreulem  15303  sqreu  15304  mulcn2  15537  o1mul  15556  climmul  15574  iseraltlem2  15626  prodf  15830  clim2div  15832  prodfmul  15833  prodfn0  15837  prodfrec  15838  prodfdiv  15839  prodmolem3  15874  prodmolem2a  15875  fprodcl  15893  fprodclf  15933  risefaccl  15956  fallfaccl  15957  bpoly3  15999  fsumcube  16001  efexp  16041  sinf  16064  cosf  16065  tanval2  16073  tanval3  16074  resinval  16075  recosval  16076  efi4p  16077  resin4p  16078  recos4p  16079  resincl  16080  recoscl  16081  sinneg  16086  cosneg  16087  efival  16092  efmival  16093  sinhval  16094  coshval  16095  retanhcl  16099  tanhlt1  16100  tanhbnd  16101  efeul  16102  sinadd  16104  cosadd  16105  sinsub  16108  cossub  16109  subsin  16111  sinmul  16112  cosmul  16113  addcos  16114  subcos  16115  cos2tsin  16119  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  absef  16137  absefib  16138  efieq1re  16139  demoivre  16140  demoivreALT  16141  dvdscmulr  16225  dvdsmulcr  16226  odd2np1lem  16280  odd2np1  16281  opoe  16303  omoe  16304  opeo  16305  omeo  16306  gcdaddm  16463  modgcd  16471  bezoutlem1  16478  qredeq  16591  eulerthlem2  16712  modprm0  16735  pythagtriplem1  16746  pythagtriplem12  16756  pythagtriplem14  16758  iserodd  16765  gzmulcl  16868  4sqlem11  16885  4sqlem17  16891  cncrng  20959  cnfldmulg  20970  cnsubrg  20998  mulc1cncf  24413  icccvx  24458  pcorevlem  24534  cnlmod  24648  cnstrcvs  24649  cncvs  24653  itgcnlem  25299  itgneg  25313  itgconst  25328  itgadd  25334  iblabs  25338  itgmulc2  25343  dvmulbr  25448  dvmulf  25452  dvsincos  25490  plymullem1  25720  plymulcl  25727  plysubcl  25728  dgrcolem1  25779  dgrcolem2  25780  plydivlem4  25801  quotlem  25805  quotcl2  25807  quotdgr  25808  aaliou3lem3  25849  efper  25981  sinperlem  25982  sin2kpi  25985  cos2kpi  25986  efimpi  25993  sincosq1eq  26014  pige3ALT  26021  abssinper  26022  sinkpi  26023  coskpi  26024  sineq0  26025  coseq1  26026  tanregt0  26040  efif1olem4  26046  efifo  26048  eff1olem  26049  lognegb  26090  eflogeq  26102  efiarg  26107  tanarg  26119  logf1o2  26150  cxpcl  26174  cxpne0  26177  cxpsqrtlem  26202  cxpsqrt  26203  dvcxp1  26238  dvcncxp1  26241  root1eq1  26253  cxpeq  26255  relogbmul  26272  quad2  26334  quad  26335  dcubic2  26339  dcubic1  26340  dcubic  26341  mcubic  26342  cubic2  26343  cubic  26344  binom4  26345  dquartlem1  26346  dquartlem2  26347  dquart  26348  quart1cl  26349  quart1lem  26350  quart1  26351  quartlem1  26352  quartlem2  26353  quartlem3  26354  quart  26356  asinlem  26363  asinlem2  26364  asinlem3a  26365  asinlem3  26366  asinf  26367  atandm2  26372  atanf  26375  asinneg  26381  efiasin  26383  sinasin  26384  asinsinlem  26386  asinsin  26387  asinbnd  26394  cosasin  26399  atanneg  26402  atancj  26405  efiatan  26407  atanlogaddlem  26408  atanlogadd  26409  atanlogsublem  26410  atanlogsub  26411  efiatan2  26412  2efiatan  26413  tanatan  26414  cosatan  26416  atantan  26418  atanbndlem  26420  atans2  26426  dvatan  26430  atantayl  26432  atantayl2  26433  leibpilem2  26436  efrlim  26464  zetacvg  26509  ftalem7  26573  basellem3  26577  basellem7  26581  basellem8  26582  basellem9  26583  ppiub  26697  dchrmulcl  26742  bposlem9  26785  lgsdir  26825  lgsdilem2  26826  lgsdi  26827  lgsne0  26828  lgsquadlem1  26873  2sqlem2  26911  rpvmasum2  27005  dchrisum0lem1  27009  dchrisum0lem2  27011  mulogsumlem  27024  mulog2sumlem3  27029  log2sumbnd  27037  selberglem1  27038  selberglem2  27039  selberg2  27044  pntlemk  27099  colinearalglem1  28154  colinearalglem2  28155  ax5seglem1  28176  axcontlem2  28213  axcontlem8  28219  numclwwlk3lem1  29625  smcnlem  29938  ipval2  29948  4ipval2  29949  ipidsq  29951  dipcj  29955  cncph  30060  ipasslem2  30073  ipasslem4  30075  ipasslem9  30079  ipasslem11  30081  hhssnv  30505  spansncol  30809  homulass  31043  lnfnmuli  31285  riesz3i  31303  circum  34648  faclim  34705  mpomulf  35148  ovmul  35149  gg-dvmulbr  35164  sin2h  36467  cos2h  36468  itg2addnclem3  36530  itgaddnc  36537  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nc  36545  ftc1anclem3  36552  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  dvasin  36561  cntotbnd  36653  fac2xp3  41009  rmxluc  41661  rmyluc  41662  jm2.17a  41685  jm2.18  41713  jm3.1lem1  41742  jm3.1lem2  41743  proot1ex  41929  lhe4.4ex1a  43074  expgrowthi  43078  expgrowth  43080  binomcxplemnotnn0  43101  dvsinax  44616  dvasinbx  44623  dvcosax  44629  stoweidlem10  44713  wallispi2lem1  44774  wallispi2  44776  fouriersw  44934  dfodd6  46292  opoeALTV  46338  opeoALTV  46339  2zrngnmrid  46802  m1modmmod  47161  sinh-conventional  47738  amgmwlem  47803