Theorem mulcl 11311

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

Assertion

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

Proof of Theorem mulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

This proof depends on axioms:  ax-mulcl 11289

This theorem is used by:  mpomulf  11322  0cn  11325  mulrid  11333  mulcli  11343  mulcld  11356  mul31  11504  mul4  11505  mul02  11515  cnegex2  11519  muladd11r  11550  muladd  11775  subdi  11776  submul2  11783  mulsub  11786  recextlem1  11973  recex  11975  muleqadd  11987  mulnzcnf  11989  mulcan1g  11996  divass  12019  divmulass  12024  divmuldiv  12044  divmuleq  12049  divadddiv  12059  conjmul  12061  cju  12343  zneo  12809  cnref1o  13140  modcyc2  14074  muladdmodid  14080  negmod  14086  modaddmulmod  14108  expcl  14249  expclzlem  14253  mulexp  14271  sqcl  14288  subsq  14381  subsq2  14382  binom2sub  14391  mulbinom2  14394  binom3  14395  zesq  14397  bernneq  14400  bernneq2  14401  mulsubdivbinom2  14433  bcval5  14489  reim  15305  imcl  15307  crre  15310  crim  15311  remim  15313  mulre  15317  cjreb  15319  recj  15320  reneg  15321  readd  15322  remullem  15324  remul2  15326  imcj  15328  imneg  15329  imadd  15330  immul2  15333  cjadd  15337  ipcnval  15339  cjmulrcl  15340  cjneg  15343  imval2  15347  cjreim  15356  rennim  15435  cnpart  15436  sqrtneg  15463  sqabsadd  15478  sqabssub  15479  absreimsq  15488  absreim  15489  absmul  15490  sqreulem  15556  sqreu  15557  mulcn2  15792  o1mul  15811  climmul  15829  iseraltlem2  15879  prodf  16085  clim2div  16087  prodfmul  16088  prodfn0  16092  prodfrec  16093  prodfdiv  16094  prodmolem3  16129  prodmolem2a  16130  fprodcl  16148  fprodclf  16188  risefaccl  16211  fallfaccl  16212  bpoly3  16253  fsumcube  16255  efexp  16298  sinf  16321  cosf  16322  tanval2  16330  tanval3  16331  resinval  16332  recosval  16333  efi4p  16334  resin4p  16335  recos4p  16336  resincl  16337  recoscl  16338  sinneg  16343  cosneg  16344  efival  16349  efmival  16350  sinhval  16351  coshval  16352  retanhcl  16356  tanhlt1  16357  tanhbnd  16358  efeul  16359  sinadd  16361  cosadd  16362  sinsub  16365  cossub  16366  subsin  16368  sinmul  16369  cosmul  16370  addcos  16371  subcos  16372  cos2tsin  16376  ef01bndlem  16381  sin01bnd  16382  cos01bnd  16383  absef  16394  absefib  16395  efieq1re  16396  demoivre  16397  demoivreALT  16398  dvdscmulr  16483  dvdsmulcr  16484  odd2np1lem  16539  odd2np1  16540  opoe  16562  omoe  16563  opeo  16564  omeo  16565  gcdaddm  16726  modgcd  16734  bezoutlem1  16741  qredeq  16861  eulerthlem2  16988  modprm0  17012  pythagtriplem1  17023  pythagtriplem12  17033  pythagtriplem14  17035  iserodd  17042  gzmulcl  17145  4sqlem11  17162  4sqlem17  17168  cncrng  21729  cnfldmulg  21740  cnsubrg  21763  mpomulcn  25218  mulc1cncf  25256  icccvx  25301  pcorevlem  25377  cnlmod  25491  cnstrcvs  25492  cncvs  25496  itgcnlem  26140  itgneg  26154  itgconst  26169  itgadd  26175  iblabs  26179  itgmulc2  26184  dvmulbr  26289  dvmulf  26293  dvsincos  26331  plymullem1  26563  plymulcl  26570  plysubcl  26571  dgrcolem1  26622  dgrcolem2  26623  plydivlem4  26647  quotlem  26651  quotcl2  26653  quotdgr  26654  aaliou3lem3  26701  efper  26838  sinperlem  26839  sin2kpi  26842  cos2kpi  26843  efimpi  26850  sincosq1eq  26871  pige3ALT  26878  abssinper  26879  sinkpi  26880  coskpi  26881  sineq0  26882  coseq1  26883  tanregt0  26897  efif1olem4  26903  efifo  26905  eff1olem  26906  lognegb  26948  eflogeq  26960  efiarg  26965  tanarg  26977  logf1o2  27008  cxpcl  27032  cxpne0  27035  cxpsqrtlem  27060  cxpsqrt  27061  dvcxp1  27098  dvcncxp1  27101  root1eq1  27113  cxpeq  27115  relogbmul  27135  quad2  27197  quad  27198  dcubic2  27202  dcubic1  27203  dcubic  27204  mcubic  27205  cubic2  27206  cubic  27207  binom4  27208  dquartlem1  27209  dquartlem2  27210  dquart  27211  quart1cl  27212  quart1lem  27213  quart1  27214  quartlem1  27215  quartlem2  27216  quartlem3  27217  quart  27219  asinlem  27226  asinlem2  27227  asinlem3a  27228  asinlem3  27229  asinf  27230  atandm2  27235  atanf  27238  asinneg  27244  efiasin  27246  sinasin  27247  asinsinlem  27249  asinsin  27250  asinbnd  27257  cosasin  27262  atanneg  27265  atancj  27268  efiatan  27270  atanlogaddlem  27271  atanlogadd  27272  atanlogsublem  27273  atanlogsub  27274  efiatan2  27275  2efiatan  27276  tanatan  27277  cosatan  27279  atantan  27281  atanbndlem  27283  atans2  27289  dvatan  27293  atantayl  27295  atantayl2  27296  leibpilem2  27299  efrlim  27327  zetacvg  27372  ftalem7  27436  basellem3  27440  basellem7  27444  basellem8  27445  basellem9  27446  ppiub  27561  dchrmulcl  27606  bposlem9  27649  lgsdir  27689  lgsdilem2  27690  lgsdi  27691  lgsne0  27692  lgsquadlem1  27737  2sqlem2  27775  rpvmasum2  27869  dchrisum0lem1  27873  dchrisum0lem2  27875  mulogsumlem  27888  mulog2sumlem3  27893  log2sumbnd  27901  selberglem1  27902  selberglem2  27903  selberg2  27908  pntlemk  27963  colinearalglem1  29514  colinearalglem2  29515  ax5seglem1  29536  axcontlem2  29573  axcontlem8  29579  numclwwlk3lem1  31013  smcnlem  31329  ipval2  31339  4ipval2  31340  ipidsq  31342  dipcj  31346  cncph  31451  ipasslem2  31464  ipasslem4  31466  ipasslem9  31470  ipasslem11  31472  hhssnv  31896  spansncol  32200  homulass  32434  lnfnmuli  32676  riesz3i  32694  circum  36606  faclim  36689  mpomulnzcnf  37266  sin2h  38725  cos2h  38726  itg2addnclem3  38783  itgaddnc  38790  iblabsnc  38794  iblmulc2nc  38795  itgmulc2nc  38798  ftc1anclem3  38805  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  dvasin  38814  cntotbnd  38922  rmxluc  44136  rmyluc  44137  jm2.17a  44160  jm2.18  44188  jm3.1lem1  44217  jm3.1lem2  44218  proot1ex  44390  lhe4.4ex1a  45505  expgrowthi  45509  expgrowth  45511  binomcxplemnotnn0  45532  dvsinax  47128  dvasinbx  47135  dvcosax  47141  stoweidlem10  47225  wallispi2lem1  47286  wallispi2  47288  fouriersw  47446  sinnpoly  48146  m1modmmod  48639  dfodd6  48940  opoeALTV  48986  opeoALTV  48987  2zrngnmrid  49558  sinh-conventional  51112  amgmwlem  51267