Theorem mulcl 10623

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   · cmul 10544

This theorem was proved from axioms:  ax-mulcl 10601

This theorem is referenced by:  0cn  10635  mulid1  10641  mulcli  10650  mulcld  10663  mul31  10809  mul4  10810  mul02  10820  cnegex2  10824  muladd11r  10855  muladd  11074  subdi  11075  submul2  11082  mulsub  11085  recextlem1  11272  recex  11274  muleqadd  11286  mulnzcnopr  11288  mulcan1g  11295  divass  11318  divmulass  11323  divmuldiv  11342  divmuleq  11347  divadddiv  11357  conjmul  11359  cju  11636  zneo  12068  cnref1o  12387  modcyc2  13278  muladdmodid  13282  negmod  13287  modaddmulmod  13309  expcl  13450  expclzlem  13456  mulexp  13471  sqcl  13487  subsq  13575  subsq2  13576  binom2sub  13584  mulbinom2  13587  binom3  13588  zesq  13590  bernneq  13593  bernneq2  13594  mulsubdivbinom2  13625  bcval5  13681  reim  14470  imcl  14472  crre  14475  crim  14476  remim  14478  mulre  14482  cjreb  14484  recj  14485  reneg  14486  readd  14487  remullem  14489  remul2  14491  imcj  14493  imneg  14494  imadd  14495  immul2  14498  cjadd  14502  ipcnval  14504  cjmulrcl  14505  cjneg  14508  imval2  14512  cjreim  14521  rennim  14600  cnpart  14601  sqrtneg  14629  sqabsadd  14644  sqabssub  14645  absreimsq  14654  absreim  14655  absmul  14656  sqreulem  14721  sqreu  14722  mulcn2  14954  o1mul  14973  climmul  14991  iseraltlem2  15041  prodf  15245  clim2div  15247  prodfmul  15248  prodfn0  15252  prodfrec  15253  prodfdiv  15254  prodmolem3  15289  prodmolem2a  15290  fprodcl  15308  fprodclf  15348  risefaccl  15371  fallfaccl  15372  bpoly3  15414  fsumcube  15416  efexp  15456  sinf  15479  cosf  15480  tanval2  15488  tanval3  15489  resinval  15490  recosval  15491  efi4p  15492  resin4p  15493  recos4p  15494  resincl  15495  recoscl  15496  sinneg  15501  cosneg  15502  efival  15507  efmival  15508  sinhval  15509  coshval  15510  retanhcl  15514  tanhlt1  15515  tanhbnd  15516  efeul  15517  sinadd  15519  cosadd  15520  sinsub  15523  cossub  15524  subsin  15526  sinmul  15527  cosmul  15528  addcos  15529  subcos  15530  cos2tsin  15534  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  absef  15552  absefib  15553  efieq1re  15554  demoivre  15555  demoivreALT  15556  dvdscmulr  15640  dvdsmulcr  15641  odd2np1lem  15691  odd2np1  15692  opoe  15714  omoe  15715  opeo  15716  omeo  15717  gcdaddm  15875  modgcd  15882  bezoutlem1  15889  qredeq  16003  eulerthlem2  16121  modprm0  16144  pythagtriplem1  16155  pythagtriplem12  16165  pythagtriplem14  16167  iserodd  16174  gzmulcl  16276  4sqlem11  16293  4sqlem17  16299  cncrng  20568  cnfldmulg  20579  cnsubrg  20607  mulc1cncf  23515  icccvx  23556  pcorevlem  23632  cnlmod  23746  cnstrcvs  23747  cncvs  23751  itgcnlem  24392  itgneg  24406  itgconst  24421  itgadd  24427  iblabs  24431  itgmulc2  24436  dvmulbr  24538  dvmulf  24542  dvsincos  24580  plymullem1  24806  plymulcl  24813  plysubcl  24814  dgrcolem1  24865  dgrcolem2  24866  plydivlem4  24887  quotlem  24891  quotcl2  24893  quotdgr  24894  aaliou3lem3  24935  efper  25067  sinperlem  25068  sin2kpi  25071  cos2kpi  25072  efimpi  25079  sincosq1eq  25100  pige3ALT  25107  abssinper  25108  sinkpi  25109  coskpi  25110  sineq0  25111  coseq1  25112  tanregt0  25125  efif1olem4  25131  efifo  25133  eff1olem  25134  lognegb  25175  eflogeq  25187  efiarg  25192  tanarg  25204  logf1o2  25235  cxpcl  25259  cxpne0  25262  cxpsqrtlem  25287  cxpsqrt  25288  dvcxp1  25323  dvcncxp1  25326  root1eq1  25338  cxpeq  25340  relogbmul  25357  quad2  25419  quad  25420  dcubic2  25424  dcubic1  25425  dcubic  25426  mcubic  25427  cubic2  25428  cubic  25429  binom4  25430  dquartlem1  25431  dquartlem2  25432  dquart  25433  quart1cl  25434  quart1lem  25435  quart1  25436  quartlem1  25437  quartlem2  25438  quartlem3  25439  quart  25441  asinlem  25448  asinlem2  25449  asinlem3a  25450  asinlem3  25451  asinf  25452  atandm2  25457  atanf  25460  asinneg  25466  efiasin  25468  sinasin  25469  asinsinlem  25471  asinsin  25472  asinbnd  25479  cosasin  25484  atanneg  25487  atancj  25490  efiatan  25492  atanlogaddlem  25493  atanlogadd  25494  atanlogsublem  25495  atanlogsub  25496  efiatan2  25497  2efiatan  25498  tanatan  25499  cosatan  25501  atantan  25503  atanbndlem  25505  atans2  25511  dvatan  25515  atantayl  25517  atantayl2  25518  leibpilem2  25521  efrlim  25549  zetacvg  25594  ftalem7  25658  basellem3  25662  basellem7  25666  basellem8  25667  basellem9  25668  ppiub  25782  dchrmulcl  25827  bposlem9  25870  lgsdir  25910  lgsdilem2  25911  lgsdi  25912  lgsne0  25913  lgsquadlem1  25958  2sqlem2  25996  rpvmasum2  26090  dchrisum0lem1  26094  dchrisum0lem2  26096  mulogsumlem  26109  mulog2sumlem3  26114  log2sumbnd  26122  selberglem1  26123  selberglem2  26124  selberg2  26129  pntlemk  26184  colinearalglem1  26694  colinearalglem2  26695  ax5seglem1  26716  axcontlem2  26753  axcontlem8  26759  numclwwlk3lem1  28163  smcnlem  28476  ipval2  28486  4ipval2  28487  ipidsq  28489  dipcj  28493  cncph  28598  ipasslem2  28611  ipasslem4  28613  ipasslem9  28617  ipasslem11  28619  hhssnv  29043  spansncol  29347  homulass  29581  lnfnmuli  29823  riesz3i  29841  circum  32919  faclim  32980  sin2h  34884  cos2h  34885  itg2addnclem3  34947  itgaddnc  34954  iblabsnc  34958  iblmulc2nc  34959  itgmulc2nc  34962  ftc1anclem3  34971  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  dvasin  34980  cntotbnd  35076  fac2xp3  39101  rmxluc  39540  rmyluc  39541  jm2.17a  39564  jm2.18  39592  jm3.1lem1  39621  jm3.1lem2  39622  proot1ex  39808  lhe4.4ex1a  40668  expgrowthi  40672  expgrowth  40674  binomcxplemnotnn0  40695  dvsinax  42204  dvasinbx  42212  dvcosax  42218  stoweidlem10  42302  wallispi2lem1  42363  wallispi2  42365  fouriersw  42523  dfodd6  43809  opoeALTV  43855  opeoALTV  43856  2zrngnmrid  44228  m1modmmod  44588  sinh-conventional  44845  amgmwlem  44910