Theorem mulcl 11172

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

This theorem was proved from axioms:  ax-mulcl 11150

This theorem is referenced by:  mpomulf  11183  0cn  11186  mulrid  11194  mulcli  11204  mulcld  11217  mul31  11365  mul4  11366  mul02  11376  cnegex2  11380  muladd11r  11411  muladd  11634  subdi  11635  submul2  11642  mulsub  11645  recextlem1  11832  recex  11834  muleqadd  11846  mulnzcnf  11848  mulcan1g  11855  divass  11878  divmulass  11883  divmuldiv  11906  divmuleq  11911  divadddiv  11921  conjmul  11923  cju  12205  zneo  12670  cnref1o  13000  modcyc2  13931  muladdmodid  13937  negmod  13943  modaddmulmod  13965  expcl  14106  expclzlem  14110  mulexp  14128  sqcl  14145  subsq  14237  subsq2  14238  binom2sub  14247  mulbinom2  14250  binom3  14251  zesq  14253  bernneq  14256  bernneq2  14257  mulsubdivbinom2  14289  bcval5  14345  reim  15150  imcl  15152  crre  15155  crim  15156  remim  15158  mulre  15162  cjreb  15164  recj  15165  reneg  15166  readd  15167  remullem  15169  remul2  15171  imcj  15173  imneg  15174  imadd  15175  immul2  15178  cjadd  15182  ipcnval  15184  cjmulrcl  15185  cjneg  15188  imval2  15192  cjreim  15201  rennim  15280  cnpart  15281  sqrtneg  15308  sqabsadd  15323  sqabssub  15324  absreimsq  15333  absreim  15334  absmul  15335  sqreulem  15401  sqreu  15402  mulcn2  15637  o1mul  15656  climmul  15674  iseraltlem2  15724  prodf  15931  clim2div  15933  prodfmul  15934  prodfn0  15938  prodfrec  15939  prodfdiv  15940  prodmolem3  15977  prodmolem2a  15978  fprodcl  15996  fprodclf  16036  risefaccl  16059  fallfaccl  16060  bpoly3  16102  fsumcube  16104  efexp  16147  sinf  16170  cosf  16171  tanval2  16179  tanval3  16180  resinval  16181  recosval  16182  efi4p  16183  resin4p  16184  recos4p  16185  resincl  16186  recoscl  16187  sinneg  16192  cosneg  16193  efival  16198  efmival  16199  sinhval  16200  coshval  16201  retanhcl  16205  tanhlt1  16206  tanhbnd  16207  efeul  16208  sinadd  16210  cosadd  16211  sinsub  16214  cossub  16215  subsin  16217  sinmul  16218  cosmul  16219  addcos  16220  subcos  16221  cos2tsin  16225  ef01bndlem  16230  sin01bnd  16231  cos01bnd  16232  absef  16243  absefib  16244  efieq1re  16245  demoivre  16246  demoivreALT  16247  dvdscmulr  16332  dvdsmulcr  16333  odd2np1lem  16388  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  gcdaddm  16573  modgcd  16580  bezoutlem1  16587  qredeq  16705  eulerthlem2  16831  modprm0  16855  pythagtriplem1  16866  pythagtriplem12  16876  pythagtriplem14  16878  iserodd  16885  gzmulcl  16988  4sqlem11  17005  4sqlem17  17011  cncrng  21503  cnfldmulg  21514  cnsubrg  21537  mpomulcn  24987  mulc1cncf  25025  icccvx  25070  pcorevlem  25146  cnlmod  25260  cnstrcvs  25261  cncvs  25265  itgcnlem  25910  itgneg  25924  itgconst  25939  itgadd  25945  iblabs  25949  itgmulc2  25954  dvmulbr  26059  dvmulf  26063  dvsincos  26101  plymullem1  26332  plymulcl  26339  plysubcl  26340  dgrcolem1  26391  dgrcolem2  26392  plydivlem4  26418  quotlem  26422  quotcl2  26424  quotdgr  26425  aaliou3lem3  26466  efper  26602  sinperlem  26603  sin2kpi  26606  cos2kpi  26607  efimpi  26614  sincosq1eq  26635  pige3ALT  26643  abssinper  26644  sinkpi  26645  coskpi  26646  sineq0  26647  coseq1  26648  tanregt0  26662  efif1olem4  26668  efifo  26670  eff1olem  26671  lognegb  26713  eflogeq  26725  efiarg  26730  tanarg  26742  logf1o2  26773  cxpcl  26797  cxpne0  26800  cxpsqrtlem  26825  cxpsqrt  26826  dvcxp1  26863  dvcncxp1  26866  root1eq1  26878  cxpeq  26880  relogbmul  26900  quad2  26962  quad  26963  dcubic2  26967  dcubic1  26968  dcubic  26969  mcubic  26970  cubic2  26971  cubic  26972  binom4  26973  dquartlem1  26974  dquartlem2  26975  dquart  26976  quart1cl  26977  quart1lem  26978  quart1  26979  quartlem1  26980  quartlem2  26981  quartlem3  26982  quart  26984  asinlem  26991  asinlem2  26992  asinlem3a  26993  asinlem3  26994  asinf  26995  atandm2  27000  atanf  27003  asinneg  27009  efiasin  27011  sinasin  27012  asinsinlem  27014  asinsin  27015  asinbnd  27022  cosasin  27027  atanneg  27030  atancj  27033  efiatan  27035  atanlogaddlem  27036  atanlogadd  27037  atanlogsublem  27038  atanlogsub  27039  efiatan2  27040  2efiatan  27041  tanatan  27042  cosatan  27044  atantan  27046  atanbndlem  27048  atans2  27054  dvatan  27058  atantayl  27060  atantayl2  27061  leibpilem2  27064  efrlim  27092  zetacvg  27137  ftalem7  27201  basellem3  27205  basellem7  27209  basellem8  27210  basellem9  27211  ppiub  27326  dchrmulcl  27371  bposlem9  27414  lgsdir  27454  lgsdilem2  27455  lgsdi  27456  lgsne0  27457  lgsquadlem1  27502  2sqlem2  27540  rpvmasum2  27634  dchrisum0lem1  27638  dchrisum0lem2  27640  mulogsumlem  27653  mulog2sumlem3  27658  log2sumbnd  27666  selberglem1  27667  selberglem2  27668  selberg2  27673  pntlemk  27728  colinearalglem1  29165  colinearalglem2  29166  ax5seglem1  29187  axcontlem2  29224  axcontlem8  29230  numclwwlk3lem1  30642  smcnlem  30958  ipval2  30968  4ipval2  30969  ipidsq  30971  dipcj  30975  cncph  31080  ipasslem2  31093  ipasslem4  31095  ipasslem9  31099  ipasslem11  31101  hhssnv  31525  spansncol  31829  homulass  32063  lnfnmuli  32305  riesz3i  32323  circum  36037  faclim  36109  mpomulnzcnf  36672  sin2h  38121  cos2h  38122  itg2addnclem3  38184  itgaddnc  38191  iblabsnc  38195  iblmulc2nc  38196  itgmulc2nc  38199  ftc1anclem3  38206  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  dvasin  38215  cntotbnd  38307  rmxluc  43525  rmyluc  43526  jm2.17a  43549  jm2.18  43577  jm3.1lem1  43606  jm3.1lem2  43607  proot1ex  43785  lhe4.4ex1a  44903  expgrowthi  44907  expgrowth  44909  binomcxplemnotnn0  44930  dvsinax  46485  dvasinbx  46492  dvcosax  46498  stoweidlem10  46582  wallispi2lem1  46643  wallispi2  46645  fouriersw  46803  sinnpoly  47483  m1modmmod  47956  dfodd6  48257  opoeALTV  48303  opeoALTV  48304  2zrngnmrid  48876  sinh-conventional  50368  amgmwlem  50431