Theorem mulcl 10621

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

This theorem was proved from axioms:  ax-mulcl 10599

This theorem is referenced by:  0cn  10633  mulid1  10639  mulcli  10648  mulcld  10661  mul31  10807  mul4  10808  mul02  10818  cnegex2  10822  muladd11r  10853  muladd  11072  subdi  11073  submul2  11080  mulsub  11083  recextlem1  11270  recex  11272  muleqadd  11284  mulnzcnopr  11286  mulcan1g  11293  divass  11316  divmulass  11321  divmuldiv  11340  divmuleq  11345  divadddiv  11355  conjmul  11357  cju  11634  zneo  12066  cnref1o  12385  modcyc2  13276  muladdmodid  13280  negmod  13285  modaddmulmod  13307  expcl  13448  expclzlem  13454  mulexp  13469  sqcl  13485  subsq  13573  subsq2  13574  binom2sub  13582  mulbinom2  13585  binom3  13586  zesq  13588  bernneq  13591  bernneq2  13592  mulsubdivbinom2  13623  bcval5  13679  reim  14468  imcl  14470  crre  14473  crim  14474  remim  14476  mulre  14480  cjreb  14482  recj  14483  reneg  14484  readd  14485  remullem  14487  remul2  14489  imcj  14491  imneg  14492  imadd  14493  immul2  14496  cjadd  14500  ipcnval  14502  cjmulrcl  14503  cjneg  14506  imval2  14510  cjreim  14519  rennim  14598  cnpart  14599  sqrtneg  14627  sqabsadd  14642  sqabssub  14643  absreimsq  14652  absreim  14653  absmul  14654  sqreulem  14719  sqreu  14720  mulcn2  14952  o1mul  14971  climmul  14989  iseraltlem2  15039  prodf  15243  clim2div  15245  prodfmul  15246  prodfn0  15250  prodfrec  15251  prodfdiv  15252  prodmolem3  15287  prodmolem2a  15288  fprodcl  15306  fprodclf  15346  risefaccl  15369  fallfaccl  15370  bpoly3  15412  fsumcube  15414  efexp  15454  sinf  15477  cosf  15478  tanval2  15486  tanval3  15487  resinval  15488  recosval  15489  efi4p  15490  resin4p  15491  recos4p  15492  resincl  15493  recoscl  15494  sinneg  15499  cosneg  15500  efival  15505  efmival  15506  sinhval  15507  coshval  15508  retanhcl  15512  tanhlt1  15513  tanhbnd  15514  efeul  15515  sinadd  15517  cosadd  15518  sinsub  15521  cossub  15522  subsin  15524  sinmul  15525  cosmul  15526  addcos  15527  subcos  15528  cos2tsin  15532  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  absef  15550  absefib  15551  efieq1re  15552  demoivre  15553  demoivreALT  15554  dvdscmulr  15638  dvdsmulcr  15639  odd2np1lem  15689  odd2np1  15690  opoe  15712  omoe  15713  opeo  15714  omeo  15715  gcdaddm  15873  modgcd  15880  bezoutlem1  15887  qredeq  16001  eulerthlem2  16119  modprm0  16142  pythagtriplem1  16153  pythagtriplem12  16163  pythagtriplem14  16165  iserodd  16172  gzmulcl  16274  4sqlem11  16291  4sqlem17  16297  cncrng  20566  cnfldmulg  20577  cnsubrg  20605  mulc1cncf  23513  icccvx  23554  pcorevlem  23630  cnlmod  23744  cnstrcvs  23745  cncvs  23749  itgcnlem  24390  itgneg  24404  itgconst  24419  itgadd  24425  iblabs  24429  itgmulc2  24434  dvmulbr  24536  dvmulf  24540  dvsincos  24578  plymullem1  24804  plymulcl  24811  plysubcl  24812  dgrcolem1  24863  dgrcolem2  24864  plydivlem4  24885  quotlem  24889  quotcl2  24891  quotdgr  24892  aaliou3lem3  24933  efper  25065  sinperlem  25066  sin2kpi  25069  cos2kpi  25070  efimpi  25077  sincosq1eq  25098  pige3ALT  25105  abssinper  25106  sinkpi  25107  coskpi  25108  sineq0  25109  coseq1  25110  tanregt0  25123  efif1olem4  25129  efifo  25131  eff1olem  25132  lognegb  25173  eflogeq  25185  efiarg  25190  tanarg  25202  logf1o2  25233  cxpcl  25257  cxpne0  25260  cxpsqrtlem  25285  cxpsqrt  25286  dvcxp1  25321  dvcncxp1  25324  root1eq1  25336  cxpeq  25338  relogbmul  25355  quad2  25417  quad  25418  dcubic2  25422  dcubic1  25423  dcubic  25424  mcubic  25425  cubic2  25426  cubic  25427  binom4  25428  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem1  25435  quartlem2  25436  quartlem3  25437  quart  25439  asinlem  25446  asinlem2  25447  asinlem3a  25448  asinlem3  25449  asinf  25450  atandm2  25455  atanf  25458  asinneg  25464  efiasin  25466  sinasin  25467  asinsinlem  25469  asinsin  25470  asinbnd  25477  cosasin  25482  atanneg  25485  atancj  25488  efiatan  25490  atanlogaddlem  25491  atanlogadd  25492  atanlogsublem  25493  atanlogsub  25494  efiatan2  25495  2efiatan  25496  tanatan  25497  cosatan  25499  atantan  25501  atanbndlem  25503  atans2  25509  dvatan  25513  atantayl  25515  atantayl2  25516  leibpilem2  25519  efrlim  25547  zetacvg  25592  ftalem7  25656  basellem3  25660  basellem7  25664  basellem8  25665  basellem9  25666  ppiub  25780  dchrmulcl  25825  bposlem9  25868  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  lgsquadlem1  25956  2sqlem2  25994  rpvmasum2  26088  dchrisum0lem1  26092  dchrisum0lem2  26094  mulogsumlem  26107  mulog2sumlem3  26112  log2sumbnd  26120  selberglem1  26121  selberglem2  26122  selberg2  26127  pntlemk  26182  colinearalglem1  26692  colinearalglem2  26693  ax5seglem1  26714  axcontlem2  26751  axcontlem8  26757  numclwwlk3lem1  28161  smcnlem  28474  ipval2  28484  4ipval2  28485  ipidsq  28487  dipcj  28491  cncph  28596  ipasslem2  28609  ipasslem4  28611  ipasslem9  28615  ipasslem11  28617  hhssnv  29041  spansncol  29345  homulass  29579  lnfnmuli  29821  riesz3i  29839  circum  32917  faclim  32978  sin2h  34897  cos2h  34898  itg2addnclem3  34960  itgaddnc  34967  iblabsnc  34971  iblmulc2nc  34972  itgmulc2nc  34975  ftc1anclem3  34984  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  dvasin  34993  cntotbnd  35089  fac2xp3  39114  rmxluc  39553  rmyluc  39554  jm2.17a  39577  jm2.18  39605  jm3.1lem1  39634  jm3.1lem2  39635  proot1ex  39821  lhe4.4ex1a  40681  expgrowthi  40685  expgrowth  40687  binomcxplemnotnn0  40708  dvsinax  42217  dvasinbx  42225  dvcosax  42231  stoweidlem10  42315  wallispi2lem1  42376  wallispi2  42378  fouriersw  42536  dfodd6  43822  opoeALTV  43868  opeoALTV  43869  2zrngnmrid  44241  m1modmmod  44601  sinh-conventional  44858  amgmwlem  44923