Theorem mulcl 11287

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

Assertion

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

Proof of Theorem mulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   · cmul 11208

This proof depends on axioms:  ax-mulcl 11265

This theorem is used by:  mpomulf  11298  0cn  11301  mulrid  11309  mulcli  11319  mulcld  11332  mul31  11480  mul4  11481  mul02  11491  cnegex2  11495  muladd11r  11526  muladd  11751  subdi  11752  submul2  11759  mulsub  11762  recextlem1  11949  recex  11951  muleqadd  11963  mulnzcnf  11965  mulcan1g  11972  divass  11995  divmulass  12000  divmuldiv  12020  divmuleq  12025  divadddiv  12035  conjmul  12037  cju  12319  zneo  12785  cnref1o  13116  modcyc2  14050  muladdmodid  14056  negmod  14062  modaddmulmod  14084  expcl  14225  expclzlem  14229  mulexp  14247  sqcl  14264  subsq  14357  subsq2  14358  binom2sub  14367  mulbinom2  14370  binom3  14371  zesq  14373  bernneq  14376  bernneq2  14377  mulsubdivbinom2  14409  bcval5  14465  reim  15281  imcl  15283  crre  15286  crim  15287  remim  15289  mulre  15293  cjreb  15295  recj  15296  reneg  15297  readd  15298  remullem  15300  remul2  15302  imcj  15304  imneg  15305  imadd  15306  immul2  15309  cjadd  15313  ipcnval  15315  cjmulrcl  15316  cjneg  15319  imval2  15323  cjreim  15332  rennim  15411  cnpart  15412  sqrtneg  15439  sqabsadd  15454  sqabssub  15455  absreimsq  15464  absreim  15465  absmul  15466  sqreulem  15532  sqreu  15533  mulcn2  15768  o1mul  15787  climmul  15805  iseraltlem2  15855  prodf  16061  clim2div  16063  prodfmul  16064  prodfn0  16068  prodfrec  16069  prodfdiv  16070  prodmolem3  16105  prodmolem2a  16106  fprodcl  16124  fprodclf  16164  risefaccl  16187  fallfaccl  16188  bpoly3  16229  fsumcube  16231  efexp  16274  sinf  16297  cosf  16298  tanval2  16306  tanval3  16307  resinval  16308  recosval  16309  efi4p  16310  resin4p  16311  recos4p  16312  resincl  16313  recoscl  16314  sinneg  16319  cosneg  16320  efival  16325  efmival  16326  sinhval  16327  coshval  16328  retanhcl  16332  tanhlt1  16333  tanhbnd  16334  efeul  16335  sinadd  16337  cosadd  16338  sinsub  16341  cossub  16342  subsin  16344  sinmul  16345  cosmul  16346  addcos  16347  subcos  16348  cos2tsin  16352  ef01bndlem  16357  sin01bnd  16358  cos01bnd  16359  absef  16370  absefib  16371  efieq1re  16372  demoivre  16373  demoivreALT  16374  dvdscmulr  16459  dvdsmulcr  16460  odd2np1lem  16515  odd2np1  16516  opoe  16538  omoe  16539  opeo  16540  omeo  16541  gcdaddm  16702  modgcd  16710  bezoutlem1  16717  qredeq  16837  eulerthlem2  16964  modprm0  16988  pythagtriplem1  16999  pythagtriplem12  17009  pythagtriplem14  17011  iserodd  17018  gzmulcl  17121  4sqlem11  17138  4sqlem17  17144  cncrng  21704  cnfldmulg  21715  cnsubrg  21738  mpomulcn  25193  mulc1cncf  25231  icccvx  25276  pcorevlem  25352  cnlmod  25466  cnstrcvs  25467  cncvs  25471  itgcnlem  26115  itgneg  26129  itgconst  26144  itgadd  26150  iblabs  26154  itgmulc2  26159  dvmulbr  26264  dvmulf  26268  dvsincos  26306  plymullem1  26538  plymulcl  26545  plysubcl  26546  dgrcolem1  26597  dgrcolem2  26598  plydivlem4  26622  quotlem  26626  quotcl2  26628  quotdgr  26629  aaliou3lem3  26676  efper  26813  sinperlem  26814  sin2kpi  26817  cos2kpi  26818  efimpi  26825  sincosq1eq  26846  pige3ALT  26853  abssinper  26854  sinkpi  26855  coskpi  26856  sineq0  26857  coseq1  26858  tanregt0  26872  efif1olem4  26878  efifo  26880  eff1olem  26881  lognegb  26923  eflogeq  26935  efiarg  26940  tanarg  26952  logf1o2  26983  cxpcl  27007  cxpne0  27010  cxpsqrtlem  27035  cxpsqrt  27036  dvcxp1  27073  dvcncxp1  27076  root1eq1  27088  cxpeq  27090  relogbmul  27110  quad2  27172  quad  27173  dcubic2  27177  dcubic1  27178  dcubic  27179  mcubic  27180  cubic2  27181  cubic  27182  binom4  27183  dquartlem1  27184  dquartlem2  27185  dquart  27186  quart1cl  27187  quart1lem  27188  quart1  27189  quartlem1  27190  quartlem2  27191  quartlem3  27192  quart  27194  asinlem  27201  asinlem2  27202  asinlem3a  27203  asinlem3  27204  asinf  27205  atandm2  27210  atanf  27213  asinneg  27219  efiasin  27221  sinasin  27222  asinsinlem  27224  asinsin  27225  asinbnd  27232  cosasin  27237  atanneg  27240  atancj  27243  efiatan  27245  atanlogaddlem  27246  atanlogadd  27247  atanlogsublem  27248  atanlogsub  27249  efiatan2  27250  2efiatan  27251  tanatan  27252  cosatan  27254  atantan  27256  atanbndlem  27258  atans2  27264  dvatan  27268  atantayl  27270  atantayl2  27271  leibpilem2  27274  efrlim  27302  zetacvg  27347  ftalem7  27411  basellem3  27415  basellem7  27419  basellem8  27420  basellem9  27421  ppiub  27536  dchrmulcl  27581  bposlem9  27624  lgsdir  27664  lgsdilem2  27665  lgsdi  27666  lgsne0  27667  lgsquadlem1  27712  2sqlem2  27750  rpvmasum2  27844  dchrisum0lem1  27848  dchrisum0lem2  27850  mulogsumlem  27863  mulog2sumlem3  27868  log2sumbnd  27876  selberglem1  27877  selberglem2  27878  selberg2  27883  pntlemk  27938  colinearalglem1  29489  colinearalglem2  29490  ax5seglem1  29511  axcontlem2  29548  axcontlem8  29554  numclwwlk3lem1  30988  smcnlem  31304  ipval2  31314  4ipval2  31315  ipidsq  31317  dipcj  31321  cncph  31426  ipasslem2  31439  ipasslem4  31441  ipasslem9  31445  ipasslem11  31447  hhssnv  31871  spansncol  32175  homulass  32409  lnfnmuli  32651  riesz3i  32669  circum  36525  faclim  36603  mpomulnzcnf  37180  sin2h  38626  cos2h  38627  itg2addnclem3  38684  itgaddnc  38691  iblabsnc  38695  iblmulc2nc  38696  itgmulc2nc  38699  ftc1anclem3  38706  ftc1anclem6  38709  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  dvasin  38715  cntotbnd  38823  rmxluc  44036  rmyluc  44037  jm2.17a  44060  jm2.18  44088  jm3.1lem1  44117  jm3.1lem2  44118  proot1ex  44291  lhe4.4ex1a  45406  expgrowthi  45410  expgrowth  45412  binomcxplemnotnn0  45433  dvsinax  47016  dvasinbx  47023  dvcosax  47029  stoweidlem10  47113  wallispi2lem1  47174  wallispi2  47176  fouriersw  47334  sinnpoly  48034  m1modmmod  48527  dfodd6  48828  opoeALTV  48874  opeoALTV  48875  2zrngnmrid  49446  sinh-conventional  51000  amgmwlem  51155