Theorem mulcl 11202

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

Assertion

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

Proof of Theorem mulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   · cmul 11123

This proof depends on axioms:  ax-mulcl 11180

This theorem is used by:  mpomulf  11213  0cn  11216  mulrid  11224  mulcli  11234  mulcld  11247  mul31  11395  mul4  11396  mul02  11406  cnegex2  11410  muladd11r  11441  muladd  11664  subdi  11665  submul2  11672  mulsub  11675  recextlem1  11862  recex  11864  muleqadd  11876  mulnzcnf  11878  mulcan1g  11885  divass  11908  divmulass  11913  divmuldiv  11933  divmuleq  11938  divadddiv  11948  conjmul  11950  cju  12232  zneo  12697  cnref1o  13027  modcyc2  13960  muladdmodid  13966  negmod  13972  modaddmulmod  13994  expcl  14135  expclzlem  14139  mulexp  14157  sqcl  14174  subsq  14266  subsq2  14267  binom2sub  14276  mulbinom2  14279  binom3  14280  zesq  14282  bernneq  14285  bernneq2  14286  mulsubdivbinom2  14318  bcval5  14374  reim  15186  imcl  15188  crre  15191  crim  15192  remim  15194  mulre  15198  cjreb  15200  recj  15201  reneg  15202  readd  15203  remullem  15205  remul2  15207  imcj  15209  imneg  15210  imadd  15211  immul2  15214  cjadd  15218  ipcnval  15220  cjmulrcl  15221  cjneg  15224  imval2  15228  cjreim  15237  rennim  15316  cnpart  15317  sqrtneg  15344  sqabsadd  15359  sqabssub  15360  absreimsq  15369  absreim  15370  absmul  15371  sqreulem  15437  sqreu  15438  mulcn2  15673  o1mul  15692  climmul  15710  iseraltlem2  15760  prodf  15967  clim2div  15969  prodfmul  15970  prodfn0  15974  prodfrec  15975  prodfdiv  15976  prodmolem3  16013  prodmolem2a  16014  fprodcl  16032  fprodclf  16072  risefaccl  16095  fallfaccl  16096  bpoly3  16137  fsumcube  16139  efexp  16182  sinf  16205  cosf  16206  tanval2  16214  tanval3  16215  resinval  16216  recosval  16217  efi4p  16218  resin4p  16219  recos4p  16220  resincl  16221  recoscl  16222  sinneg  16227  cosneg  16228  efival  16233  efmival  16234  sinhval  16235  coshval  16236  retanhcl  16240  tanhlt1  16241  tanhbnd  16242  efeul  16243  sinadd  16245  cosadd  16246  sinsub  16249  cossub  16250  subsin  16252  sinmul  16253  cosmul  16254  addcos  16255  subcos  16256  cos2tsin  16260  ef01bndlem  16265  sin01bnd  16266  cos01bnd  16267  absef  16278  absefib  16279  efieq1re  16280  demoivre  16281  demoivreALT  16282  dvdscmulr  16367  dvdsmulcr  16368  odd2np1lem  16423  odd2np1  16424  opoe  16446  omoe  16447  opeo  16448  omeo  16449  gcdaddm  16608  modgcd  16615  bezoutlem1  16622  qredeq  16740  eulerthlem2  16866  modprm0  16890  pythagtriplem1  16901  pythagtriplem12  16911  pythagtriplem14  16913  iserodd  16920  gzmulcl  17023  4sqlem11  17040  4sqlem17  17046  cncrng  21580  cnfldmulg  21591  cnsubrg  21614  mpomulcn  25063  mulc1cncf  25101  icccvx  25146  pcorevlem  25222  cnlmod  25336  cnstrcvs  25337  cncvs  25341  itgcnlem  25986  itgneg  26000  itgconst  26015  itgadd  26021  iblabs  26025  itgmulc2  26030  dvmulbr  26135  dvmulf  26139  dvsincos  26177  plymullem1  26408  plymulcl  26415  plysubcl  26416  dgrcolem1  26467  dgrcolem2  26468  plydivlem4  26494  quotlem  26498  quotcl2  26500  quotdgr  26501  aaliou3lem3  26544  efper  26681  sinperlem  26682  sin2kpi  26685  cos2kpi  26686  efimpi  26693  sincosq1eq  26714  pige3ALT  26722  abssinper  26723  sinkpi  26724  coskpi  26725  sineq0  26726  coseq1  26727  tanregt0  26741  efif1olem4  26747  efifo  26749  eff1olem  26750  lognegb  26792  eflogeq  26804  efiarg  26809  tanarg  26821  logf1o2  26852  cxpcl  26876  cxpne0  26879  cxpsqrtlem  26904  cxpsqrt  26905  dvcxp1  26942  dvcncxp1  26945  root1eq1  26957  cxpeq  26959  relogbmul  26979  quad2  27041  quad  27042  dcubic2  27046  dcubic1  27047  dcubic  27048  mcubic  27049  cubic2  27050  cubic  27051  binom4  27052  dquartlem1  27053  dquartlem2  27054  dquart  27055  quart1cl  27056  quart1lem  27057  quart1  27058  quartlem1  27059  quartlem2  27060  quartlem3  27061  quart  27063  asinlem  27070  asinlem2  27071  asinlem3a  27072  asinlem3  27073  asinf  27074  atandm2  27079  atanf  27082  asinneg  27088  efiasin  27090  sinasin  27091  asinsinlem  27093  asinsin  27094  asinbnd  27101  cosasin  27106  atanneg  27109  atancj  27112  efiatan  27114  atanlogaddlem  27115  atanlogadd  27116  atanlogsublem  27117  atanlogsub  27118  efiatan2  27119  2efiatan  27120  tanatan  27121  cosatan  27123  atantan  27125  atanbndlem  27127  atans2  27133  dvatan  27137  atantayl  27139  atantayl2  27140  leibpilem2  27143  efrlim  27171  zetacvg  27216  ftalem7  27280  basellem3  27284  basellem7  27288  basellem8  27289  basellem9  27290  ppiub  27405  dchrmulcl  27450  bposlem9  27493  lgsdir  27533  lgsdilem2  27534  lgsdi  27535  lgsne0  27536  lgsquadlem1  27581  2sqlem2  27619  rpvmasum2  27713  dchrisum0lem1  27717  dchrisum0lem2  27719  mulogsumlem  27732  mulog2sumlem3  27737  log2sumbnd  27745  selberglem1  27746  selberglem2  27747  selberg2  27752  pntlemk  27807  colinearalglem1  29293  colinearalglem2  29294  ax5seglem1  29315  axcontlem2  29352  axcontlem8  29358  numclwwlk3lem1  30770  smcnlem  31086  ipval2  31096  4ipval2  31097  ipidsq  31099  dipcj  31103  cncph  31208  ipasslem2  31221  ipasslem4  31223  ipasslem9  31227  ipasslem11  31229  hhssnv  31653  spansncol  31957  homulass  32191  lnfnmuli  32433  riesz3i  32451  circum  36186  faclim  36258  mpomulnzcnf  36851  sin2h  38301  cos2h  38302  itg2addnclem3  38364  itgaddnc  38371  iblabsnc  38375  iblmulc2nc  38376  itgmulc2nc  38379  ftc1anclem3  38386  ftc1anclem6  38389  ftc1anclem7  38390  ftc1anclem8  38391  ftc1anc  38392  dvasin  38395  cntotbnd  38487  rmxluc  43703  rmyluc  43704  jm2.17a  43727  jm2.18  43755  jm3.1lem1  43784  jm3.1lem2  43785  proot1ex  43963  lhe4.4ex1a  45079  expgrowthi  45083  expgrowth  45085  binomcxplemnotnn0  45106  dvsinax  46667  dvasinbx  46674  dvcosax  46680  stoweidlem10  46764  wallispi2lem1  46825  wallispi2  46827  fouriersw  46985  sinnpoly  47668  m1modmmod  48141  dfodd6  48442  opoeALTV  48488  opeoALTV  48489  2zrngnmrid  49061  sinh-conventional  50557  amgmwlem  50690