Theorem mulcl 11185

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

This theorem was proved from axioms:  ax-mulcl 11163

This theorem is referenced by:  mpomulf  11196  0cn  11199  mulrid  11207  mulcli  11217  mulcld  11230  mul31  11378  mul4  11379  mul02  11389  cnegex2  11393  muladd11r  11424  muladd  11647  subdi  11648  submul2  11655  mulsub  11658  recextlem1  11845  recex  11847  muleqadd  11859  mulnzcnf  11861  mulcan1g  11868  divass  11891  divmulass  11896  divmuldiv  11916  divmuleq  11921  divadddiv  11931  conjmul  11933  cju  12215  zneo  12680  cnref1o  13010  modcyc2  13942  muladdmodid  13948  negmod  13954  modaddmulmod  13976  expcl  14117  expclzlem  14121  mulexp  14139  sqcl  14156  subsq  14248  subsq2  14249  binom2sub  14258  mulbinom2  14261  binom3  14262  zesq  14264  bernneq  14267  bernneq2  14268  mulsubdivbinom2  14300  bcval5  14356  reim  15162  imcl  15164  crre  15167  crim  15168  remim  15170  mulre  15174  cjreb  15176  recj  15177  reneg  15178  readd  15179  remullem  15181  remul2  15183  imcj  15185  imneg  15186  imadd  15187  immul2  15190  cjadd  15194  ipcnval  15196  cjmulrcl  15197  cjneg  15200  imval2  15204  cjreim  15213  rennim  15292  cnpart  15293  sqrtneg  15320  sqabsadd  15335  sqabssub  15336  absreimsq  15345  absreim  15346  absmul  15347  sqreulem  15413  sqreu  15414  mulcn2  15649  o1mul  15668  climmul  15686  iseraltlem2  15736  prodf  15943  clim2div  15945  prodfmul  15946  prodfn0  15950  prodfrec  15951  prodfdiv  15952  prodmolem3  15989  prodmolem2a  15990  fprodcl  16008  fprodclf  16048  risefaccl  16071  fallfaccl  16072  bpoly3  16113  fsumcube  16115  efexp  16158  sinf  16181  cosf  16182  tanval2  16190  tanval3  16191  resinval  16192  recosval  16193  efi4p  16194  resin4p  16195  recos4p  16196  resincl  16197  recoscl  16198  sinneg  16203  cosneg  16204  efival  16209  efmival  16210  sinhval  16211  coshval  16212  retanhcl  16216  tanhlt1  16217  tanhbnd  16218  efeul  16219  sinadd  16221  cosadd  16222  sinsub  16225  cossub  16226  subsin  16228  sinmul  16229  cosmul  16230  addcos  16231  subcos  16232  cos2tsin  16236  ef01bndlem  16241  sin01bnd  16242  cos01bnd  16243  absef  16254  absefib  16255  efieq1re  16256  demoivre  16257  demoivreALT  16258  dvdscmulr  16343  dvdsmulcr  16344  odd2np1lem  16399  odd2np1  16400  opoe  16422  omoe  16423  opeo  16424  omeo  16425  gcdaddm  16584  modgcd  16591  bezoutlem1  16598  qredeq  16716  eulerthlem2  16842  modprm0  16866  pythagtriplem1  16877  pythagtriplem12  16887  pythagtriplem14  16889  iserodd  16896  gzmulcl  16999  4sqlem11  17016  4sqlem17  17022  cncrng  21524  cnfldmulg  21535  cnsubrg  21558  mpomulcn  25007  mulc1cncf  25045  icccvx  25090  pcorevlem  25166  cnlmod  25280  cnstrcvs  25281  cncvs  25285  itgcnlem  25930  itgneg  25944  itgconst  25959  itgadd  25965  iblabs  25969  itgmulc2  25974  dvmulbr  26079  dvmulf  26083  dvsincos  26121  plymullem1  26352  plymulcl  26359  plysubcl  26360  dgrcolem1  26411  dgrcolem2  26412  plydivlem4  26438  quotlem  26442  quotcl2  26444  quotdgr  26445  aaliou3lem3  26486  efper  26622  sinperlem  26623  sin2kpi  26626  cos2kpi  26627  efimpi  26634  sincosq1eq  26655  pige3ALT  26663  abssinper  26664  sinkpi  26665  coskpi  26666  sineq0  26667  coseq1  26668  tanregt0  26682  efif1olem4  26688  efifo  26690  eff1olem  26691  lognegb  26733  eflogeq  26745  efiarg  26750  tanarg  26762  logf1o2  26793  cxpcl  26817  cxpne0  26820  cxpsqrtlem  26845  cxpsqrt  26846  dvcxp1  26883  dvcncxp1  26886  root1eq1  26898  cxpeq  26900  relogbmul  26920  quad2  26982  quad  26983  dcubic2  26987  dcubic1  26988  dcubic  26989  mcubic  26990  cubic2  26991  cubic  26992  binom4  26993  dquartlem1  26994  dquartlem2  26995  dquart  26996  quart1cl  26997  quart1lem  26998  quart1  26999  quartlem1  27000  quartlem2  27001  quartlem3  27002  quart  27004  asinlem  27011  asinlem2  27012  asinlem3a  27013  asinlem3  27014  asinf  27015  atandm2  27020  atanf  27023  asinneg  27029  efiasin  27031  sinasin  27032  asinsinlem  27034  asinsin  27035  asinbnd  27042  cosasin  27047  atanneg  27050  atancj  27053  efiatan  27055  atanlogaddlem  27056  atanlogadd  27057  atanlogsublem  27058  atanlogsub  27059  efiatan2  27060  2efiatan  27061  tanatan  27062  cosatan  27064  atantan  27066  atanbndlem  27068  atans2  27074  dvatan  27078  atantayl  27080  atantayl2  27081  leibpilem2  27084  efrlim  27112  zetacvg  27157  ftalem7  27221  basellem3  27225  basellem7  27229  basellem8  27230  basellem9  27231  ppiub  27346  dchrmulcl  27391  bposlem9  27434  lgsdir  27474  lgsdilem2  27475  lgsdi  27476  lgsne0  27477  lgsquadlem1  27522  2sqlem2  27560  rpvmasum2  27654  dchrisum0lem1  27658  dchrisum0lem2  27660  mulogsumlem  27673  mulog2sumlem3  27678  log2sumbnd  27686  selberglem1  27687  selberglem2  27688  selberg2  27693  pntlemk  27748  colinearalglem1  29234  colinearalglem2  29235  ax5seglem1  29256  axcontlem2  29293  axcontlem8  29299  numclwwlk3lem1  30711  smcnlem  31027  ipval2  31037  4ipval2  31038  ipidsq  31040  dipcj  31044  cncph  31149  ipasslem2  31162  ipasslem4  31164  ipasslem9  31168  ipasslem11  31170  hhssnv  31594  spansncol  31898  homulass  32132  lnfnmuli  32374  riesz3i  32392  circum  36144  faclim  36216  mpomulnzcnf  36789  sin2h  38239  cos2h  38240  itg2addnclem3  38302  itgaddnc  38309  iblabsnc  38313  iblmulc2nc  38314  itgmulc2nc  38317  ftc1anclem3  38324  ftc1anclem6  38327  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  dvasin  38333  cntotbnd  38425  rmxluc  43643  rmyluc  43644  jm2.17a  43667  jm2.18  43695  jm3.1lem1  43724  jm3.1lem2  43725  proot1ex  43903  lhe4.4ex1a  45019  expgrowthi  45023  expgrowth  45025  binomcxplemnotnn0  45046  dvsinax  46607  dvasinbx  46614  dvcosax  46620  stoweidlem10  46704  wallispi2lem1  46765  wallispi2  46767  fouriersw  46925  sinnpoly  47605  m1modmmod  48078  dfodd6  48379  opoeALTV  48425  opeoALTV  48426  2zrngnmrid  48998  sinh-conventional  50494  amgmwlem  50579