Theorem mulcl 11122

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mulcl 11100

This theorem is referenced by:  mpomulf  11133  0cn  11136  mulrid  11142  mulcli  11152  mulcld  11165  mul31  11313  mul4  11314  mul02  11324  cnegex2  11328  muladd11r  11359  muladd  11582  subdi  11583  submul2  11590  mulsub  11593  recextlem1  11780  recex  11782  muleqadd  11794  mulnzcnf  11796  mulcan1g  11803  divass  11827  divmulass  11832  divmuldiv  11855  divmuleq  11860  divadddiv  11870  conjmul  11872  cju  12155  zneo  12612  cnref1o  12935  modcyc2  13866  muladdmodid  13872  negmod  13878  modaddmulmod  13900  expcl  14041  expclzlem  14045  mulexp  14063  sqcl  14080  subsq  14172  subsq2  14173  binom2sub  14182  mulbinom2  14185  binom3  14186  zesq  14188  bernneq  14191  bernneq2  14192  mulsubdivbinom2  14224  bcval5  14280  reim  15071  imcl  15073  crre  15076  crim  15077  remim  15079  mulre  15083  cjreb  15085  recj  15086  reneg  15087  readd  15088  remullem  15090  remul2  15092  imcj  15094  imneg  15095  imadd  15096  immul2  15099  cjadd  15103  ipcnval  15105  cjmulrcl  15106  cjneg  15109  imval2  15113  cjreim  15122  rennim  15201  cnpart  15202  sqrtneg  15229  sqabsadd  15244  sqabssub  15245  absreimsq  15254  absreim  15255  absmul  15256  sqreulem  15322  sqreu  15323  mulcn2  15558  o1mul  15577  climmul  15595  iseraltlem2  15645  prodf  15852  clim2div  15854  prodfmul  15855  prodfn0  15859  prodfrec  15860  prodfdiv  15861  prodmolem3  15898  prodmolem2a  15899  fprodcl  15917  fprodclf  15957  risefaccl  15980  fallfaccl  15981  bpoly3  16023  fsumcube  16025  efexp  16068  sinf  16091  cosf  16092  tanval2  16100  tanval3  16101  resinval  16102  recosval  16103  efi4p  16104  resin4p  16105  recos4p  16106  resincl  16107  recoscl  16108  sinneg  16113  cosneg  16114  efival  16119  efmival  16120  sinhval  16121  coshval  16122  retanhcl  16126  tanhlt1  16127  tanhbnd  16128  efeul  16129  sinadd  16131  cosadd  16132  sinsub  16135  cossub  16136  subsin  16138  sinmul  16139  cosmul  16140  addcos  16141  subcos  16142  cos2tsin  16146  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  absef  16164  absefib  16165  efieq1re  16166  demoivre  16167  demoivreALT  16168  dvdscmulr  16253  dvdsmulcr  16254  odd2np1lem  16309  odd2np1  16310  opoe  16332  omoe  16333  opeo  16334  omeo  16335  gcdaddm  16494  modgcd  16501  bezoutlem1  16508  qredeq  16626  eulerthlem2  16752  modprm0  16776  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem14  16799  iserodd  16806  gzmulcl  16909  4sqlem11  16926  4sqlem17  16932  cncrng  21373  cnfldmulg  21384  cnsubrg  21407  mpomulcn  24834  mulc1cncf  24872  icccvx  24917  pcorevlem  24993  cnlmod  25107  cnstrcvs  25108  cncvs  25112  itgcnlem  25757  itgneg  25771  itgconst  25786  itgadd  25792  iblabs  25796  itgmulc2  25801  dvmulbr  25906  dvmulf  25910  dvsincos  25948  plymullem1  26179  plymulcl  26186  plysubcl  26187  dgrcolem1  26238  dgrcolem2  26239  plydivlem4  26262  quotlem  26266  quotcl2  26268  quotdgr  26269  aaliou3lem3  26310  efper  26443  sinperlem  26444  sin2kpi  26447  cos2kpi  26448  efimpi  26455  sincosq1eq  26476  pige3ALT  26484  abssinper  26485  sinkpi  26486  coskpi  26487  sineq0  26488  coseq1  26489  tanregt0  26503  efif1olem4  26509  efifo  26511  eff1olem  26512  lognegb  26554  eflogeq  26566  efiarg  26571  tanarg  26583  logf1o2  26614  cxpcl  26638  cxpne0  26641  cxpsqrtlem  26666  cxpsqrt  26667  dvcxp1  26704  dvcncxp1  26707  root1eq1  26719  cxpeq  26721  relogbmul  26741  quad2  26803  quad  26804  dcubic2  26808  dcubic1  26809  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  binom4  26814  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  quartlem2  26822  quartlem3  26823  quart  26825  asinlem  26832  asinlem2  26833  asinlem3a  26834  asinlem3  26835  asinf  26836  atandm2  26841  atanf  26844  asinneg  26850  efiasin  26852  sinasin  26853  asinsinlem  26855  asinsin  26856  asinbnd  26863  cosasin  26868  atanneg  26871  atancj  26874  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsublem  26879  atanlogsub  26880  efiatan2  26881  2efiatan  26882  tanatan  26883  cosatan  26885  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl  26901  atantayl2  26902  leibpilem2  26905  efrlim  26933  zetacvg  26978  ftalem7  27042  basellem3  27046  basellem7  27050  basellem8  27051  basellem9  27052  ppiub  27167  dchrmulcl  27212  bposlem9  27255  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  lgsquadlem1  27343  2sqlem2  27381  rpvmasum2  27475  dchrisum0lem1  27479  dchrisum0lem2  27481  mulogsumlem  27494  mulog2sumlem3  27499  log2sumbnd  27507  selberglem1  27508  selberglem2  27509  selberg2  27514  pntlemk  27569  colinearalglem1  28975  colinearalglem2  28976  ax5seglem1  28997  axcontlem2  29034  axcontlem8  29040  numclwwlk3lem1  30452  smcnlem  30768  ipval2  30778  4ipval2  30779  ipidsq  30781  dipcj  30785  cncph  30890  ipasslem2  30903  ipasslem4  30905  ipasslem9  30909  ipasslem11  30911  hhssnv  31335  spansncol  31639  homulass  31873  lnfnmuli  32115  riesz3i  32133  circum  35856  faclim  35928  mpomulnzcnf  36481  sin2h  37931  cos2h  37932  itg2addnclem3  37994  itgaddnc  38001  iblabsnc  38005  iblmulc2nc  38006  itgmulc2nc  38009  ftc1anclem3  38016  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  dvasin  38025  cntotbnd  38117  rmxluc  43364  rmyluc  43365  jm2.17a  43388  jm2.18  43416  jm3.1lem1  43445  jm3.1lem2  43446  proot1ex  43624  lhe4.4ex1a  44756  expgrowthi  44760  expgrowth  44762  binomcxplemnotnn0  44783  dvsinax  46341  dvasinbx  46348  dvcosax  46354  stoweidlem10  46438  wallispi2lem1  46499  wallispi2  46501  fouriersw  46659  sinnpoly  47339  m1modmmod  47812  dfodd6  48113  opoeALTV  48159  opeoALTV  48160  2zrngnmrid  48732  sinh-conventional  50214  amgmwlem  50277