Theorem mulcl 11212

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

Assertion

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

Proof of Theorem mulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   · cmul 11133

This proof depends on axioms:  ax-mulcl 11190

This theorem is used by:  mpomulf  11223  0cn  11226  mulrid  11234  mulcli  11244  mulcld  11257  mul31  11405  mul4  11406  mul02  11416  cnegex2  11420  muladd11r  11451  muladd  11674  subdi  11675  submul2  11682  mulsub  11685  recextlem1  11872  recex  11874  muleqadd  11886  mulnzcnf  11888  mulcan1g  11895  divass  11918  divmulass  11923  divmuldiv  11943  divmuleq  11948  divadddiv  11958  conjmul  11960  cju  12242  zneo  12708  cnref1o  13039  modcyc2  13972  muladdmodid  13978  negmod  13984  modaddmulmod  14006  expcl  14147  expclzlem  14151  mulexp  14169  sqcl  14186  subsq  14278  subsq2  14279  binom2sub  14288  mulbinom2  14291  binom3  14292  zesq  14294  bernneq  14297  bernneq2  14298  mulsubdivbinom2  14330  bcval5  14386  reim  15200  imcl  15202  crre  15205  crim  15206  remim  15208  mulre  15212  cjreb  15214  recj  15215  reneg  15216  readd  15217  remullem  15219  remul2  15221  imcj  15223  imneg  15224  imadd  15225  immul2  15228  cjadd  15232  ipcnval  15234  cjmulrcl  15235  cjneg  15238  imval2  15242  cjreim  15251  rennim  15330  cnpart  15331  sqrtneg  15358  sqabsadd  15373  sqabssub  15374  absreimsq  15383  absreim  15384  absmul  15385  sqreulem  15451  sqreu  15452  mulcn2  15687  o1mul  15706  climmul  15724  iseraltlem2  15774  prodf  15980  clim2div  15982  prodfmul  15983  prodfn0  15987  prodfrec  15988  prodfdiv  15989  prodmolem3  16026  prodmolem2a  16027  fprodcl  16045  fprodclf  16085  risefaccl  16108  fallfaccl  16109  bpoly3  16150  fsumcube  16152  efexp  16195  sinf  16218  cosf  16219  tanval2  16227  tanval3  16228  resinval  16229  recosval  16230  efi4p  16231  resin4p  16232  recos4p  16233  resincl  16234  recoscl  16235  sinneg  16240  cosneg  16241  efival  16246  efmival  16247  sinhval  16248  coshval  16249  retanhcl  16253  tanhlt1  16254  tanhbnd  16255  efeul  16256  sinadd  16258  cosadd  16259  sinsub  16262  cossub  16263  subsin  16265  sinmul  16266  cosmul  16267  addcos  16268  subcos  16269  cos2tsin  16273  ef01bndlem  16278  sin01bnd  16279  cos01bnd  16280  absef  16291  absefib  16292  efieq1re  16293  demoivre  16294  demoivreALT  16295  dvdscmulr  16380  dvdsmulcr  16381  odd2np1lem  16436  odd2np1  16437  opoe  16459  omoe  16460  opeo  16461  omeo  16462  gcdaddm  16621  modgcd  16628  bezoutlem1  16635  qredeq  16753  eulerthlem2  16879  modprm0  16903  pythagtriplem1  16914  pythagtriplem12  16924  pythagtriplem14  16926  iserodd  16933  gzmulcl  17036  4sqlem11  17053  4sqlem17  17059  cncrng  21612  cnfldmulg  21623  cnsubrg  21646  mpomulcn  25101  mulc1cncf  25139  icccvx  25184  pcorevlem  25260  cnlmod  25374  cnstrcvs  25375  cncvs  25379  itgcnlem  26024  itgneg  26038  itgconst  26053  itgadd  26059  iblabs  26063  itgmulc2  26068  dvmulbr  26173  dvmulf  26177  dvsincos  26215  plymullem1  26447  plymulcl  26454  plysubcl  26455  dgrcolem1  26506  dgrcolem2  26507  plydivlem4  26533  quotlem  26537  quotcl2  26539  quotdgr  26540  aaliou3lem3  26587  efper  26724  sinperlem  26725  sin2kpi  26728  cos2kpi  26729  efimpi  26736  sincosq1eq  26757  pige3ALT  26765  abssinper  26766  sinkpi  26767  coskpi  26768  sineq0  26769  coseq1  26770  tanregt0  26784  efif1olem4  26790  efifo  26792  eff1olem  26793  lognegb  26835  eflogeq  26847  efiarg  26852  tanarg  26864  logf1o2  26895  cxpcl  26919  cxpne0  26922  cxpsqrtlem  26947  cxpsqrt  26948  dvcxp1  26985  dvcncxp1  26988  root1eq1  27000  cxpeq  27002  relogbmul  27022  quad2  27084  quad  27085  dcubic2  27089  dcubic1  27090  dcubic  27091  mcubic  27092  cubic2  27093  cubic  27094  binom4  27095  dquartlem1  27096  dquartlem2  27097  dquart  27098  quart1cl  27099  quart1lem  27100  quart1  27101  quartlem1  27102  quartlem2  27103  quartlem3  27104  quart  27106  asinlem  27113  asinlem2  27114  asinlem3a  27115  asinlem3  27116  asinf  27117  atandm2  27122  atanf  27125  asinneg  27131  efiasin  27133  sinasin  27134  asinsinlem  27136  asinsin  27137  asinbnd  27144  cosasin  27149  atanneg  27152  atancj  27155  efiatan  27157  atanlogaddlem  27158  atanlogadd  27159  atanlogsublem  27160  atanlogsub  27161  efiatan2  27162  2efiatan  27163  tanatan  27164  cosatan  27166  atantan  27168  atanbndlem  27170  atans2  27176  dvatan  27180  atantayl  27182  atantayl2  27183  leibpilem2  27186  efrlim  27214  zetacvg  27259  ftalem7  27323  basellem3  27327  basellem7  27331  basellem8  27332  basellem9  27333  ppiub  27448  dchrmulcl  27493  bposlem9  27536  lgsdir  27576  lgsdilem2  27577  lgsdi  27578  lgsne0  27579  lgsquadlem1  27624  2sqlem2  27662  rpvmasum2  27756  dchrisum0lem1  27760  dchrisum0lem2  27762  mulogsumlem  27775  mulog2sumlem3  27780  log2sumbnd  27788  selberglem1  27789  selberglem2  27790  selberg2  27795  pntlemk  27850  colinearalglem1  29371  colinearalglem2  29372  ax5seglem1  29393  axcontlem2  29430  axcontlem8  29436  numclwwlk3lem1  30870  smcnlem  31186  ipval2  31196  4ipval2  31197  ipidsq  31199  dipcj  31203  cncph  31308  ipasslem2  31321  ipasslem4  31323  ipasslem9  31327  ipasslem11  31329  hhssnv  31753  spansncol  32057  homulass  32291  lnfnmuli  32533  riesz3i  32551  circum  36261  faclim  36333  mpomulnzcnf  36927  sin2h  38372  cos2h  38373  itg2addnclem3  38430  itgaddnc  38437  iblabsnc  38441  iblmulc2nc  38442  itgmulc2nc  38445  ftc1anclem3  38452  ftc1anclem6  38455  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  dvasin  38461  cntotbnd  38554  rmxluc  43785  rmyluc  43786  jm2.17a  43809  jm2.18  43837  jm3.1lem1  43866  jm3.1lem2  43867  proot1ex  44045  lhe4.4ex1a  45161  expgrowthi  45165  expgrowth  45167  binomcxplemnotnn0  45188  dvsinax  46749  dvasinbx  46756  dvcosax  46762  stoweidlem10  46846  wallispi2lem1  46907  wallispi2  46909  fouriersw  47067  sinnpoly  47767  m1modmmod  48260  dfodd6  48561  opoeALTV  48607  opeoALTV  48608  2zrngnmrid  49179  sinh-conventional  50673  amgmwlem  50828