Theorem mulcl 10301

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2156  (class class class)co 6870  ℂcc 10215   · cmul 10222

This theorem was proved from axioms:  ax-mulcl 10279

This theorem is referenced by:  0cn  10313  mulid1  10319  mulcli  10328  mulcld  10341  mul31  10485  mul4  10486  mul02  10495  cnegex2  10499  muladd11r  10530  muladd  10743  subdi  10744  submul2  10751  mulsub  10754  recextlem1  10938  recex  10940  muleqadd  10952  mulnzcnopr  10954  mulcan1g  10961  divass  10984  divmulass  10989  divmuldiv  11006  divmuleq  11011  divadddiv  11021  conjmul  11023  cju  11297  zneo  11722  cnref1o  12037  modcyc2  12926  muladdmodid  12930  negmod  12935  modaddmulmod  12957  expcl  13097  expclzlem  13103  mulexp  13118  sqcl  13144  subsq  13191  subsq2  13192  binom2sub  13200  mulbinom2  13203  binom3  13204  zesq  13206  bernneq  13209  bernneq2  13210  mulsubdivbinom2  13265  bcval5  13321  reim  14068  imcl  14070  crre  14073  crim  14074  remim  14076  mulre  14080  cjreb  14082  recj  14083  reneg  14084  readd  14085  remullem  14087  remul2  14089  imcj  14091  imneg  14092  imadd  14093  immul2  14096  cjadd  14100  ipcnval  14102  cjmulrcl  14103  cjneg  14106  imval2  14110  cjreim  14119  rennim  14198  cnpart  14199  sqrtneg  14227  sqabsadd  14241  sqabssub  14242  absreimsq  14251  absreim  14252  absmul  14253  sqreulem  14318  sqreu  14319  mulcn2  14545  o1mul  14564  climmul  14582  iseraltlem2  14632  prodf  14836  clim2div  14838  prodfmul  14839  prodfn0  14843  prodfrec  14844  prodfdiv  14845  prodmolem3  14880  prodmolem2a  14881  fprodcl  14899  fprodclf  14939  risefaccl  14962  fallfaccl  14963  bpoly3  15005  fsumcube  15007  efexp  15047  sinf  15070  cosf  15071  tanval2  15079  tanval3  15080  resinval  15081  recosval  15082  efi4p  15083  resin4p  15084  recos4p  15085  resincl  15086  recoscl  15087  sinneg  15092  cosneg  15093  efival  15098  efmival  15099  sinhval  15100  coshval  15101  retanhcl  15105  tanhlt1  15106  tanhbnd  15107  efeul  15108  sinadd  15110  cosadd  15111  sinsub  15114  cossub  15115  subsin  15117  sinmul  15118  cosmul  15119  addcos  15120  subcos  15121  cos2tsin  15125  ef01bndlem  15130  sin01bnd  15131  cos01bnd  15132  absef  15143  absefib  15144  efieq1re  15145  demoivre  15146  demoivreALT  15147  dvdscmulr  15229  dvdsmulcr  15230  odd2np1lem  15280  odd2np1  15281  opoe  15303  omoe  15304  opeo  15305  omeo  15306  gcdaddm  15461  modgcd  15468  bezoutlem1  15471  qredeq  15585  eulerthlem2  15700  modprm0  15723  pythagtriplem1  15734  pythagtriplem12  15744  pythagtriplem14  15746  iserodd  15753  gzmulcl  15855  4sqlem11  15872  4sqlem17  15878  cncrng  19971  cnfldmulg  19982  cnsubrg  20010  mulc1cncf  22918  icccvx  22959  pcorevlem  23035  cnlmod  23149  cnstrcvs  23150  cncvs  23154  itgcnlem  23769  itgneg  23783  itgconst  23798  itgadd  23804  iblabs  23808  itgmulc2  23813  dvmulbr  23915  dvmulf  23919  dvsincos  23957  plymullem1  24183  plymulcl  24190  plysubcl  24191  dgrcolem1  24242  dgrcolem2  24243  plydivlem4  24264  quotlem  24268  quotcl2  24270  quotdgr  24271  aaliou3lem3  24312  efper  24445  sinperlem  24446  sin2kpi  24449  cos2kpi  24450  efimpi  24457  sincosq1eq  24478  pige3  24483  abssinper  24484  sinkpi  24485  coskpi  24486  sineq0  24487  coseq1  24488  tanregt0  24499  efif1olem4  24505  efifo  24507  eff1olem  24508  lognegb  24549  eflogeq  24561  efiarg  24566  tanarg  24578  logf1o2  24609  cxpcl  24633  cxpne0  24636  cxpsqrtlem  24661  cxpsqrt  24662  dvcxp1  24694  dvcncxp1  24697  root1eq1  24709  cxpeq  24711  relogbmul  24728  quad2  24779  quad  24780  dcubic2  24784  dcubic1  24785  dcubic  24786  mcubic  24787  cubic2  24788  cubic  24789  binom4  24790  dquartlem1  24791  dquartlem2  24792  dquart  24793  quart1cl  24794  quart1lem  24795  quart1  24796  quartlem1  24797  quartlem2  24798  quartlem3  24799  quart  24801  asinlem  24808  asinlem2  24809  asinlem3a  24810  asinlem3  24811  asinf  24812  atandm2  24817  atanf  24820  asinneg  24826  efiasin  24828  sinasin  24829  asinsinlem  24831  asinsin  24832  asinbnd  24839  cosasin  24844  atanneg  24847  atancj  24850  efiatan  24852  atanlogaddlem  24853  atanlogadd  24854  atanlogsublem  24855  atanlogsub  24856  efiatan2  24857  2efiatan  24858  tanatan  24859  cosatan  24861  atantan  24863  atanbndlem  24865  atans2  24871  dvatan  24875  atantayl  24877  atantayl2  24878  leibpilem1  24880  leibpilem2  24881  efrlim  24909  zetacvg  24954  ftalem7  25018  basellem3  25022  basellem7  25026  basellem8  25027  basellem9  25028  ppiub  25142  dchrmulcl  25187  bposlem9  25230  lgsdir  25270  lgsdilem2  25271  lgsdi  25272  lgsne0  25273  lgsquadlem1  25318  2sqlem2  25356  rpvmasum2  25414  dchrisum0lem1  25418  dchrisum0lem2  25420  mulogsumlem  25433  mulog2sumlem3  25438  log2sumbnd  25446  selberglem1  25447  selberglem2  25448  selberg2  25453  pntlemk  25508  colinearalglem1  25999  colinearalglem2  26000  ax5seglem1  26021  axcontlem2  26058  axcontlem8  26064  numclwwlk3lem1  27569  smcnlem  27879  ipval2  27889  4ipval2  27890  ipidsq  27892  dipcj  27896  cncph  28001  ipasslem2  28014  ipasslem4  28016  ipasslem9  28020  ipasslem11  28022  hhssnv  28448  spansncol  28754  homulass  28988  lnfnmuli  29230  riesz3i  29248  circum  31888  faclim  31952  sin2h  33710  cos2h  33711  itg2addnclem3  33773  itgaddnc  33780  iblabsnc  33784  iblmulc2nc  33785  itgmulc2nc  33788  ftc1anclem3  33797  ftc1anclem6  33800  ftc1anclem7  33801  ftc1anclem8  33802  ftc1anc  33803  dvasin  33806  cntotbnd  33904  rmxluc  37999  rmyluc  38000  jm2.17a  38025  jm2.18  38053  jm3.1lem1  38082  jm3.1lem2  38083  proot1ex  38277  lhe4.4ex1a  39025  expgrowthi  39029  expgrowth  39031  binomcxplemnotnn0  39052  dvsinax  40604  dvasinbx  40612  dvcosax  40618  stoweidlem10  40703  wallispi2lem1  40764  wallispi2  40766  fouriersw  40924  dfodd6  42122  opoeALTV  42166  opeoALTV  42167  2zrngnmrid  42515  m1modmmod  42881  sinh-conventional  43048  amgmwlem  43116