Theorem mulcl 11236

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

This theorem was proved from axioms:  ax-mulcl 11214

This theorem is referenced by:  mpomulf  11247  0cn  11250  mulrid  11256  mulcli  11265  mulcld  11278  mul31  11425  mul4  11426  mul02  11436  cnegex2  11440  muladd11r  11471  muladd  11692  subdi  11693  submul2  11700  mulsub  11703  recextlem1  11890  recex  11892  muleqadd  11904  mulnzcnf  11906  mulcan1g  11913  divass  11937  divmulass  11942  divmuldiv  11964  divmuleq  11969  divadddiv  11979  conjmul  11981  cju  12259  zneo  12698  cnref1o  13024  modcyc2  13943  muladdmodid  13947  negmod  13953  modaddmulmod  13975  expcl  14116  expclzlem  14120  mulexp  14138  sqcl  14154  subsq  14245  subsq2  14246  binom2sub  14255  mulbinom2  14258  binom3  14259  zesq  14261  bernneq  14264  bernneq2  14265  mulsubdivbinom2  14297  bcval5  14353  reim  15144  imcl  15146  crre  15149  crim  15150  remim  15152  mulre  15156  cjreb  15158  recj  15159  reneg  15160  readd  15161  remullem  15163  remul2  15165  imcj  15167  imneg  15168  imadd  15169  immul2  15172  cjadd  15176  ipcnval  15178  cjmulrcl  15179  cjneg  15182  imval2  15186  cjreim  15195  rennim  15274  cnpart  15275  sqrtneg  15302  sqabsadd  15317  sqabssub  15318  absreimsq  15327  absreim  15328  absmul  15329  sqreulem  15394  sqreu  15395  mulcn2  15628  o1mul  15647  climmul  15665  iseraltlem2  15715  prodf  15919  clim2div  15921  prodfmul  15922  prodfn0  15926  prodfrec  15927  prodfdiv  15928  prodmolem3  15965  prodmolem2a  15966  fprodcl  15984  fprodclf  16024  risefaccl  16047  fallfaccl  16048  bpoly3  16090  fsumcube  16092  efexp  16133  sinf  16156  cosf  16157  tanval2  16165  tanval3  16166  resinval  16167  recosval  16168  efi4p  16169  resin4p  16170  recos4p  16171  resincl  16172  recoscl  16173  sinneg  16178  cosneg  16179  efival  16184  efmival  16185  sinhval  16186  coshval  16187  retanhcl  16191  tanhlt1  16192  tanhbnd  16193  efeul  16194  sinadd  16196  cosadd  16197  sinsub  16200  cossub  16201  subsin  16203  sinmul  16204  cosmul  16205  addcos  16206  subcos  16207  cos2tsin  16211  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  absef  16229  absefib  16230  efieq1re  16231  demoivre  16232  demoivreALT  16233  dvdscmulr  16318  dvdsmulcr  16319  odd2np1lem  16373  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  gcdaddm  16558  modgcd  16565  bezoutlem1  16572  qredeq  16690  eulerthlem2  16815  modprm0  16838  pythagtriplem1  16849  pythagtriplem12  16859  pythagtriplem14  16861  iserodd  16868  gzmulcl  16971  4sqlem11  16988  4sqlem17  16994  cncrng  21418  cncrngOLD  21419  cnfldmulg  21433  cnsubrg  21462  mpomulcn  24904  mulc1cncf  24944  icccvx  24994  pcorevlem  25072  cnlmod  25186  cnstrcvs  25187  cncvs  25191  itgcnlem  25839  itgneg  25853  itgconst  25868  itgadd  25874  iblabs  25878  itgmulc2  25883  dvmulbr  25989  dvmulbrOLD  25990  dvmulf  25994  dvsincos  26033  plymullem1  26267  plymulcl  26274  plysubcl  26275  dgrcolem1  26327  dgrcolem2  26328  plydivlem4  26352  quotlem  26356  quotcl2  26358  quotdgr  26359  aaliou3lem3  26400  efper  26535  sinperlem  26536  sin2kpi  26539  cos2kpi  26540  efimpi  26547  sincosq1eq  26568  pige3ALT  26576  abssinper  26577  sinkpi  26578  coskpi  26579  sineq0  26580  coseq1  26581  tanregt0  26595  efif1olem4  26601  efifo  26603  eff1olem  26604  lognegb  26646  eflogeq  26658  efiarg  26663  tanarg  26675  logf1o2  26706  cxpcl  26730  cxpne0  26733  cxpsqrtlem  26758  cxpsqrt  26759  dvcxp1  26796  dvcncxp1  26799  root1eq1  26812  cxpeq  26814  relogbmul  26834  quad2  26896  quad  26897  dcubic2  26901  dcubic1  26902  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  binom4  26907  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1cl  26911  quart1lem  26912  quart1  26913  quartlem1  26914  quartlem2  26915  quartlem3  26916  quart  26918  asinlem  26925  asinlem2  26926  asinlem3a  26927  asinlem3  26928  asinf  26929  atandm2  26934  atanf  26937  asinneg  26943  efiasin  26945  sinasin  26946  asinsinlem  26948  asinsin  26949  asinbnd  26956  cosasin  26961  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atanlogsub  26973  efiatan2  26974  2efiatan  26975  tanatan  26976  cosatan  26978  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl  26994  atantayl2  26995  leibpilem2  26998  efrlim  27026  efrlimOLD  27027  zetacvg  27072  ftalem7  27136  basellem3  27140  basellem7  27144  basellem8  27145  basellem9  27146  ppiub  27262  dchrmulcl  27307  bposlem9  27350  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  lgsquadlem1  27438  2sqlem2  27476  rpvmasum2  27570  dchrisum0lem1  27574  dchrisum0lem2  27576  mulogsumlem  27589  mulog2sumlem3  27594  log2sumbnd  27602  selberglem1  27603  selberglem2  27604  selberg2  27609  pntlemk  27664  colinearalglem1  28935  colinearalglem2  28936  ax5seglem1  28957  axcontlem2  28994  axcontlem8  29000  numclwwlk3lem1  30410  smcnlem  30725  ipval2  30735  4ipval2  30736  ipidsq  30738  dipcj  30742  cncph  30847  ipasslem2  30860  ipasslem4  30862  ipasslem9  30866  ipasslem11  30868  hhssnv  31292  spansncol  31596  homulass  31830  lnfnmuli  32072  riesz3i  32090  circum  35658  faclim  35725  mpomulnzcnf  36281  sin2h  37596  cos2h  37597  itg2addnclem3  37659  itgaddnc  37666  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nc  37674  ftc1anclem3  37681  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  dvasin  37690  cntotbnd  37782  fac2xp3  42220  rmxluc  42924  rmyluc  42925  jm2.17a  42948  jm2.18  42976  jm3.1lem1  43005  jm3.1lem2  43006  proot1ex  43184  lhe4.4ex1a  44324  expgrowthi  44328  expgrowth  44330  binomcxplemnotnn0  44351  dvsinax  45868  dvasinbx  45875  dvcosax  45881  stoweidlem10  45965  wallispi2lem1  46026  wallispi2  46028  fouriersw  46186  dfodd6  47561  opoeALTV  47607  opeoALTV  47608  2zrngnmrid  48099  m1modmmod  48370  sinh-conventional  48969  amgmwlem  49032