Theorem mulcl 11180

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094   · cmul 11101

This theorem was proved from axioms:  ax-mulcl 11158

This theorem is referenced by:  mpomulf  11191  0cn  11194  mulrid  11202  mulcli  11212  mulcld  11225  mul31  11373  mul4  11374  mul02  11384  cnegex2  11388  muladd11r  11419  muladd  11642  subdi  11643  submul2  11650  mulsub  11653  recextlem1  11840  recex  11842  muleqadd  11854  mulnzcnf  11856  mulcan1g  11863  divass  11886  divmulass  11891  divmuldiv  11911  divmuleq  11916  divadddiv  11926  conjmul  11928  cju  12210  zneo  12675  cnref1o  13005  modcyc2  13936  muladdmodid  13942  negmod  13948  modaddmulmod  13970  expcl  14111  expclzlem  14115  mulexp  14133  sqcl  14150  subsq  14242  subsq2  14243  binom2sub  14252  mulbinom2  14255  binom3  14256  zesq  14258  bernneq  14261  bernneq2  14262  mulsubdivbinom2  14294  bcval5  14350  reim  15156  imcl  15158  crre  15161  crim  15162  remim  15164  mulre  15168  cjreb  15170  recj  15171  reneg  15172  readd  15173  remullem  15175  remul2  15177  imcj  15179  imneg  15180  imadd  15181  immul2  15184  cjadd  15188  ipcnval  15190  cjmulrcl  15191  cjneg  15194  imval2  15198  cjreim  15207  rennim  15286  cnpart  15287  sqrtneg  15314  sqabsadd  15329  sqabssub  15330  absreimsq  15339  absreim  15340  absmul  15341  sqreulem  15407  sqreu  15408  mulcn2  15643  o1mul  15662  climmul  15680  iseraltlem2  15730  prodf  15937  clim2div  15939  prodfmul  15940  prodfn0  15944  prodfrec  15945  prodfdiv  15946  prodmolem3  15983  prodmolem2a  15984  fprodcl  16002  fprodclf  16042  risefaccl  16065  fallfaccl  16066  bpoly3  16108  fsumcube  16110  efexp  16153  sinf  16176  cosf  16177  tanval2  16185  tanval3  16186  resinval  16187  recosval  16188  efi4p  16189  resin4p  16190  recos4p  16191  resincl  16192  recoscl  16193  sinneg  16198  cosneg  16199  efival  16204  efmival  16205  sinhval  16206  coshval  16207  retanhcl  16211  tanhlt1  16212  tanhbnd  16213  efeul  16214  sinadd  16216  cosadd  16217  sinsub  16220  cossub  16221  subsin  16223  sinmul  16224  cosmul  16225  addcos  16226  subcos  16227  cos2tsin  16231  ef01bndlem  16236  sin01bnd  16237  cos01bnd  16238  absef  16249  absefib  16250  efieq1re  16251  demoivre  16252  demoivreALT  16253  dvdscmulr  16338  dvdsmulcr  16339  odd2np1lem  16394  odd2np1  16395  opoe  16417  omoe  16418  opeo  16419  omeo  16420  gcdaddm  16579  modgcd  16586  bezoutlem1  16593  qredeq  16711  eulerthlem2  16837  modprm0  16861  pythagtriplem1  16872  pythagtriplem12  16882  pythagtriplem14  16884  iserodd  16891  gzmulcl  16994  4sqlem11  17011  4sqlem17  17017  cncrng  21508  cnfldmulg  21519  cnsubrg  21542  mpomulcn  24991  mulc1cncf  25029  icccvx  25074  pcorevlem  25150  cnlmod  25264  cnstrcvs  25265  cncvs  25269  itgcnlem  25914  itgneg  25928  itgconst  25943  itgadd  25949  iblabs  25953  itgmulc2  25958  dvmulbr  26063  dvmulf  26067  dvsincos  26105  plymullem1  26336  plymulcl  26343  plysubcl  26344  dgrcolem1  26395  dgrcolem2  26396  plydivlem4  26422  quotlem  26426  quotcl2  26428  quotdgr  26429  aaliou3lem3  26470  efper  26606  sinperlem  26607  sin2kpi  26610  cos2kpi  26611  efimpi  26618  sincosq1eq  26639  pige3ALT  26647  abssinper  26648  sinkpi  26649  coskpi  26650  sineq0  26651  coseq1  26652  tanregt0  26666  efif1olem4  26672  efifo  26674  eff1olem  26675  lognegb  26717  eflogeq  26729  efiarg  26734  tanarg  26746  logf1o2  26777  cxpcl  26801  cxpne0  26804  cxpsqrtlem  26829  cxpsqrt  26830  dvcxp1  26867  dvcncxp1  26870  root1eq1  26882  cxpeq  26884  relogbmul  26904  quad2  26966  quad  26967  dcubic2  26971  dcubic1  26972  dcubic  26973  mcubic  26974  cubic2  26975  cubic  26976  binom4  26977  dquartlem1  26978  dquartlem2  26979  dquart  26980  quart1cl  26981  quart1lem  26982  quart1  26983  quartlem1  26984  quartlem2  26985  quartlem3  26986  quart  26988  asinlem  26995  asinlem2  26996  asinlem3a  26997  asinlem3  26998  asinf  26999  atandm2  27004  atanf  27007  asinneg  27013  efiasin  27015  sinasin  27016  asinsinlem  27018  asinsin  27019  asinbnd  27026  cosasin  27031  atanneg  27034  atancj  27037  efiatan  27039  atanlogaddlem  27040  atanlogadd  27041  atanlogsublem  27042  atanlogsub  27043  efiatan2  27044  2efiatan  27045  tanatan  27046  cosatan  27048  atantan  27050  atanbndlem  27052  atans2  27058  dvatan  27062  atantayl  27064  atantayl2  27065  leibpilem2  27068  efrlim  27096  zetacvg  27141  ftalem7  27205  basellem3  27209  basellem7  27213  basellem8  27214  basellem9  27215  ppiub  27330  dchrmulcl  27375  bposlem9  27418  lgsdir  27458  lgsdilem2  27459  lgsdi  27460  lgsne0  27461  lgsquadlem1  27506  2sqlem2  27544  rpvmasum2  27638  dchrisum0lem1  27642  dchrisum0lem2  27644  mulogsumlem  27657  mulog2sumlem3  27662  log2sumbnd  27670  selberglem1  27671  selberglem2  27672  selberg2  27677  pntlemk  27732  colinearalglem1  29193  colinearalglem2  29194  ax5seglem1  29215  axcontlem2  29252  axcontlem8  29258  numclwwlk3lem1  30670  smcnlem  30986  ipval2  30996  4ipval2  30997  ipidsq  30999  dipcj  31003  cncph  31108  ipasslem2  31121  ipasslem4  31123  ipasslem9  31127  ipasslem11  31129  hhssnv  31553  spansncol  31857  homulass  32091  lnfnmuli  32333  riesz3i  32351  circum  36061  faclim  36133  mpomulnzcnf  36696  sin2h  38144  cos2h  38145  itg2addnclem3  38207  itgaddnc  38214  iblabsnc  38218  iblmulc2nc  38219  itgmulc2nc  38222  ftc1anclem3  38229  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  dvasin  38238  cntotbnd  38330  rmxluc  43548  rmyluc  43549  jm2.17a  43572  jm2.18  43600  jm3.1lem1  43629  jm3.1lem2  43630  proot1ex  43808  lhe4.4ex1a  44924  expgrowthi  44928  expgrowth  44930  binomcxplemnotnn0  44951  dvsinax  46512  dvasinbx  46519  dvcosax  46525  stoweidlem10  46609  wallispi2lem1  46670  wallispi2  46672  fouriersw  46830  sinnpoly  47510  m1modmmod  47983  dfodd6  48284  opoeALTV  48330  opeoALTV  48331  2zrngnmrid  48903  sinh-conventional  50395  amgmwlem  50458