Theorem mulcl 11097

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

This theorem was proved from axioms:  ax-mulcl 11075

This theorem is referenced by:  mpomulf  11108  0cn  11111  mulrid  11117  mulcli  11126  mulcld  11139  mul31  11287  mul4  11288  mul02  11298  cnegex2  11302  muladd11r  11333  muladd  11556  subdi  11557  submul2  11564  mulsub  11567  recextlem1  11754  recex  11756  muleqadd  11768  mulnzcnf  11770  mulcan1g  11777  divass  11801  divmulass  11806  divmuldiv  11828  divmuleq  11833  divadddiv  11843  conjmul  11845  cju  12128  zneo  12562  cnref1o  12885  modcyc2  13813  muladdmodid  13819  negmod  13825  modaddmulmod  13847  expcl  13988  expclzlem  13992  mulexp  14010  sqcl  14027  subsq  14119  subsq2  14120  binom2sub  14129  mulbinom2  14132  binom3  14133  zesq  14135  bernneq  14138  bernneq2  14139  mulsubdivbinom2  14171  bcval5  14227  reim  15018  imcl  15020  crre  15023  crim  15024  remim  15026  mulre  15030  cjreb  15032  recj  15033  reneg  15034  readd  15035  remullem  15037  remul2  15039  imcj  15041  imneg  15042  imadd  15043  immul2  15046  cjadd  15050  ipcnval  15052  cjmulrcl  15053  cjneg  15056  imval2  15060  cjreim  15069  rennim  15148  cnpart  15149  sqrtneg  15176  sqabsadd  15191  sqabssub  15192  absreimsq  15201  absreim  15202  absmul  15203  sqreulem  15269  sqreu  15270  mulcn2  15505  o1mul  15524  climmul  15542  iseraltlem2  15592  prodf  15796  clim2div  15798  prodfmul  15799  prodfn0  15803  prodfrec  15804  prodfdiv  15805  prodmolem3  15842  prodmolem2a  15843  fprodcl  15861  fprodclf  15901  risefaccl  15924  fallfaccl  15925  bpoly3  15967  fsumcube  15969  efexp  16012  sinf  16035  cosf  16036  tanval2  16044  tanval3  16045  resinval  16046  recosval  16047  efi4p  16048  resin4p  16049  recos4p  16050  resincl  16051  recoscl  16052  sinneg  16057  cosneg  16058  efival  16063  efmival  16064  sinhval  16065  coshval  16066  retanhcl  16070  tanhlt1  16071  tanhbnd  16072  efeul  16073  sinadd  16075  cosadd  16076  sinsub  16079  cossub  16080  subsin  16082  sinmul  16083  cosmul  16084  addcos  16085  subcos  16086  cos2tsin  16090  ef01bndlem  16095  sin01bnd  16096  cos01bnd  16097  absef  16108  absefib  16109  efieq1re  16110  demoivre  16111  demoivreALT  16112  dvdscmulr  16197  dvdsmulcr  16198  odd2np1lem  16253  odd2np1  16254  opoe  16276  omoe  16277  opeo  16278  omeo  16279  gcdaddm  16438  modgcd  16445  bezoutlem1  16452  qredeq  16570  eulerthlem2  16695  modprm0  16719  pythagtriplem1  16730  pythagtriplem12  16740  pythagtriplem14  16742  iserodd  16749  gzmulcl  16852  4sqlem11  16869  4sqlem17  16875  cncrng  21327  cncrngOLD  21328  cnfldmulg  21342  cnsubrg  21366  mpomulcn  24786  mulc1cncf  24826  icccvx  24876  pcorevlem  24954  cnlmod  25068  cnstrcvs  25069  cncvs  25073  itgcnlem  25719  itgneg  25733  itgconst  25748  itgadd  25754  iblabs  25758  itgmulc2  25763  dvmulbr  25869  dvmulbrOLD  25870  dvmulf  25874  dvsincos  25913  plymullem1  26147  plymulcl  26154  plysubcl  26155  dgrcolem1  26207  dgrcolem2  26208  plydivlem4  26232  quotlem  26236  quotcl2  26238  quotdgr  26239  aaliou3lem3  26280  efper  26416  sinperlem  26417  sin2kpi  26420  cos2kpi  26421  efimpi  26428  sincosq1eq  26449  pige3ALT  26457  abssinper  26458  sinkpi  26459  coskpi  26460  sineq0  26461  coseq1  26462  tanregt0  26476  efif1olem4  26482  efifo  26484  eff1olem  26485  lognegb  26527  eflogeq  26539  efiarg  26544  tanarg  26556  logf1o2  26587  cxpcl  26611  cxpne0  26614  cxpsqrtlem  26639  cxpsqrt  26640  dvcxp1  26677  dvcncxp1  26680  root1eq1  26693  cxpeq  26695  relogbmul  26715  quad2  26777  quad  26778  dcubic2  26782  dcubic1  26783  dcubic  26784  mcubic  26785  cubic2  26786  cubic  26787  binom4  26788  dquartlem1  26789  dquartlem2  26790  dquart  26791  quart1cl  26792  quart1lem  26793  quart1  26794  quartlem1  26795  quartlem2  26796  quartlem3  26797  quart  26799  asinlem  26806  asinlem2  26807  asinlem3a  26808  asinlem3  26809  asinf  26810  atandm2  26815  atanf  26818  asinneg  26824  efiasin  26826  sinasin  26827  asinsinlem  26829  asinsin  26830  asinbnd  26837  cosasin  26842  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsublem  26853  atanlogsub  26854  efiatan2  26855  2efiatan  26856  tanatan  26857  cosatan  26859  atantan  26861  atanbndlem  26863  atans2  26869  dvatan  26873  atantayl  26875  atantayl2  26876  leibpilem2  26879  efrlim  26907  efrlimOLD  26908  zetacvg  26953  ftalem7  27017  basellem3  27021  basellem7  27025  basellem8  27026  basellem9  27027  ppiub  27143  dchrmulcl  27188  bposlem9  27231  lgsdir  27271  lgsdilem2  27272  lgsdi  27273  lgsne0  27274  lgsquadlem1  27319  2sqlem2  27357  rpvmasum2  27451  dchrisum0lem1  27455  dchrisum0lem2  27457  mulogsumlem  27470  mulog2sumlem3  27475  log2sumbnd  27483  selberglem1  27484  selberglem2  27485  selberg2  27490  pntlemk  27545  colinearalglem1  28886  colinearalglem2  28887  ax5seglem1  28908  axcontlem2  28945  axcontlem8  28951  numclwwlk3lem1  30364  smcnlem  30679  ipval2  30689  4ipval2  30690  ipidsq  30692  dipcj  30696  cncph  30801  ipasslem2  30814  ipasslem4  30816  ipasslem9  30820  ipasslem11  30822  hhssnv  31246  spansncol  31550  homulass  31784  lnfnmuli  32026  riesz3i  32044  circum  35739  faclim  35811  mpomulnzcnf  36364  sin2h  37671  cos2h  37672  itg2addnclem3  37734  itgaddnc  37741  iblabsnc  37745  iblmulc2nc  37746  itgmulc2nc  37749  ftc1anclem3  37756  ftc1anclem6  37759  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  dvasin  37765  cntotbnd  37857  rmxluc  43054  rmyluc  43055  jm2.17a  43078  jm2.18  43106  jm3.1lem1  43135  jm3.1lem2  43136  proot1ex  43314  lhe4.4ex1a  44447  expgrowthi  44451  expgrowth  44453  binomcxplemnotnn0  44474  dvsinax  46036  dvasinbx  46043  dvcosax  46049  stoweidlem10  46133  wallispi2lem1  46194  wallispi2  46196  fouriersw  46354  sinnpoly  47016  m1modmmod  47483  dfodd6  47762  opoeALTV  47808  opeoALTV  47809  2zrngnmrid  48381  sinh-conventional  49865  amgmwlem  49928