Theorem mulcl 11198

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  (class class class)co 7413  ℂcc 11112   · cmul 11119

This theorem was proved from axioms:  ax-mulcl 11176

This theorem is referenced by:  mpomulf  11208  0cn  11212  mulrid  11218  mulcli  11227  mulcld  11240  mul31  11387  mul4  11388  mul02  11398  cnegex2  11402  muladd11r  11433  muladd  11652  subdi  11653  submul2  11660  mulsub  11663  recextlem1  11850  recex  11852  muleqadd  11864  mulnzcnopr  11866  mulcan1g  11873  divass  11896  divmulass  11901  divmuldiv  11920  divmuleq  11925  divadddiv  11935  conjmul  11937  cju  12214  zneo  12651  cnref1o  12975  modcyc2  13878  muladdmodid  13882  negmod  13887  modaddmulmod  13909  expcl  14051  expclzlem  14055  mulexp  14073  sqcl  14089  subsq  14180  subsq2  14181  binom2sub  14189  mulbinom2  14192  binom3  14193  zesq  14195  bernneq  14198  bernneq2  14199  mulsubdivbinom2  14228  bcval5  14284  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  15312  sqreu  15313  mulcn2  15546  o1mul  15565  climmul  15583  iseraltlem2  15635  prodf  15839  clim2div  15841  prodfmul  15842  prodfn0  15846  prodfrec  15847  prodfdiv  15848  prodmolem3  15883  prodmolem2a  15884  fprodcl  15902  fprodclf  15942  risefaccl  15965  fallfaccl  15966  bpoly3  16008  fsumcube  16010  efexp  16050  sinf  16073  cosf  16074  tanval2  16082  tanval3  16083  resinval  16084  recosval  16085  efi4p  16086  resin4p  16087  recos4p  16088  resincl  16089  recoscl  16090  sinneg  16095  cosneg  16096  efival  16101  efmival  16102  sinhval  16103  coshval  16104  retanhcl  16108  tanhlt1  16109  tanhbnd  16110  efeul  16111  sinadd  16113  cosadd  16114  sinsub  16117  cossub  16118  subsin  16120  sinmul  16121  cosmul  16122  addcos  16123  subcos  16124  cos2tsin  16128  ef01bndlem  16133  sin01bnd  16134  cos01bnd  16135  absef  16146  absefib  16147  efieq1re  16148  demoivre  16149  demoivreALT  16150  dvdscmulr  16234  dvdsmulcr  16235  odd2np1lem  16289  odd2np1  16290  opoe  16312  omoe  16313  opeo  16314  omeo  16315  gcdaddm  16472  modgcd  16480  bezoutlem1  16487  qredeq  16600  eulerthlem2  16721  modprm0  16744  pythagtriplem1  16755  pythagtriplem12  16765  pythagtriplem14  16767  iserodd  16774  gzmulcl  16877  4sqlem11  16894  4sqlem17  16900  cncrng  21168  cnfldmulg  21179  cnsubrg  21207  mpomulcn  24607  mulc1cncf  24647  icccvx  24697  pcorevlem  24775  cnlmod  24889  cnstrcvs  24890  cncvs  24894  itgcnlem  25541  itgneg  25555  itgconst  25570  itgadd  25576  iblabs  25580  itgmulc2  25585  dvmulbr  25690  dvmulf  25694  dvsincos  25732  plymullem1  25962  plymulcl  25969  plysubcl  25970  dgrcolem1  26021  dgrcolem2  26022  plydivlem4  26043  quotlem  26047  quotcl2  26049  quotdgr  26050  aaliou3lem3  26091  efper  26223  sinperlem  26224  sin2kpi  26227  cos2kpi  26228  efimpi  26235  sincosq1eq  26256  pige3ALT  26263  abssinper  26264  sinkpi  26265  coskpi  26266  sineq0  26267  coseq1  26268  tanregt0  26282  efif1olem4  26288  efifo  26290  eff1olem  26291  lognegb  26332  eflogeq  26344  efiarg  26349  tanarg  26361  logf1o2  26392  cxpcl  26416  cxpne0  26419  cxpsqrtlem  26444  cxpsqrt  26445  dvcxp1  26482  dvcncxp1  26485  root1eq1  26497  cxpeq  26499  relogbmul  26516  quad2  26578  quad  26579  dcubic2  26583  dcubic1  26584  dcubic  26585  mcubic  26586  cubic2  26587  cubic  26588  binom4  26589  dquartlem1  26590  dquartlem2  26591  dquart  26592  quart1cl  26593  quart1lem  26594  quart1  26595  quartlem1  26596  quartlem2  26597  quartlem3  26598  quart  26600  asinlem  26607  asinlem2  26608  asinlem3a  26609  asinlem3  26610  asinf  26611  atandm2  26616  atanf  26619  asinneg  26625  efiasin  26627  sinasin  26628  asinsinlem  26630  asinsin  26631  asinbnd  26638  cosasin  26643  atanneg  26646  atancj  26649  efiatan  26651  atanlogaddlem  26652  atanlogadd  26653  atanlogsublem  26654  atanlogsub  26655  efiatan2  26656  2efiatan  26657  tanatan  26658  cosatan  26660  atantan  26662  atanbndlem  26664  atans2  26670  dvatan  26674  atantayl  26676  atantayl2  26677  leibpilem2  26680  efrlim  26708  zetacvg  26753  ftalem7  26817  basellem3  26821  basellem7  26825  basellem8  26826  basellem9  26827  ppiub  26941  dchrmulcl  26986  bposlem9  27029  lgsdir  27069  lgsdilem2  27070  lgsdi  27071  lgsne0  27072  lgsquadlem1  27117  2sqlem2  27155  rpvmasum2  27249  dchrisum0lem1  27253  dchrisum0lem2  27255  mulogsumlem  27268  mulog2sumlem3  27273  log2sumbnd  27281  selberglem1  27282  selberglem2  27283  selberg2  27288  pntlemk  27343  colinearalglem1  28429  colinearalglem2  28430  ax5seglem1  28451  axcontlem2  28488  axcontlem8  28494  numclwwlk3lem1  29900  smcnlem  30215  ipval2  30225  4ipval2  30226  ipidsq  30228  dipcj  30232  cncph  30337  ipasslem2  30350  ipasslem4  30352  ipasslem9  30356  ipasslem11  30358  hhssnv  30782  spansncol  31086  homulass  31320  lnfnmuli  31562  riesz3i  31580  circum  34955  faclim  35018  gg-dvmulbr  35463  sin2h  36783  cos2h  36784  itg2addnclem3  36846  itgaddnc  36853  iblabsnc  36857  iblmulc2nc  36858  itgmulc2nc  36861  ftc1anclem3  36868  ftc1anclem6  36871  ftc1anclem7  36872  ftc1anclem8  36873  ftc1anc  36874  dvasin  36877  cntotbnd  36969  fac2xp3  41328  rmxluc  41979  rmyluc  41980  jm2.17a  42003  jm2.18  42031  jm3.1lem1  42060  jm3.1lem2  42061  proot1ex  42247  lhe4.4ex1a  43392  expgrowthi  43396  expgrowth  43398  binomcxplemnotnn0  43419  dvsinax  44929  dvasinbx  44936  dvcosax  44942  stoweidlem10  45026  wallispi2lem1  45087  wallispi2  45089  fouriersw  45247  dfodd6  46605  opoeALTV  46651  opeoALTV  46652  2zrngnmrid  46938  m1modmmod  47296  sinh-conventional  47873  amgmwlem  47938