Theorem mulcl 10886

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

This theorem was proved from axioms:  ax-mulcl 10864

This theorem is referenced by:  0cn  10898  mulid1  10904  mulcli  10913  mulcld  10926  mul31  11072  mul4  11073  mul02  11083  cnegex2  11087  muladd11r  11118  muladd  11337  subdi  11338  submul2  11345  mulsub  11348  recextlem1  11535  recex  11537  muleqadd  11549  mulnzcnopr  11551  mulcan1g  11558  divass  11581  divmulass  11586  divmuldiv  11605  divmuleq  11610  divadddiv  11620  conjmul  11622  cju  11899  zneo  12333  cnref1o  12654  modcyc2  13555  muladdmodid  13559  negmod  13564  modaddmulmod  13586  expcl  13728  expclzlem  13734  mulexp  13750  sqcl  13766  subsq  13854  subsq2  13855  binom2sub  13863  mulbinom2  13866  binom3  13867  zesq  13869  bernneq  13872  bernneq2  13873  mulsubdivbinom2  13904  bcval5  13960  reim  14748  imcl  14750  crre  14753  crim  14754  remim  14756  mulre  14760  cjreb  14762  recj  14763  reneg  14764  readd  14765  remullem  14767  remul2  14769  imcj  14771  imneg  14772  imadd  14773  immul2  14776  cjadd  14780  ipcnval  14782  cjmulrcl  14783  cjneg  14786  imval2  14790  cjreim  14799  rennim  14878  cnpart  14879  sqrtneg  14907  sqabsadd  14922  sqabssub  14923  absreimsq  14932  absreim  14933  absmul  14934  sqreulem  14999  sqreu  15000  mulcn2  15233  o1mul  15252  climmul  15270  iseraltlem2  15322  prodf  15527  clim2div  15529  prodfmul  15530  prodfn0  15534  prodfrec  15535  prodfdiv  15536  prodmolem3  15571  prodmolem2a  15572  fprodcl  15590  fprodclf  15630  risefaccl  15653  fallfaccl  15654  bpoly3  15696  fsumcube  15698  efexp  15738  sinf  15761  cosf  15762  tanval2  15770  tanval3  15771  resinval  15772  recosval  15773  efi4p  15774  resin4p  15775  recos4p  15776  resincl  15777  recoscl  15778  sinneg  15783  cosneg  15784  efival  15789  efmival  15790  sinhval  15791  coshval  15792  retanhcl  15796  tanhlt1  15797  tanhbnd  15798  efeul  15799  sinadd  15801  cosadd  15802  sinsub  15805  cossub  15806  subsin  15808  sinmul  15809  cosmul  15810  addcos  15811  subcos  15812  cos2tsin  15816  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  absef  15834  absefib  15835  efieq1re  15836  demoivre  15837  demoivreALT  15838  dvdscmulr  15922  dvdsmulcr  15923  odd2np1lem  15977  odd2np1  15978  opoe  16000  omoe  16001  opeo  16002  omeo  16003  gcdaddm  16160  modgcd  16168  bezoutlem1  16175  qredeq  16290  eulerthlem2  16411  modprm0  16434  pythagtriplem1  16445  pythagtriplem12  16455  pythagtriplem14  16457  iserodd  16464  gzmulcl  16567  4sqlem11  16584  4sqlem17  16590  cncrng  20531  cnfldmulg  20542  cnsubrg  20570  mulc1cncf  23974  icccvx  24019  pcorevlem  24095  cnlmod  24209  cnstrcvs  24210  cncvs  24214  itgcnlem  24859  itgneg  24873  itgconst  24888  itgadd  24894  iblabs  24898  itgmulc2  24903  dvmulbr  25008  dvmulf  25012  dvsincos  25050  plymullem1  25280  plymulcl  25287  plysubcl  25288  dgrcolem1  25339  dgrcolem2  25340  plydivlem4  25361  quotlem  25365  quotcl2  25367  quotdgr  25368  aaliou3lem3  25409  efper  25541  sinperlem  25542  sin2kpi  25545  cos2kpi  25546  efimpi  25553  sincosq1eq  25574  pige3ALT  25581  abssinper  25582  sinkpi  25583  coskpi  25584  sineq0  25585  coseq1  25586  tanregt0  25600  efif1olem4  25606  efifo  25608  eff1olem  25609  lognegb  25650  eflogeq  25662  efiarg  25667  tanarg  25679  logf1o2  25710  cxpcl  25734  cxpne0  25737  cxpsqrtlem  25762  cxpsqrt  25763  dvcxp1  25798  dvcncxp1  25801  root1eq1  25813  cxpeq  25815  relogbmul  25832  quad2  25894  quad  25895  dcubic2  25899  dcubic1  25900  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  binom4  25905  dquartlem1  25906  dquartlem2  25907  dquart  25908  quart1cl  25909  quart1lem  25910  quart1  25911  quartlem1  25912  quartlem2  25913  quartlem3  25914  quart  25916  asinlem  25923  asinlem2  25924  asinlem3a  25925  asinlem3  25926  asinf  25927  atandm2  25932  atanf  25935  asinneg  25941  efiasin  25943  sinasin  25944  asinsinlem  25946  asinsin  25947  asinbnd  25954  cosasin  25959  atanneg  25962  atancj  25965  efiatan  25967  atanlogaddlem  25968  atanlogadd  25969  atanlogsublem  25970  atanlogsub  25971  efiatan2  25972  2efiatan  25973  tanatan  25974  cosatan  25976  atantan  25978  atanbndlem  25980  atans2  25986  dvatan  25990  atantayl  25992  atantayl2  25993  leibpilem2  25996  efrlim  26024  zetacvg  26069  ftalem7  26133  basellem3  26137  basellem7  26141  basellem8  26142  basellem9  26143  ppiub  26257  dchrmulcl  26302  bposlem9  26345  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  lgsquadlem1  26433  2sqlem2  26471  rpvmasum2  26565  dchrisum0lem1  26569  dchrisum0lem2  26571  mulogsumlem  26584  mulog2sumlem3  26589  log2sumbnd  26597  selberglem1  26598  selberglem2  26599  selberg2  26604  pntlemk  26659  colinearalglem1  27177  colinearalglem2  27178  ax5seglem1  27199  axcontlem2  27236  axcontlem8  27242  numclwwlk3lem1  28647  smcnlem  28960  ipval2  28970  4ipval2  28971  ipidsq  28973  dipcj  28977  cncph  29082  ipasslem2  29095  ipasslem4  29097  ipasslem9  29101  ipasslem11  29103  hhssnv  29527  spansncol  29831  homulass  30065  lnfnmuli  30307  riesz3i  30325  circum  33532  faclim  33618  sin2h  35694  cos2h  35695  itg2addnclem3  35757  itgaddnc  35764  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nc  35772  ftc1anclem3  35779  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  dvasin  35788  cntotbnd  35881  fac2xp3  40088  rmxluc  40674  rmyluc  40675  jm2.17a  40698  jm2.18  40726  jm3.1lem1  40755  jm3.1lem2  40756  proot1ex  40942  lhe4.4ex1a  41836  expgrowthi  41840  expgrowth  41842  binomcxplemnotnn0  41863  dvsinax  43344  dvasinbx  43351  dvcosax  43357  stoweidlem10  43441  wallispi2lem1  43502  wallispi2  43504  fouriersw  43662  dfodd6  44977  opoeALTV  45023  opeoALTV  45024  2zrngnmrid  45396  m1modmmod  45755  sinh-conventional  46327  amgmwlem  46392