Theorem mulcl 10778

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692   · cmul 10699

This theorem was proved from axioms:  ax-mulcl 10756

This theorem is referenced by:  0cn  10790  mulid1  10796  mulcli  10805  mulcld  10818  mul31  10964  mul4  10965  mul02  10975  cnegex2  10979  muladd11r  11010  muladd  11229  subdi  11230  submul2  11237  mulsub  11240  recextlem1  11427  recex  11429  muleqadd  11441  mulnzcnopr  11443  mulcan1g  11450  divass  11473  divmulass  11478  divmuldiv  11497  divmuleq  11502  divadddiv  11512  conjmul  11514  cju  11791  zneo  12225  cnref1o  12546  modcyc2  13445  muladdmodid  13449  negmod  13454  modaddmulmod  13476  expcl  13618  expclzlem  13624  mulexp  13639  sqcl  13655  subsq  13743  subsq2  13744  binom2sub  13752  mulbinom2  13755  binom3  13756  zesq  13758  bernneq  13761  bernneq2  13762  mulsubdivbinom2  13793  bcval5  13849  reim  14637  imcl  14639  crre  14642  crim  14643  remim  14645  mulre  14649  cjreb  14651  recj  14652  reneg  14653  readd  14654  remullem  14656  remul2  14658  imcj  14660  imneg  14661  imadd  14662  immul2  14665  cjadd  14669  ipcnval  14671  cjmulrcl  14672  cjneg  14675  imval2  14679  cjreim  14688  rennim  14767  cnpart  14768  sqrtneg  14796  sqabsadd  14811  sqabssub  14812  absreimsq  14821  absreim  14822  absmul  14823  sqreulem  14888  sqreu  14889  mulcn2  15122  o1mul  15141  climmul  15159  iseraltlem2  15211  prodf  15414  clim2div  15416  prodfmul  15417  prodfn0  15421  prodfrec  15422  prodfdiv  15423  prodmolem3  15458  prodmolem2a  15459  fprodcl  15477  fprodclf  15517  risefaccl  15540  fallfaccl  15541  bpoly3  15583  fsumcube  15585  efexp  15625  sinf  15648  cosf  15649  tanval2  15657  tanval3  15658  resinval  15659  recosval  15660  efi4p  15661  resin4p  15662  recos4p  15663  resincl  15664  recoscl  15665  sinneg  15670  cosneg  15671  efival  15676  efmival  15677  sinhval  15678  coshval  15679  retanhcl  15683  tanhlt1  15684  tanhbnd  15685  efeul  15686  sinadd  15688  cosadd  15689  sinsub  15692  cossub  15693  subsin  15695  sinmul  15696  cosmul  15697  addcos  15698  subcos  15699  cos2tsin  15703  ef01bndlem  15708  sin01bnd  15709  cos01bnd  15710  absef  15721  absefib  15722  efieq1re  15723  demoivre  15724  demoivreALT  15725  dvdscmulr  15809  dvdsmulcr  15810  odd2np1lem  15864  odd2np1  15865  opoe  15887  omoe  15888  opeo  15889  omeo  15890  gcdaddm  16047  modgcd  16055  bezoutlem1  16062  qredeq  16177  eulerthlem2  16298  modprm0  16321  pythagtriplem1  16332  pythagtriplem12  16342  pythagtriplem14  16344  iserodd  16351  gzmulcl  16454  4sqlem11  16471  4sqlem17  16477  cncrng  20338  cnfldmulg  20349  cnsubrg  20377  mulc1cncf  23756  icccvx  23801  pcorevlem  23877  cnlmod  23991  cnstrcvs  23992  cncvs  23996  itgcnlem  24641  itgneg  24655  itgconst  24670  itgadd  24676  iblabs  24680  itgmulc2  24685  dvmulbr  24790  dvmulf  24794  dvsincos  24832  plymullem1  25062  plymulcl  25069  plysubcl  25070  dgrcolem1  25121  dgrcolem2  25122  plydivlem4  25143  quotlem  25147  quotcl2  25149  quotdgr  25150  aaliou3lem3  25191  efper  25323  sinperlem  25324  sin2kpi  25327  cos2kpi  25328  efimpi  25335  sincosq1eq  25356  pige3ALT  25363  abssinper  25364  sinkpi  25365  coskpi  25366  sineq0  25367  coseq1  25368  tanregt0  25382  efif1olem4  25388  efifo  25390  eff1olem  25391  lognegb  25432  eflogeq  25444  efiarg  25449  tanarg  25461  logf1o2  25492  cxpcl  25516  cxpne0  25519  cxpsqrtlem  25544  cxpsqrt  25545  dvcxp1  25580  dvcncxp1  25583  root1eq1  25595  cxpeq  25597  relogbmul  25614  quad2  25676  quad  25677  dcubic2  25681  dcubic1  25682  dcubic  25683  mcubic  25684  cubic2  25685  cubic  25686  binom4  25687  dquartlem1  25688  dquartlem2  25689  dquart  25690  quart1cl  25691  quart1lem  25692  quart1  25693  quartlem1  25694  quartlem2  25695  quartlem3  25696  quart  25698  asinlem  25705  asinlem2  25706  asinlem3a  25707  asinlem3  25708  asinf  25709  atandm2  25714  atanf  25717  asinneg  25723  efiasin  25725  sinasin  25726  asinsinlem  25728  asinsin  25729  asinbnd  25736  cosasin  25741  atanneg  25744  atancj  25747  efiatan  25749  atanlogaddlem  25750  atanlogadd  25751  atanlogsublem  25752  atanlogsub  25753  efiatan2  25754  2efiatan  25755  tanatan  25756  cosatan  25758  atantan  25760  atanbndlem  25762  atans2  25768  dvatan  25772  atantayl  25774  atantayl2  25775  leibpilem2  25778  efrlim  25806  zetacvg  25851  ftalem7  25915  basellem3  25919  basellem7  25923  basellem8  25924  basellem9  25925  ppiub  26039  dchrmulcl  26084  bposlem9  26127  lgsdir  26167  lgsdilem2  26168  lgsdi  26169  lgsne0  26170  lgsquadlem1  26215  2sqlem2  26253  rpvmasum2  26347  dchrisum0lem1  26351  dchrisum0lem2  26353  mulogsumlem  26366  mulog2sumlem3  26371  log2sumbnd  26379  selberglem1  26380  selberglem2  26381  selberg2  26386  pntlemk  26441  colinearalglem1  26951  colinearalglem2  26952  ax5seglem1  26973  axcontlem2  27010  axcontlem8  27016  numclwwlk3lem1  28419  smcnlem  28732  ipval2  28742  4ipval2  28743  ipidsq  28745  dipcj  28749  cncph  28854  ipasslem2  28867  ipasslem4  28869  ipasslem9  28873  ipasslem11  28875  hhssnv  29299  spansncol  29603  homulass  29837  lnfnmuli  30079  riesz3i  30097  circum  33299  faclim  33381  sin2h  35453  cos2h  35454  itg2addnclem3  35516  itgaddnc  35523  iblabsnc  35527  iblmulc2nc  35528  itgmulc2nc  35531  ftc1anclem3  35538  ftc1anclem6  35541  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  dvasin  35547  cntotbnd  35640  fac2xp3  39823  rmxluc  40402  rmyluc  40403  jm2.17a  40426  jm2.18  40454  jm3.1lem1  40483  jm3.1lem2  40484  proot1ex  40670  lhe4.4ex1a  41561  expgrowthi  41565  expgrowth  41567  binomcxplemnotnn0  41588  dvsinax  43072  dvasinbx  43079  dvcosax  43085  stoweidlem10  43169  wallispi2lem1  43230  wallispi2  43232  fouriersw  43390  dfodd6  44705  opoeALTV  44751  opeoALTV  44752  2zrngnmrid  45124  m1modmmod  45483  sinh-conventional  46055  amgmwlem  46120