Theorem mulcl 11087

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

This theorem was proved from axioms:  ax-mulcl 11065

This theorem is referenced by:  mpomulf  11098  0cn  11101  mulrid  11107  mulcli  11116  mulcld  11129  mul31  11277  mul4  11278  mul02  11288  cnegex2  11292  muladd11r  11323  muladd  11546  subdi  11547  submul2  11554  mulsub  11557  recextlem1  11744  recex  11746  muleqadd  11758  mulnzcnf  11760  mulcan1g  11767  divass  11791  divmulass  11796  divmuldiv  11818  divmuleq  11823  divadddiv  11833  conjmul  11835  cju  12118  zneo  12553  cnref1o  12880  modcyc2  13808  muladdmodid  13814  negmod  13820  modaddmulmod  13842  expcl  13983  expclzlem  13987  mulexp  14005  sqcl  14022  subsq  14114  subsq2  14115  binom2sub  14124  mulbinom2  14127  binom3  14128  zesq  14130  bernneq  14133  bernneq2  14134  mulsubdivbinom2  14166  bcval5  14222  reim  15013  imcl  15015  crre  15018  crim  15019  remim  15021  mulre  15025  cjreb  15027  recj  15028  reneg  15029  readd  15030  remullem  15032  remul2  15034  imcj  15036  imneg  15037  imadd  15038  immul2  15041  cjadd  15045  ipcnval  15047  cjmulrcl  15048  cjneg  15051  imval2  15055  cjreim  15064  rennim  15143  cnpart  15144  sqrtneg  15171  sqabsadd  15186  sqabssub  15187  absreimsq  15196  absreim  15197  absmul  15198  sqreulem  15264  sqreu  15265  mulcn2  15500  o1mul  15519  climmul  15537  iseraltlem2  15587  prodf  15791  clim2div  15793  prodfmul  15794  prodfn0  15798  prodfrec  15799  prodfdiv  15800  prodmolem3  15837  prodmolem2a  15838  fprodcl  15856  fprodclf  15896  risefaccl  15919  fallfaccl  15920  bpoly3  15962  fsumcube  15964  efexp  16007  sinf  16030  cosf  16031  tanval2  16039  tanval3  16040  resinval  16041  recosval  16042  efi4p  16043  resin4p  16044  recos4p  16045  resincl  16046  recoscl  16047  sinneg  16052  cosneg  16053  efival  16058  efmival  16059  sinhval  16060  coshval  16061  retanhcl  16065  tanhlt1  16066  tanhbnd  16067  efeul  16068  sinadd  16070  cosadd  16071  sinsub  16074  cossub  16075  subsin  16077  sinmul  16078  cosmul  16079  addcos  16080  subcos  16081  cos2tsin  16085  ef01bndlem  16090  sin01bnd  16091  cos01bnd  16092  absef  16103  absefib  16104  efieq1re  16105  demoivre  16106  demoivreALT  16107  dvdscmulr  16192  dvdsmulcr  16193  odd2np1lem  16248  odd2np1  16249  opoe  16271  omoe  16272  opeo  16273  omeo  16274  gcdaddm  16433  modgcd  16440  bezoutlem1  16447  qredeq  16565  eulerthlem2  16690  modprm0  16714  pythagtriplem1  16725  pythagtriplem12  16735  pythagtriplem14  16737  iserodd  16744  gzmulcl  16847  4sqlem11  16864  4sqlem17  16870  cncrng  21323  cncrngOLD  21324  cnfldmulg  21338  cnsubrg  21362  mpomulcn  24783  mulc1cncf  24823  icccvx  24873  pcorevlem  24951  cnlmod  25065  cnstrcvs  25066  cncvs  25070  itgcnlem  25716  itgneg  25730  itgconst  25745  itgadd  25751  iblabs  25755  itgmulc2  25760  dvmulbr  25866  dvmulbrOLD  25867  dvmulf  25871  dvsincos  25910  plymullem1  26144  plymulcl  26151  plysubcl  26152  dgrcolem1  26204  dgrcolem2  26205  plydivlem4  26229  quotlem  26233  quotcl2  26235  quotdgr  26236  aaliou3lem3  26277  efper  26413  sinperlem  26414  sin2kpi  26417  cos2kpi  26418  efimpi  26425  sincosq1eq  26446  pige3ALT  26454  abssinper  26455  sinkpi  26456  coskpi  26457  sineq0  26458  coseq1  26459  tanregt0  26473  efif1olem4  26479  efifo  26481  eff1olem  26482  lognegb  26524  eflogeq  26536  efiarg  26541  tanarg  26553  logf1o2  26584  cxpcl  26608  cxpne0  26611  cxpsqrtlem  26636  cxpsqrt  26637  dvcxp1  26674  dvcncxp1  26677  root1eq1  26690  cxpeq  26692  relogbmul  26712  quad2  26774  quad  26775  dcubic2  26779  dcubic1  26780  dcubic  26781  mcubic  26782  cubic2  26783  cubic  26784  binom4  26785  dquartlem1  26786  dquartlem2  26787  dquart  26788  quart1cl  26789  quart1lem  26790  quart1  26791  quartlem1  26792  quartlem2  26793  quartlem3  26794  quart  26796  asinlem  26803  asinlem2  26804  asinlem3a  26805  asinlem3  26806  asinf  26807  atandm2  26812  atanf  26815  asinneg  26821  efiasin  26823  sinasin  26824  asinsinlem  26826  asinsin  26827  asinbnd  26834  cosasin  26839  atanneg  26842  atancj  26845  efiatan  26847  atanlogaddlem  26848  atanlogadd  26849  atanlogsublem  26850  atanlogsub  26851  efiatan2  26852  2efiatan  26853  tanatan  26854  cosatan  26856  atantan  26858  atanbndlem  26860  atans2  26866  dvatan  26870  atantayl  26872  atantayl2  26873  leibpilem2  26876  efrlim  26904  efrlimOLD  26905  zetacvg  26950  ftalem7  27014  basellem3  27018  basellem7  27022  basellem8  27023  basellem9  27024  ppiub  27140  dchrmulcl  27185  bposlem9  27228  lgsdir  27268  lgsdilem2  27269  lgsdi  27270  lgsne0  27271  lgsquadlem1  27316  2sqlem2  27354  rpvmasum2  27448  dchrisum0lem1  27452  dchrisum0lem2  27454  mulogsumlem  27467  mulog2sumlem3  27472  log2sumbnd  27480  selberglem1  27481  selberglem2  27482  selberg2  27487  pntlemk  27542  colinearalglem1  28882  colinearalglem2  28883  ax5seglem1  28904  axcontlem2  28941  axcontlem8  28947  numclwwlk3lem1  30357  smcnlem  30672  ipval2  30682  4ipval2  30683  ipidsq  30685  dipcj  30689  cncph  30794  ipasslem2  30807  ipasslem4  30809  ipasslem9  30813  ipasslem11  30815  hhssnv  31239  spansncol  31543  homulass  31777  lnfnmuli  32019  riesz3i  32037  circum  35706  faclim  35778  mpomulnzcnf  36332  sin2h  37649  cos2h  37650  itg2addnclem3  37712  itgaddnc  37719  iblabsnc  37723  iblmulc2nc  37724  itgmulc2nc  37727  ftc1anclem3  37734  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  dvasin  37743  cntotbnd  37835  rmxluc  42968  rmyluc  42969  jm2.17a  42992  jm2.18  43020  jm3.1lem1  43049  jm3.1lem2  43050  proot1ex  43228  lhe4.4ex1a  44361  expgrowthi  44365  expgrowth  44367  binomcxplemnotnn0  44388  dvsinax  45950  dvasinbx  45957  dvcosax  45963  stoweidlem10  46047  wallispi2lem1  46108  wallispi2  46110  fouriersw  46268  sinnpoly  46921  m1modmmod  47388  dfodd6  47667  opoeALTV  47713  opeoALTV  47714  2zrngnmrid  48286  sinh-conventional  49770  amgmwlem  49833