Theorem mulcl 11112

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

This theorem was proved from axioms:  ax-mulcl 11090

This theorem is referenced by:  mpomulf  11123  0cn  11126  mulrid  11132  mulcli  11141  mulcld  11154  mul31  11301  mul4  11302  mul02  11312  cnegex2  11316  muladd11r  11347  muladd  11570  subdi  11571  submul2  11578  mulsub  11581  recextlem1  11768  recex  11770  muleqadd  11782  mulnzcnf  11784  mulcan1g  11791  divass  11815  divmulass  11820  divmuldiv  11842  divmuleq  11847  divadddiv  11857  conjmul  11859  cju  12142  zneo  12577  cnref1o  12904  modcyc2  13829  muladdmodid  13835  negmod  13841  modaddmulmod  13863  expcl  14004  expclzlem  14008  mulexp  14026  sqcl  14043  subsq  14135  subsq2  14136  binom2sub  14145  mulbinom2  14148  binom3  14149  zesq  14151  bernneq  14154  bernneq2  14155  mulsubdivbinom2  14187  bcval5  14243  reim  15034  imcl  15036  crre  15039  crim  15040  remim  15042  mulre  15046  cjreb  15048  recj  15049  reneg  15050  readd  15051  remullem  15053  remul2  15055  imcj  15057  imneg  15058  imadd  15059  immul2  15062  cjadd  15066  ipcnval  15068  cjmulrcl  15069  cjneg  15072  imval2  15076  cjreim  15085  rennim  15164  cnpart  15165  sqrtneg  15192  sqabsadd  15207  sqabssub  15208  absreimsq  15217  absreim  15218  absmul  15219  sqreulem  15285  sqreu  15286  mulcn2  15521  o1mul  15540  climmul  15558  iseraltlem2  15608  prodf  15812  clim2div  15814  prodfmul  15815  prodfn0  15819  prodfrec  15820  prodfdiv  15821  prodmolem3  15858  prodmolem2a  15859  fprodcl  15877  fprodclf  15917  risefaccl  15940  fallfaccl  15941  bpoly3  15983  fsumcube  15985  efexp  16028  sinf  16051  cosf  16052  tanval2  16060  tanval3  16061  resinval  16062  recosval  16063  efi4p  16064  resin4p  16065  recos4p  16066  resincl  16067  recoscl  16068  sinneg  16073  cosneg  16074  efival  16079  efmival  16080  sinhval  16081  coshval  16082  retanhcl  16086  tanhlt1  16087  tanhbnd  16088  efeul  16089  sinadd  16091  cosadd  16092  sinsub  16095  cossub  16096  subsin  16098  sinmul  16099  cosmul  16100  addcos  16101  subcos  16102  cos2tsin  16106  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  absef  16124  absefib  16125  efieq1re  16126  demoivre  16127  demoivreALT  16128  dvdscmulr  16213  dvdsmulcr  16214  odd2np1lem  16269  odd2np1  16270  opoe  16292  omoe  16293  opeo  16294  omeo  16295  gcdaddm  16454  modgcd  16461  bezoutlem1  16468  qredeq  16586  eulerthlem2  16711  modprm0  16735  pythagtriplem1  16746  pythagtriplem12  16756  pythagtriplem14  16758  iserodd  16765  gzmulcl  16868  4sqlem11  16885  4sqlem17  16891  cncrng  21313  cncrngOLD  21314  cnfldmulg  21328  cnsubrg  21352  mpomulcn  24774  mulc1cncf  24814  icccvx  24864  pcorevlem  24942  cnlmod  25056  cnstrcvs  25057  cncvs  25061  itgcnlem  25707  itgneg  25721  itgconst  25736  itgadd  25742  iblabs  25746  itgmulc2  25751  dvmulbr  25857  dvmulbrOLD  25858  dvmulf  25862  dvsincos  25901  plymullem1  26135  plymulcl  26142  plysubcl  26143  dgrcolem1  26195  dgrcolem2  26196  plydivlem4  26220  quotlem  26224  quotcl2  26226  quotdgr  26227  aaliou3lem3  26268  efper  26404  sinperlem  26405  sin2kpi  26408  cos2kpi  26409  efimpi  26416  sincosq1eq  26437  pige3ALT  26445  abssinper  26446  sinkpi  26447  coskpi  26448  sineq0  26449  coseq1  26450  tanregt0  26464  efif1olem4  26470  efifo  26472  eff1olem  26473  lognegb  26515  eflogeq  26527  efiarg  26532  tanarg  26544  logf1o2  26575  cxpcl  26599  cxpne0  26602  cxpsqrtlem  26627  cxpsqrt  26628  dvcxp1  26665  dvcncxp1  26668  root1eq1  26681  cxpeq  26683  relogbmul  26703  quad2  26765  quad  26766  dcubic2  26770  dcubic1  26771  dcubic  26772  mcubic  26773  cubic2  26774  cubic  26775  binom4  26776  dquartlem1  26777  dquartlem2  26778  dquart  26779  quart1cl  26780  quart1lem  26781  quart1  26782  quartlem1  26783  quartlem2  26784  quartlem3  26785  quart  26787  asinlem  26794  asinlem2  26795  asinlem3a  26796  asinlem3  26797  asinf  26798  atandm2  26803  atanf  26806  asinneg  26812  efiasin  26814  sinasin  26815  asinsinlem  26817  asinsin  26818  asinbnd  26825  cosasin  26830  atanneg  26833  atancj  26836  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsublem  26841  atanlogsub  26842  efiatan2  26843  2efiatan  26844  tanatan  26845  cosatan  26847  atantan  26849  atanbndlem  26851  atans2  26857  dvatan  26861  atantayl  26863  atantayl2  26864  leibpilem2  26867  efrlim  26895  efrlimOLD  26896  zetacvg  26941  ftalem7  27005  basellem3  27009  basellem7  27013  basellem8  27014  basellem9  27015  ppiub  27131  dchrmulcl  27176  bposlem9  27219  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  lgsquadlem1  27307  2sqlem2  27345  rpvmasum2  27439  dchrisum0lem1  27443  dchrisum0lem2  27445  mulogsumlem  27458  mulog2sumlem3  27463  log2sumbnd  27471  selberglem1  27472  selberglem2  27473  selberg2  27478  pntlemk  27533  colinearalglem1  28869  colinearalglem2  28870  ax5seglem1  28891  axcontlem2  28928  axcontlem8  28934  numclwwlk3lem1  30344  smcnlem  30659  ipval2  30669  4ipval2  30670  ipidsq  30672  dipcj  30676  cncph  30781  ipasslem2  30794  ipasslem4  30796  ipasslem9  30800  ipasslem11  30802  hhssnv  31226  spansncol  31530  homulass  31764  lnfnmuli  32006  riesz3i  32024  circum  35646  faclim  35718  mpomulnzcnf  36272  sin2h  37589  cos2h  37590  itg2addnclem3  37652  itgaddnc  37659  iblabsnc  37663  iblmulc2nc  37664  itgmulc2nc  37667  ftc1anclem3  37674  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  dvasin  37683  cntotbnd  37775  rmxluc  42909  rmyluc  42910  jm2.17a  42933  jm2.18  42961  jm3.1lem1  42990  jm3.1lem2  42991  proot1ex  43169  lhe4.4ex1a  44302  expgrowthi  44306  expgrowth  44308  binomcxplemnotnn0  44329  dvsinax  45895  dvasinbx  45902  dvcosax  45908  stoweidlem10  45992  wallispi2lem1  46053  wallispi2  46055  fouriersw  46213  sinnpoly  46876  m1modmmod  47343  dfodd6  47622  opoeALTV  47668  opeoALTV  47669  2zrngnmrid  48241  sinh-conventional  49725  amgmwlem  49788