Theorem mulcl 11113

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

This theorem was proved from axioms:  ax-mulcl 11091

This theorem is referenced by:  mpomulf  11124  0cn  11127  mulrid  11133  mulcli  11143  mulcld  11156  mul31  11304  mul4  11305  mul02  11315  cnegex2  11319  muladd11r  11350  muladd  11573  subdi  11574  submul2  11581  mulsub  11584  recextlem1  11771  recex  11773  muleqadd  11785  mulnzcnf  11787  mulcan1g  11794  divass  11818  divmulass  11823  divmuldiv  11846  divmuleq  11851  divadddiv  11861  conjmul  11863  cju  12146  zneo  12603  cnref1o  12926  modcyc2  13857  muladdmodid  13863  negmod  13869  modaddmulmod  13891  expcl  14032  expclzlem  14036  mulexp  14054  sqcl  14071  subsq  14163  subsq2  14164  binom2sub  14173  mulbinom2  14176  binom3  14177  zesq  14179  bernneq  14182  bernneq2  14183  mulsubdivbinom2  14215  bcval5  14271  reim  15062  imcl  15064  crre  15067  crim  15068  remim  15070  mulre  15074  cjreb  15076  recj  15077  reneg  15078  readd  15079  remullem  15081  remul2  15083  imcj  15085  imneg  15086  imadd  15087  immul2  15090  cjadd  15094  ipcnval  15096  cjmulrcl  15097  cjneg  15100  imval2  15104  cjreim  15113  rennim  15192  cnpart  15193  sqrtneg  15220  sqabsadd  15235  sqabssub  15236  absreimsq  15245  absreim  15246  absmul  15247  sqreulem  15313  sqreu  15314  mulcn2  15549  o1mul  15568  climmul  15586  iseraltlem2  15636  prodf  15843  clim2div  15845  prodfmul  15846  prodfn0  15850  prodfrec  15851  prodfdiv  15852  prodmolem3  15889  prodmolem2a  15890  fprodcl  15908  fprodclf  15948  risefaccl  15971  fallfaccl  15972  bpoly3  16014  fsumcube  16016  efexp  16059  sinf  16082  cosf  16083  tanval2  16091  tanval3  16092  resinval  16093  recosval  16094  efi4p  16095  resin4p  16096  recos4p  16097  resincl  16098  recoscl  16099  sinneg  16104  cosneg  16105  efival  16110  efmival  16111  sinhval  16112  coshval  16113  retanhcl  16117  tanhlt1  16118  tanhbnd  16119  efeul  16120  sinadd  16122  cosadd  16123  sinsub  16126  cossub  16127  subsin  16129  sinmul  16130  cosmul  16131  addcos  16132  subcos  16133  cos2tsin  16137  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  absef  16155  absefib  16156  efieq1re  16157  demoivre  16158  demoivreALT  16159  dvdscmulr  16244  dvdsmulcr  16245  odd2np1lem  16300  odd2np1  16301  opoe  16323  omoe  16324  opeo  16325  omeo  16326  gcdaddm  16485  modgcd  16492  bezoutlem1  16499  qredeq  16617  eulerthlem2  16743  modprm0  16767  pythagtriplem1  16778  pythagtriplem12  16788  pythagtriplem14  16790  iserodd  16797  gzmulcl  16900  4sqlem11  16917  4sqlem17  16923  cncrng  21378  cncrngOLD  21379  cnfldmulg  21393  cnsubrg  21417  mpomulcn  24844  mulc1cncf  24882  icccvx  24927  pcorevlem  25003  cnlmod  25117  cnstrcvs  25118  cncvs  25122  itgcnlem  25767  itgneg  25781  itgconst  25796  itgadd  25802  iblabs  25806  itgmulc2  25811  dvmulbr  25916  dvmulf  25920  dvsincos  25958  plymullem1  26189  plymulcl  26196  plysubcl  26197  dgrcolem1  26248  dgrcolem2  26249  plydivlem4  26273  quotlem  26277  quotcl2  26279  quotdgr  26280  aaliou3lem3  26321  efper  26456  sinperlem  26457  sin2kpi  26460  cos2kpi  26461  efimpi  26468  sincosq1eq  26489  pige3ALT  26497  abssinper  26498  sinkpi  26499  coskpi  26500  sineq0  26501  coseq1  26502  tanregt0  26516  efif1olem4  26522  efifo  26524  eff1olem  26525  lognegb  26567  eflogeq  26579  efiarg  26584  tanarg  26596  logf1o2  26627  cxpcl  26651  cxpne0  26654  cxpsqrtlem  26679  cxpsqrt  26680  dvcxp1  26717  dvcncxp1  26720  root1eq1  26732  cxpeq  26734  relogbmul  26754  quad2  26816  quad  26817  dcubic2  26821  dcubic1  26822  dcubic  26823  mcubic  26824  cubic2  26825  cubic  26826  binom4  26827  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem1  26834  quartlem2  26835  quartlem3  26836  quart  26838  asinlem  26845  asinlem2  26846  asinlem3a  26847  asinlem3  26848  asinf  26849  atandm2  26854  atanf  26857  asinneg  26863  efiasin  26865  sinasin  26866  asinsinlem  26868  asinsin  26869  asinbnd  26876  cosasin  26881  atanneg  26884  atancj  26887  efiatan  26889  atanlogaddlem  26890  atanlogadd  26891  atanlogsublem  26892  atanlogsub  26893  efiatan2  26894  2efiatan  26895  tanatan  26896  cosatan  26898  atantan  26900  atanbndlem  26902  atans2  26908  dvatan  26912  atantayl  26914  atantayl2  26915  leibpilem2  26918  efrlim  26946  efrlimOLD  26947  zetacvg  26992  ftalem7  27056  basellem3  27060  basellem7  27064  basellem8  27065  basellem9  27066  ppiub  27181  dchrmulcl  27226  bposlem9  27269  lgsdir  27309  lgsdilem2  27310  lgsdi  27311  lgsne0  27312  lgsquadlem1  27357  2sqlem2  27395  rpvmasum2  27489  dchrisum0lem1  27493  dchrisum0lem2  27495  mulogsumlem  27508  mulog2sumlem3  27513  log2sumbnd  27521  selberglem1  27522  selberglem2  27523  selberg2  27528  pntlemk  27583  colinearalglem1  28989  colinearalglem2  28990  ax5seglem1  29011  axcontlem2  29048  axcontlem8  29054  numclwwlk3lem1  30467  smcnlem  30783  ipval2  30793  4ipval2  30794  ipidsq  30796  dipcj  30800  cncph  30905  ipasslem2  30918  ipasslem4  30920  ipasslem9  30924  ipasslem11  30926  hhssnv  31350  spansncol  31654  homulass  31888  lnfnmuli  32130  riesz3i  32148  circum  35872  faclim  35944  mpomulnzcnf  36497  sin2h  37945  cos2h  37946  itg2addnclem3  38008  itgaddnc  38015  iblabsnc  38019  iblmulc2nc  38020  itgmulc2nc  38023  ftc1anclem3  38030  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  dvasin  38039  cntotbnd  38131  rmxluc  43382  rmyluc  43383  jm2.17a  43406  jm2.18  43434  jm3.1lem1  43463  jm3.1lem2  43464  proot1ex  43642  lhe4.4ex1a  44774  expgrowthi  44778  expgrowth  44780  binomcxplemnotnn0  44801  dvsinax  46359  dvasinbx  46366  dvcosax  46372  stoweidlem10  46456  wallispi2lem1  46517  wallispi2  46519  fouriersw  46677  sinnpoly  47351  m1modmmod  47824  dfodd6  48125  opoeALTV  48171  opeoALTV  48172  2zrngnmrid  48744  sinh-conventional  50226  amgmwlem  50289