Theorem mulcl 11211

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   · cmul 11132

This theorem was proved from axioms:  ax-mulcl 11189

This theorem is referenced by:  mpomulf  11222  0cn  11225  mulrid  11231  mulcli  11240  mulcld  11253  mul31  11400  mul4  11401  mul02  11411  cnegex2  11415  muladd11r  11446  muladd  11667  subdi  11668  submul2  11675  mulsub  11678  recextlem1  11865  recex  11867  muleqadd  11879  mulnzcnf  11881  mulcan1g  11888  divass  11912  divmulass  11917  divmuldiv  11939  divmuleq  11944  divadddiv  11954  conjmul  11956  cju  12234  zneo  12674  cnref1o  12999  modcyc2  13922  muladdmodid  13926  negmod  13932  modaddmulmod  13954  expcl  14095  expclzlem  14099  mulexp  14117  sqcl  14134  subsq  14226  subsq2  14227  binom2sub  14236  mulbinom2  14239  binom3  14240  zesq  14242  bernneq  14245  bernneq2  14246  mulsubdivbinom2  14278  bcval5  14334  reim  15126  imcl  15128  crre  15131  crim  15132  remim  15134  mulre  15138  cjreb  15140  recj  15141  reneg  15142  readd  15143  remullem  15145  remul2  15147  imcj  15149  imneg  15150  imadd  15151  immul2  15154  cjadd  15158  ipcnval  15160  cjmulrcl  15161  cjneg  15164  imval2  15168  cjreim  15177  rennim  15256  cnpart  15257  sqrtneg  15284  sqabsadd  15299  sqabssub  15300  absreimsq  15309  absreim  15310  absmul  15311  sqreulem  15376  sqreu  15377  mulcn2  15610  o1mul  15629  climmul  15647  iseraltlem2  15697  prodf  15901  clim2div  15903  prodfmul  15904  prodfn0  15908  prodfrec  15909  prodfdiv  15910  prodmolem3  15947  prodmolem2a  15948  fprodcl  15966  fprodclf  16006  risefaccl  16029  fallfaccl  16030  bpoly3  16072  fsumcube  16074  efexp  16117  sinf  16140  cosf  16141  tanval2  16149  tanval3  16150  resinval  16151  recosval  16152  efi4p  16153  resin4p  16154  recos4p  16155  resincl  16156  recoscl  16157  sinneg  16162  cosneg  16163  efival  16168  efmival  16169  sinhval  16170  coshval  16171  retanhcl  16175  tanhlt1  16176  tanhbnd  16177  efeul  16178  sinadd  16180  cosadd  16181  sinsub  16184  cossub  16185  subsin  16187  sinmul  16188  cosmul  16189  addcos  16190  subcos  16191  cos2tsin  16195  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  absef  16213  absefib  16214  efieq1re  16215  demoivre  16216  demoivreALT  16217  dvdscmulr  16302  dvdsmulcr  16303  odd2np1lem  16357  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  gcdaddm  16542  modgcd  16549  bezoutlem1  16556  qredeq  16674  eulerthlem2  16799  modprm0  16823  pythagtriplem1  16834  pythagtriplem12  16844  pythagtriplem14  16846  iserodd  16853  gzmulcl  16956  4sqlem11  16973  4sqlem17  16979  cncrng  21349  cncrngOLD  21350  cnfldmulg  21364  cnsubrg  21393  mpomulcn  24807  mulc1cncf  24847  icccvx  24897  pcorevlem  24975  cnlmod  25089  cnstrcvs  25090  cncvs  25094  itgcnlem  25741  itgneg  25755  itgconst  25770  itgadd  25776  iblabs  25780  itgmulc2  25785  dvmulbr  25891  dvmulbrOLD  25892  dvmulf  25896  dvsincos  25935  plymullem1  26169  plymulcl  26176  plysubcl  26177  dgrcolem1  26229  dgrcolem2  26230  plydivlem4  26254  quotlem  26258  quotcl2  26260  quotdgr  26261  aaliou3lem3  26302  efper  26438  sinperlem  26439  sin2kpi  26442  cos2kpi  26443  efimpi  26450  sincosq1eq  26471  pige3ALT  26479  abssinper  26480  sinkpi  26481  coskpi  26482  sineq0  26483  coseq1  26484  tanregt0  26498  efif1olem4  26504  efifo  26506  eff1olem  26507  lognegb  26549  eflogeq  26561  efiarg  26566  tanarg  26578  logf1o2  26609  cxpcl  26633  cxpne0  26636  cxpsqrtlem  26661  cxpsqrt  26662  dvcxp1  26699  dvcncxp1  26702  root1eq1  26715  cxpeq  26717  relogbmul  26737  quad2  26799  quad  26800  dcubic2  26804  dcubic1  26805  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  binom4  26810  dquartlem1  26811  dquartlem2  26812  dquart  26813  quart1cl  26814  quart1lem  26815  quart1  26816  quartlem1  26817  quartlem2  26818  quartlem3  26819  quart  26821  asinlem  26828  asinlem2  26829  asinlem3a  26830  asinlem3  26831  asinf  26832  atandm2  26837  atanf  26840  asinneg  26846  efiasin  26848  sinasin  26849  asinsinlem  26851  asinsin  26852  asinbnd  26859  cosasin  26864  atanneg  26867  atancj  26870  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsublem  26875  atanlogsub  26876  efiatan2  26877  2efiatan  26878  tanatan  26879  cosatan  26881  atantan  26883  atanbndlem  26885  atans2  26891  dvatan  26895  atantayl  26897  atantayl2  26898  leibpilem2  26901  efrlim  26929  efrlimOLD  26930  zetacvg  26975  ftalem7  27039  basellem3  27043  basellem7  27047  basellem8  27048  basellem9  27049  ppiub  27165  dchrmulcl  27210  bposlem9  27253  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  lgsquadlem1  27341  2sqlem2  27379  rpvmasum2  27473  dchrisum0lem1  27477  dchrisum0lem2  27479  mulogsumlem  27492  mulog2sumlem3  27497  log2sumbnd  27505  selberglem1  27506  selberglem2  27507  selberg2  27512  pntlemk  27567  colinearalglem1  28831  colinearalglem2  28832  ax5seglem1  28853  axcontlem2  28890  axcontlem8  28896  numclwwlk3lem1  30309  smcnlem  30624  ipval2  30634  4ipval2  30635  ipidsq  30637  dipcj  30641  cncph  30746  ipasslem2  30759  ipasslem4  30761  ipasslem9  30765  ipasslem11  30767  hhssnv  31191  spansncol  31495  homulass  31729  lnfnmuli  31971  riesz3i  31989  circum  35642  faclim  35709  mpomulnzcnf  36263  sin2h  37580  cos2h  37581  itg2addnclem3  37643  itgaddnc  37650  iblabsnc  37654  iblmulc2nc  37655  itgmulc2nc  37658  ftc1anclem3  37665  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  dvasin  37674  cntotbnd  37766  fac2xp3  42198  rmxluc  42907  rmyluc  42908  jm2.17a  42931  jm2.18  42959  jm3.1lem1  42988  jm3.1lem2  42989  proot1ex  43167  lhe4.4ex1a  44301  expgrowthi  44305  expgrowth  44307  binomcxplemnotnn0  44328  dvsinax  45890  dvasinbx  45897  dvcosax  45903  stoweidlem10  45987  wallispi2lem1  46048  wallispi2  46050  fouriersw  46208  dfodd6  47599  opoeALTV  47645  opeoALTV  47646  2zrngnmrid  48179  m1modmmod  48449  sinh-conventional  49551  amgmwlem  49614