Theorem mulcl 10964

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

This theorem was proved from axioms:  ax-mulcl 10942

This theorem is referenced by:  0cn  10976  mulid1  10982  mulcli  10991  mulcld  11004  mul31  11151  mul4  11152  mul02  11162  cnegex2  11166  muladd11r  11197  muladd  11416  subdi  11417  submul2  11424  mulsub  11427  recextlem1  11614  recex  11616  muleqadd  11628  mulnzcnopr  11630  mulcan1g  11637  divass  11660  divmulass  11665  divmuldiv  11684  divmuleq  11689  divadddiv  11699  conjmul  11701  cju  11978  zneo  12412  cnref1o  12734  modcyc2  13636  muladdmodid  13640  negmod  13645  modaddmulmod  13667  expcl  13809  expclzlem  13815  mulexp  13831  sqcl  13847  subsq  13935  subsq2  13936  binom2sub  13944  mulbinom2  13947  binom3  13948  zesq  13950  bernneq  13953  bernneq2  13954  mulsubdivbinom2  13985  bcval5  14041  reim  14829  imcl  14831  crre  14834  crim  14835  remim  14837  mulre  14841  cjreb  14843  recj  14844  reneg  14845  readd  14846  remullem  14848  remul2  14850  imcj  14852  imneg  14853  imadd  14854  immul2  14857  cjadd  14861  ipcnval  14863  cjmulrcl  14864  cjneg  14867  imval2  14871  cjreim  14880  rennim  14959  cnpart  14960  sqrtneg  14988  sqabsadd  15003  sqabssub  15004  absreimsq  15013  absreim  15014  absmul  15015  sqreulem  15080  sqreu  15081  mulcn2  15314  o1mul  15333  climmul  15351  iseraltlem2  15403  prodf  15608  clim2div  15610  prodfmul  15611  prodfn0  15615  prodfrec  15616  prodfdiv  15617  prodmolem3  15652  prodmolem2a  15653  fprodcl  15671  fprodclf  15711  risefaccl  15734  fallfaccl  15735  bpoly3  15777  fsumcube  15779  efexp  15819  sinf  15842  cosf  15843  tanval2  15851  tanval3  15852  resinval  15853  recosval  15854  efi4p  15855  resin4p  15856  recos4p  15857  resincl  15858  recoscl  15859  sinneg  15864  cosneg  15865  efival  15870  efmival  15871  sinhval  15872  coshval  15873  retanhcl  15877  tanhlt1  15878  tanhbnd  15879  efeul  15880  sinadd  15882  cosadd  15883  sinsub  15886  cossub  15887  subsin  15889  sinmul  15890  cosmul  15891  addcos  15892  subcos  15893  cos2tsin  15897  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  absef  15915  absefib  15916  efieq1re  15917  demoivre  15918  demoivreALT  15919  dvdscmulr  16003  dvdsmulcr  16004  odd2np1lem  16058  odd2np1  16059  opoe  16081  omoe  16082  opeo  16083  omeo  16084  gcdaddm  16241  modgcd  16249  bezoutlem1  16256  qredeq  16371  eulerthlem2  16492  modprm0  16515  pythagtriplem1  16526  pythagtriplem12  16536  pythagtriplem14  16538  iserodd  16545  gzmulcl  16648  4sqlem11  16665  4sqlem17  16671  cncrng  20628  cnfldmulg  20639  cnsubrg  20667  mulc1cncf  24077  icccvx  24122  pcorevlem  24198  cnlmod  24312  cnstrcvs  24313  cncvs  24317  itgcnlem  24963  itgneg  24977  itgconst  24992  itgadd  24998  iblabs  25002  itgmulc2  25007  dvmulbr  25112  dvmulf  25116  dvsincos  25154  plymullem1  25384  plymulcl  25391  plysubcl  25392  dgrcolem1  25443  dgrcolem2  25444  plydivlem4  25465  quotlem  25469  quotcl2  25471  quotdgr  25472  aaliou3lem3  25513  efper  25645  sinperlem  25646  sin2kpi  25649  cos2kpi  25650  efimpi  25657  sincosq1eq  25678  pige3ALT  25685  abssinper  25686  sinkpi  25687  coskpi  25688  sineq0  25689  coseq1  25690  tanregt0  25704  efif1olem4  25710  efifo  25712  eff1olem  25713  lognegb  25754  eflogeq  25766  efiarg  25771  tanarg  25783  logf1o2  25814  cxpcl  25838  cxpne0  25841  cxpsqrtlem  25866  cxpsqrt  25867  dvcxp1  25902  dvcncxp1  25905  root1eq1  25917  cxpeq  25919  relogbmul  25936  quad2  25998  quad  25999  dcubic2  26003  dcubic1  26004  dcubic  26005  mcubic  26006  cubic2  26007  cubic  26008  binom4  26009  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem1  26016  quartlem2  26017  quartlem3  26018  quart  26020  asinlem  26027  asinlem2  26028  asinlem3a  26029  asinlem3  26030  asinf  26031  atandm2  26036  atanf  26039  asinneg  26045  efiasin  26047  sinasin  26048  asinsinlem  26050  asinsin  26051  asinbnd  26058  cosasin  26063  atanneg  26066  atancj  26069  efiatan  26071  atanlogaddlem  26072  atanlogadd  26073  atanlogsublem  26074  atanlogsub  26075  efiatan2  26076  2efiatan  26077  tanatan  26078  cosatan  26080  atantan  26082  atanbndlem  26084  atans2  26090  dvatan  26094  atantayl  26096  atantayl2  26097  leibpilem2  26100  efrlim  26128  zetacvg  26173  ftalem7  26237  basellem3  26241  basellem7  26245  basellem8  26246  basellem9  26247  ppiub  26361  dchrmulcl  26406  bposlem9  26449  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  lgsquadlem1  26537  2sqlem2  26575  rpvmasum2  26669  dchrisum0lem1  26673  dchrisum0lem2  26675  mulogsumlem  26688  mulog2sumlem3  26693  log2sumbnd  26701  selberglem1  26702  selberglem2  26703  selberg2  26708  pntlemk  26763  colinearalglem1  27283  colinearalglem2  27284  ax5seglem1  27305  axcontlem2  27342  axcontlem8  27348  numclwwlk3lem1  28755  smcnlem  29068  ipval2  29078  4ipval2  29079  ipidsq  29081  dipcj  29085  cncph  29190  ipasslem2  29203  ipasslem4  29205  ipasslem9  29209  ipasslem11  29211  hhssnv  29635  spansncol  29939  homulass  30173  lnfnmuli  30415  riesz3i  30433  circum  33641  faclim  33721  sin2h  35776  cos2h  35777  itg2addnclem3  35839  itgaddnc  35846  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nc  35854  ftc1anclem3  35861  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  dvasin  35870  cntotbnd  35963  fac2xp3  40167  rmxluc  40765  rmyluc  40766  jm2.17a  40789  jm2.18  40817  jm3.1lem1  40846  jm3.1lem2  40847  proot1ex  41033  lhe4.4ex1a  41954  expgrowthi  41958  expgrowth  41960  binomcxplemnotnn0  41981  dvsinax  43461  dvasinbx  43468  dvcosax  43474  stoweidlem10  43558  wallispi2lem1  43619  wallispi2  43621  fouriersw  43779  dfodd6  45100  opoeALTV  45146  opeoALTV  45147  2zrngnmrid  45519  m1modmmod  45878  sinh-conventional  46452  amgmwlem  46517