Theorem mulcl 11152

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

This theorem was proved from axioms:  ax-mulcl 11130

This theorem is referenced by:  mpomulf  11163  0cn  11166  mulrid  11172  mulcli  11181  mulcld  11194  mul31  11341  mul4  11342  mul02  11352  cnegex2  11356  muladd11r  11387  muladd  11610  subdi  11611  submul2  11618  mulsub  11621  recextlem1  11808  recex  11810  muleqadd  11822  mulnzcnf  11824  mulcan1g  11831  divass  11855  divmulass  11860  divmuldiv  11882  divmuleq  11887  divadddiv  11897  conjmul  11899  cju  12182  zneo  12617  cnref1o  12944  modcyc2  13869  muladdmodid  13875  negmod  13881  modaddmulmod  13903  expcl  14044  expclzlem  14048  mulexp  14066  sqcl  14083  subsq  14175  subsq2  14176  binom2sub  14185  mulbinom2  14188  binom3  14189  zesq  14191  bernneq  14194  bernneq2  14195  mulsubdivbinom2  14227  bcval5  14283  reim  15075  imcl  15077  crre  15080  crim  15081  remim  15083  mulre  15087  cjreb  15089  recj  15090  reneg  15091  readd  15092  remullem  15094  remul2  15096  imcj  15098  imneg  15099  imadd  15100  immul2  15103  cjadd  15107  ipcnval  15109  cjmulrcl  15110  cjneg  15113  imval2  15117  cjreim  15126  rennim  15205  cnpart  15206  sqrtneg  15233  sqabsadd  15248  sqabssub  15249  absreimsq  15258  absreim  15259  absmul  15260  sqreulem  15326  sqreu  15327  mulcn2  15562  o1mul  15581  climmul  15599  iseraltlem2  15649  prodf  15853  clim2div  15855  prodfmul  15856  prodfn0  15860  prodfrec  15861  prodfdiv  15862  prodmolem3  15899  prodmolem2a  15900  fprodcl  15918  fprodclf  15958  risefaccl  15981  fallfaccl  15982  bpoly3  16024  fsumcube  16026  efexp  16069  sinf  16092  cosf  16093  tanval2  16101  tanval3  16102  resinval  16103  recosval  16104  efi4p  16105  resin4p  16106  recos4p  16107  resincl  16108  recoscl  16109  sinneg  16114  cosneg  16115  efival  16120  efmival  16121  sinhval  16122  coshval  16123  retanhcl  16127  tanhlt1  16128  tanhbnd  16129  efeul  16130  sinadd  16132  cosadd  16133  sinsub  16136  cossub  16137  subsin  16139  sinmul  16140  cosmul  16141  addcos  16142  subcos  16143  cos2tsin  16147  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  absef  16165  absefib  16166  efieq1re  16167  demoivre  16168  demoivreALT  16169  dvdscmulr  16254  dvdsmulcr  16255  odd2np1lem  16310  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  gcdaddm  16495  modgcd  16502  bezoutlem1  16509  qredeq  16627  eulerthlem2  16752  modprm0  16776  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem14  16799  iserodd  16806  gzmulcl  16909  4sqlem11  16926  4sqlem17  16932  cncrng  21300  cncrngOLD  21301  cnfldmulg  21315  cnsubrg  21344  mpomulcn  24758  mulc1cncf  24798  icccvx  24848  pcorevlem  24926  cnlmod  25040  cnstrcvs  25041  cncvs  25045  itgcnlem  25691  itgneg  25705  itgconst  25720  itgadd  25726  iblabs  25730  itgmulc2  25735  dvmulbr  25841  dvmulbrOLD  25842  dvmulf  25846  dvsincos  25885  plymullem1  26119  plymulcl  26126  plysubcl  26127  dgrcolem1  26179  dgrcolem2  26180  plydivlem4  26204  quotlem  26208  quotcl2  26210  quotdgr  26211  aaliou3lem3  26252  efper  26388  sinperlem  26389  sin2kpi  26392  cos2kpi  26393  efimpi  26400  sincosq1eq  26421  pige3ALT  26429  abssinper  26430  sinkpi  26431  coskpi  26432  sineq0  26433  coseq1  26434  tanregt0  26448  efif1olem4  26454  efifo  26456  eff1olem  26457  lognegb  26499  eflogeq  26511  efiarg  26516  tanarg  26528  logf1o2  26559  cxpcl  26583  cxpne0  26586  cxpsqrtlem  26611  cxpsqrt  26612  dvcxp1  26649  dvcncxp1  26652  root1eq1  26665  cxpeq  26667  relogbmul  26687  quad2  26749  quad  26750  dcubic2  26754  dcubic1  26755  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  binom4  26760  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  quartlem2  26768  quartlem3  26769  quart  26771  asinlem  26778  asinlem2  26779  asinlem3a  26780  asinlem3  26781  asinf  26782  atandm2  26787  atanf  26790  asinneg  26796  efiasin  26798  sinasin  26799  asinsinlem  26801  asinsin  26802  asinbnd  26809  cosasin  26814  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atanlogsub  26826  efiatan2  26827  2efiatan  26828  tanatan  26829  cosatan  26831  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl  26847  atantayl2  26848  leibpilem2  26851  efrlim  26879  efrlimOLD  26880  zetacvg  26925  ftalem7  26989  basellem3  26993  basellem7  26997  basellem8  26998  basellem9  26999  ppiub  27115  dchrmulcl  27160  bposlem9  27203  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  lgsquadlem1  27291  2sqlem2  27329  rpvmasum2  27423  dchrisum0lem1  27427  dchrisum0lem2  27429  mulogsumlem  27442  mulog2sumlem3  27447  log2sumbnd  27455  selberglem1  27456  selberglem2  27457  selberg2  27462  pntlemk  27517  colinearalglem1  28833  colinearalglem2  28834  ax5seglem1  28855  axcontlem2  28892  axcontlem8  28898  numclwwlk3lem1  30311  smcnlem  30626  ipval2  30636  4ipval2  30637  ipidsq  30639  dipcj  30643  cncph  30748  ipasslem2  30761  ipasslem4  30763  ipasslem9  30767  ipasslem11  30769  hhssnv  31193  spansncol  31497  homulass  31731  lnfnmuli  31973  riesz3i  31991  circum  35661  faclim  35733  mpomulnzcnf  36287  sin2h  37604  cos2h  37605  itg2addnclem3  37667  itgaddnc  37674  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nc  37682  ftc1anclem3  37689  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  dvasin  37698  cntotbnd  37790  rmxluc  42925  rmyluc  42926  jm2.17a  42949  jm2.18  42977  jm3.1lem1  43006  jm3.1lem2  43007  proot1ex  43185  lhe4.4ex1a  44318  expgrowthi  44322  expgrowth  44324  binomcxplemnotnn0  44345  dvsinax  45911  dvasinbx  45918  dvcosax  45924  stoweidlem10  46008  wallispi2lem1  46069  wallispi2  46071  fouriersw  46229  sinnpoly  46892  m1modmmod  47359  dfodd6  47638  opoeALTV  47684  opeoALTV  47685  2zrngnmrid  48244  sinh-conventional  49728  amgmwlem  49791