Theorem mulcl 11110

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

This theorem was proved from axioms:  ax-mulcl 11088

This theorem is referenced by:  mpomulf  11121  0cn  11124  mulrid  11130  mulcli  11139  mulcld  11152  mul31  11300  mul4  11301  mul02  11311  cnegex2  11315  muladd11r  11346  muladd  11569  subdi  11570  submul2  11577  mulsub  11580  recextlem1  11767  recex  11769  muleqadd  11781  mulnzcnf  11783  mulcan1g  11790  divass  11814  divmulass  11819  divmuldiv  11841  divmuleq  11846  divadddiv  11856  conjmul  11858  cju  12141  zneo  12575  cnref1o  12898  modcyc2  13827  muladdmodid  13833  negmod  13839  modaddmulmod  13861  expcl  14002  expclzlem  14006  mulexp  14024  sqcl  14041  subsq  14133  subsq2  14134  binom2sub  14143  mulbinom2  14146  binom3  14147  zesq  14149  bernneq  14152  bernneq2  14153  mulsubdivbinom2  14185  bcval5  14241  reim  15032  imcl  15034  crre  15037  crim  15038  remim  15040  mulre  15044  cjreb  15046  recj  15047  reneg  15048  readd  15049  remullem  15051  remul2  15053  imcj  15055  imneg  15056  imadd  15057  immul2  15060  cjadd  15064  ipcnval  15066  cjmulrcl  15067  cjneg  15070  imval2  15074  cjreim  15083  rennim  15162  cnpart  15163  sqrtneg  15190  sqabsadd  15205  sqabssub  15206  absreimsq  15215  absreim  15216  absmul  15217  sqreulem  15283  sqreu  15284  mulcn2  15519  o1mul  15538  climmul  15556  iseraltlem2  15606  prodf  15810  clim2div  15812  prodfmul  15813  prodfn0  15817  prodfrec  15818  prodfdiv  15819  prodmolem3  15856  prodmolem2a  15857  fprodcl  15875  fprodclf  15915  risefaccl  15938  fallfaccl  15939  bpoly3  15981  fsumcube  15983  efexp  16026  sinf  16049  cosf  16050  tanval2  16058  tanval3  16059  resinval  16060  recosval  16061  efi4p  16062  resin4p  16063  recos4p  16064  resincl  16065  recoscl  16066  sinneg  16071  cosneg  16072  efival  16077  efmival  16078  sinhval  16079  coshval  16080  retanhcl  16084  tanhlt1  16085  tanhbnd  16086  efeul  16087  sinadd  16089  cosadd  16090  sinsub  16093  cossub  16094  subsin  16096  sinmul  16097  cosmul  16098  addcos  16099  subcos  16100  cos2tsin  16104  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  absef  16122  absefib  16123  efieq1re  16124  demoivre  16125  demoivreALT  16126  dvdscmulr  16211  dvdsmulcr  16212  odd2np1lem  16267  odd2np1  16268  opoe  16290  omoe  16291  opeo  16292  omeo  16293  gcdaddm  16452  modgcd  16459  bezoutlem1  16466  qredeq  16584  eulerthlem2  16709  modprm0  16733  pythagtriplem1  16744  pythagtriplem12  16754  pythagtriplem14  16756  iserodd  16763  gzmulcl  16866  4sqlem11  16883  4sqlem17  16889  cncrng  21343  cncrngOLD  21344  cnfldmulg  21358  cnsubrg  21382  mpomulcn  24814  mulc1cncf  24854  icccvx  24904  pcorevlem  24982  cnlmod  25096  cnstrcvs  25097  cncvs  25101  itgcnlem  25747  itgneg  25761  itgconst  25776  itgadd  25782  iblabs  25786  itgmulc2  25791  dvmulbr  25897  dvmulbrOLD  25898  dvmulf  25902  dvsincos  25941  plymullem1  26175  plymulcl  26182  plysubcl  26183  dgrcolem1  26235  dgrcolem2  26236  plydivlem4  26260  quotlem  26264  quotcl2  26266  quotdgr  26267  aaliou3lem3  26308  efper  26444  sinperlem  26445  sin2kpi  26448  cos2kpi  26449  efimpi  26456  sincosq1eq  26477  pige3ALT  26485  abssinper  26486  sinkpi  26487  coskpi  26488  sineq0  26489  coseq1  26490  tanregt0  26504  efif1olem4  26510  efifo  26512  eff1olem  26513  lognegb  26555  eflogeq  26567  efiarg  26572  tanarg  26584  logf1o2  26615  cxpcl  26639  cxpne0  26642  cxpsqrtlem  26667  cxpsqrt  26668  dvcxp1  26705  dvcncxp1  26708  root1eq1  26721  cxpeq  26723  relogbmul  26743  quad2  26805  quad  26806  dcubic2  26810  dcubic1  26811  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  binom4  26816  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  quartlem2  26824  quartlem3  26825  quart  26827  asinlem  26834  asinlem2  26835  asinlem3a  26836  asinlem3  26837  asinf  26838  atandm2  26843  atanf  26846  asinneg  26852  efiasin  26854  sinasin  26855  asinsinlem  26857  asinsin  26858  asinbnd  26865  cosasin  26870  atanneg  26873  atancj  26876  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsublem  26881  atanlogsub  26882  efiatan2  26883  2efiatan  26884  tanatan  26885  cosatan  26887  atantan  26889  atanbndlem  26891  atans2  26897  dvatan  26901  atantayl  26903  atantayl2  26904  leibpilem2  26907  efrlim  26935  efrlimOLD  26936  zetacvg  26981  ftalem7  27045  basellem3  27049  basellem7  27053  basellem8  27054  basellem9  27055  ppiub  27171  dchrmulcl  27216  bposlem9  27259  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  lgsquadlem1  27347  2sqlem2  27385  rpvmasum2  27479  dchrisum0lem1  27483  dchrisum0lem2  27485  mulogsumlem  27498  mulog2sumlem3  27503  log2sumbnd  27511  selberglem1  27512  selberglem2  27513  selberg2  27518  pntlemk  27573  colinearalglem1  28979  colinearalglem2  28980  ax5seglem1  29001  axcontlem2  29038  axcontlem8  29044  numclwwlk3lem1  30457  smcnlem  30772  ipval2  30782  4ipval2  30783  ipidsq  30785  dipcj  30789  cncph  30894  ipasslem2  30907  ipasslem4  30909  ipasslem9  30913  ipasslem11  30915  hhssnv  31339  spansncol  31643  homulass  31877  lnfnmuli  32119  riesz3i  32137  circum  35868  faclim  35940  mpomulnzcnf  36493  sin2h  37807  cos2h  37808  itg2addnclem3  37870  itgaddnc  37877  iblabsnc  37881  iblmulc2nc  37882  itgmulc2nc  37885  ftc1anclem3  37892  ftc1anclem6  37895  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  dvasin  37901  cntotbnd  37993  rmxluc  43174  rmyluc  43175  jm2.17a  43198  jm2.18  43226  jm3.1lem1  43255  jm3.1lem2  43256  proot1ex  43434  lhe4.4ex1a  44566  expgrowthi  44570  expgrowth  44572  binomcxplemnotnn0  44593  dvsinax  46153  dvasinbx  46160  dvcosax  46166  stoweidlem10  46250  wallispi2lem1  46311  wallispi2  46313  fouriersw  46471  sinnpoly  47133  m1modmmod  47600  dfodd6  47879  opoeALTV  47925  opeoALTV  47926  2zrngnmrid  48498  sinh-conventional  49980  amgmwlem  50043