Theorem mulcl 11057

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  (class class class)co 7338  ℂcc 10971   · cmul 10978

This theorem was proved from axioms:  ax-mulcl 11035

This theorem is referenced by:  0cn  11069  mulid1  11075  mulcli  11084  mulcld  11097  mul31  11244  mul4  11245  mul02  11255  cnegex2  11259  muladd11r  11290  muladd  11509  subdi  11510  submul2  11517  mulsub  11520  recextlem1  11707  recex  11709  muleqadd  11721  mulnzcnopr  11723  mulcan1g  11730  divass  11753  divmulass  11758  divmuldiv  11777  divmuleq  11782  divadddiv  11792  conjmul  11794  cju  12071  zneo  12505  cnref1o  12827  modcyc2  13729  muladdmodid  13733  negmod  13738  modaddmulmod  13760  expcl  13902  expclzlem  13908  mulexp  13924  sqcl  13940  subsq  14028  subsq2  14029  binom2sub  14037  mulbinom2  14040  binom3  14041  zesq  14043  bernneq  14046  bernneq2  14047  mulsubdivbinom2  14078  bcval5  14134  reim  14920  imcl  14922  crre  14925  crim  14926  remim  14928  mulre  14932  cjreb  14934  recj  14935  reneg  14936  readd  14937  remullem  14939  remul2  14941  imcj  14943  imneg  14944  imadd  14945  immul2  14948  cjadd  14952  ipcnval  14954  cjmulrcl  14955  cjneg  14958  imval2  14962  cjreim  14971  rennim  15050  cnpart  15051  sqrtneg  15079  sqabsadd  15094  sqabssub  15095  absreimsq  15104  absreim  15105  absmul  15106  sqreulem  15171  sqreu  15172  mulcn2  15405  o1mul  15424  climmul  15442  iseraltlem2  15494  prodf  15699  clim2div  15701  prodfmul  15702  prodfn0  15706  prodfrec  15707  prodfdiv  15708  prodmolem3  15743  prodmolem2a  15744  fprodcl  15762  fprodclf  15802  risefaccl  15825  fallfaccl  15826  bpoly3  15868  fsumcube  15870  efexp  15910  sinf  15933  cosf  15934  tanval2  15942  tanval3  15943  resinval  15944  recosval  15945  efi4p  15946  resin4p  15947  recos4p  15948  resincl  15949  recoscl  15950  sinneg  15955  cosneg  15956  efival  15961  efmival  15962  sinhval  15963  coshval  15964  retanhcl  15968  tanhlt1  15969  tanhbnd  15970  efeul  15971  sinadd  15973  cosadd  15974  sinsub  15977  cossub  15978  subsin  15980  sinmul  15981  cosmul  15982  addcos  15983  subcos  15984  cos2tsin  15988  ef01bndlem  15993  sin01bnd  15994  cos01bnd  15995  absef  16006  absefib  16007  efieq1re  16008  demoivre  16009  demoivreALT  16010  dvdscmulr  16094  dvdsmulcr  16095  odd2np1lem  16149  odd2np1  16150  opoe  16172  omoe  16173  opeo  16174  omeo  16175  gcdaddm  16332  modgcd  16340  bezoutlem1  16347  qredeq  16460  eulerthlem2  16581  modprm0  16604  pythagtriplem1  16615  pythagtriplem12  16625  pythagtriplem14  16627  iserodd  16634  gzmulcl  16737  4sqlem11  16754  4sqlem17  16760  cncrng  20726  cnfldmulg  20737  cnsubrg  20765  mulc1cncf  24175  icccvx  24220  pcorevlem  24296  cnlmod  24410  cnstrcvs  24411  cncvs  24415  itgcnlem  25061  itgneg  25075  itgconst  25090  itgadd  25096  iblabs  25100  itgmulc2  25105  dvmulbr  25210  dvmulf  25214  dvsincos  25252  plymullem1  25482  plymulcl  25489  plysubcl  25490  dgrcolem1  25541  dgrcolem2  25542  plydivlem4  25563  quotlem  25567  quotcl2  25569  quotdgr  25570  aaliou3lem3  25611  efper  25743  sinperlem  25744  sin2kpi  25747  cos2kpi  25748  efimpi  25755  sincosq1eq  25776  pige3ALT  25783  abssinper  25784  sinkpi  25785  coskpi  25786  sineq0  25787  coseq1  25788  tanregt0  25802  efif1olem4  25808  efifo  25810  eff1olem  25811  lognegb  25852  eflogeq  25864  efiarg  25869  tanarg  25881  logf1o2  25912  cxpcl  25936  cxpne0  25939  cxpsqrtlem  25964  cxpsqrt  25965  dvcxp1  26000  dvcncxp1  26003  root1eq1  26015  cxpeq  26017  relogbmul  26034  quad2  26096  quad  26097  dcubic2  26101  dcubic1  26102  dcubic  26103  mcubic  26104  cubic2  26105  cubic  26106  binom4  26107  dquartlem1  26108  dquartlem2  26109  dquart  26110  quart1cl  26111  quart1lem  26112  quart1  26113  quartlem1  26114  quartlem2  26115  quartlem3  26116  quart  26118  asinlem  26125  asinlem2  26126  asinlem3a  26127  asinlem3  26128  asinf  26129  atandm2  26134  atanf  26137  asinneg  26143  efiasin  26145  sinasin  26146  asinsinlem  26148  asinsin  26149  asinbnd  26156  cosasin  26161  atanneg  26164  atancj  26167  efiatan  26169  atanlogaddlem  26170  atanlogadd  26171  atanlogsublem  26172  atanlogsub  26173  efiatan2  26174  2efiatan  26175  tanatan  26176  cosatan  26178  atantan  26180  atanbndlem  26182  atans2  26188  dvatan  26192  atantayl  26194  atantayl2  26195  leibpilem2  26198  efrlim  26226  zetacvg  26271  ftalem7  26335  basellem3  26339  basellem7  26343  basellem8  26344  basellem9  26345  ppiub  26459  dchrmulcl  26504  bposlem9  26547  lgsdir  26587  lgsdilem2  26588  lgsdi  26589  lgsne0  26590  lgsquadlem1  26635  2sqlem2  26673  rpvmasum2  26767  dchrisum0lem1  26771  dchrisum0lem2  26773  mulogsumlem  26786  mulog2sumlem3  26791  log2sumbnd  26799  selberglem1  26800  selberglem2  26801  selberg2  26806  pntlemk  26861  colinearalglem1  27564  colinearalglem2  27565  ax5seglem1  27586  axcontlem2  27623  axcontlem8  27629  numclwwlk3lem1  29035  smcnlem  29348  ipval2  29358  4ipval2  29359  ipidsq  29361  dipcj  29365  cncph  29470  ipasslem2  29483  ipasslem4  29485  ipasslem9  29489  ipasslem11  29491  hhssnv  29915  spansncol  30219  homulass  30453  lnfnmuli  30695  riesz3i  30713  circum  33931  faclim  34004  sin2h  35923  cos2h  35924  itg2addnclem3  35986  itgaddnc  35993  iblabsnc  35997  iblmulc2nc  35998  itgmulc2nc  36001  ftc1anclem3  36008  ftc1anclem6  36011  ftc1anclem7  36012  ftc1anclem8  36013  ftc1anc  36014  dvasin  36017  cntotbnd  36110  fac2xp3  40468  rmxluc  41072  rmyluc  41073  jm2.17a  41096  jm2.18  41124  jm3.1lem1  41153  jm3.1lem2  41154  proot1ex  41340  lhe4.4ex1a  42320  expgrowthi  42324  expgrowth  42326  binomcxplemnotnn0  42347  dvsinax  43842  dvasinbx  43849  dvcosax  43855  stoweidlem10  43939  wallispi2lem1  44000  wallispi2  44002  fouriersw  44160  dfodd6  45507  opoeALTV  45553  opeoALTV  45554  2zrngnmrid  45926  m1modmmod  46285  sinh-conventional  46859  amgmwlem  46924