Theorem mulcl 11159

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

This theorem was proved from axioms:  ax-mulcl 11137

This theorem is referenced by:  mpomulf  11170  0cn  11173  mulrid  11179  mulcli  11188  mulcld  11201  mul31  11348  mul4  11349  mul02  11359  cnegex2  11363  muladd11r  11394  muladd  11617  subdi  11618  submul2  11625  mulsub  11628  recextlem1  11815  recex  11817  muleqadd  11829  mulnzcnf  11831  mulcan1g  11838  divass  11862  divmulass  11867  divmuldiv  11889  divmuleq  11894  divadddiv  11904  conjmul  11906  cju  12189  zneo  12624  cnref1o  12951  modcyc2  13876  muladdmodid  13882  negmod  13888  modaddmulmod  13910  expcl  14051  expclzlem  14055  mulexp  14073  sqcl  14090  subsq  14182  subsq2  14183  binom2sub  14192  mulbinom2  14195  binom3  14196  zesq  14198  bernneq  14201  bernneq2  14202  mulsubdivbinom2  14234  bcval5  14290  reim  15082  imcl  15084  crre  15087  crim  15088  remim  15090  mulre  15094  cjreb  15096  recj  15097  reneg  15098  readd  15099  remullem  15101  remul2  15103  imcj  15105  imneg  15106  imadd  15107  immul2  15110  cjadd  15114  ipcnval  15116  cjmulrcl  15117  cjneg  15120  imval2  15124  cjreim  15133  rennim  15212  cnpart  15213  sqrtneg  15240  sqabsadd  15255  sqabssub  15256  absreimsq  15265  absreim  15266  absmul  15267  sqreulem  15333  sqreu  15334  mulcn2  15569  o1mul  15588  climmul  15606  iseraltlem2  15656  prodf  15860  clim2div  15862  prodfmul  15863  prodfn0  15867  prodfrec  15868  prodfdiv  15869  prodmolem3  15906  prodmolem2a  15907  fprodcl  15925  fprodclf  15965  risefaccl  15988  fallfaccl  15989  bpoly3  16031  fsumcube  16033  efexp  16076  sinf  16099  cosf  16100  tanval2  16108  tanval3  16109  resinval  16110  recosval  16111  efi4p  16112  resin4p  16113  recos4p  16114  resincl  16115  recoscl  16116  sinneg  16121  cosneg  16122  efival  16127  efmival  16128  sinhval  16129  coshval  16130  retanhcl  16134  tanhlt1  16135  tanhbnd  16136  efeul  16137  sinadd  16139  cosadd  16140  sinsub  16143  cossub  16144  subsin  16146  sinmul  16147  cosmul  16148  addcos  16149  subcos  16150  cos2tsin  16154  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  absef  16172  absefib  16173  efieq1re  16174  demoivre  16175  demoivreALT  16176  dvdscmulr  16261  dvdsmulcr  16262  odd2np1lem  16317  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  gcdaddm  16502  modgcd  16509  bezoutlem1  16516  qredeq  16634  eulerthlem2  16759  modprm0  16783  pythagtriplem1  16794  pythagtriplem12  16804  pythagtriplem14  16806  iserodd  16813  gzmulcl  16916  4sqlem11  16933  4sqlem17  16939  cncrng  21307  cncrngOLD  21308  cnfldmulg  21322  cnsubrg  21351  mpomulcn  24765  mulc1cncf  24805  icccvx  24855  pcorevlem  24933  cnlmod  25047  cnstrcvs  25048  cncvs  25052  itgcnlem  25698  itgneg  25712  itgconst  25727  itgadd  25733  iblabs  25737  itgmulc2  25742  dvmulbr  25848  dvmulbrOLD  25849  dvmulf  25853  dvsincos  25892  plymullem1  26126  plymulcl  26133  plysubcl  26134  dgrcolem1  26186  dgrcolem2  26187  plydivlem4  26211  quotlem  26215  quotcl2  26217  quotdgr  26218  aaliou3lem3  26259  efper  26395  sinperlem  26396  sin2kpi  26399  cos2kpi  26400  efimpi  26407  sincosq1eq  26428  pige3ALT  26436  abssinper  26437  sinkpi  26438  coskpi  26439  sineq0  26440  coseq1  26441  tanregt0  26455  efif1olem4  26461  efifo  26463  eff1olem  26464  lognegb  26506  eflogeq  26518  efiarg  26523  tanarg  26535  logf1o2  26566  cxpcl  26590  cxpne0  26593  cxpsqrtlem  26618  cxpsqrt  26619  dvcxp1  26656  dvcncxp1  26659  root1eq1  26672  cxpeq  26674  relogbmul  26694  quad2  26756  quad  26757  dcubic2  26761  dcubic1  26762  dcubic  26763  mcubic  26764  cubic2  26765  cubic  26766  binom4  26767  dquartlem1  26768  dquartlem2  26769  dquart  26770  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  quartlem2  26775  quartlem3  26776  quart  26778  asinlem  26785  asinlem2  26786  asinlem3a  26787  asinlem3  26788  asinf  26789  atandm2  26794  atanf  26797  asinneg  26803  efiasin  26805  sinasin  26806  asinsinlem  26808  asinsin  26809  asinbnd  26816  cosasin  26821  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsublem  26832  atanlogsub  26833  efiatan2  26834  2efiatan  26835  tanatan  26836  cosatan  26838  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl  26854  atantayl2  26855  leibpilem2  26858  efrlim  26886  efrlimOLD  26887  zetacvg  26932  ftalem7  26996  basellem3  27000  basellem7  27004  basellem8  27005  basellem9  27006  ppiub  27122  dchrmulcl  27167  bposlem9  27210  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  lgsquadlem1  27298  2sqlem2  27336  rpvmasum2  27430  dchrisum0lem1  27434  dchrisum0lem2  27436  mulogsumlem  27449  mulog2sumlem3  27454  log2sumbnd  27462  selberglem1  27463  selberglem2  27464  selberg2  27469  pntlemk  27524  colinearalglem1  28840  colinearalglem2  28841  ax5seglem1  28862  axcontlem2  28899  axcontlem8  28905  numclwwlk3lem1  30318  smcnlem  30633  ipval2  30643  4ipval2  30644  ipidsq  30646  dipcj  30650  cncph  30755  ipasslem2  30768  ipasslem4  30770  ipasslem9  30774  ipasslem11  30776  hhssnv  31200  spansncol  31504  homulass  31738  lnfnmuli  31980  riesz3i  31998  circum  35668  faclim  35740  mpomulnzcnf  36294  sin2h  37611  cos2h  37612  itg2addnclem3  37674  itgaddnc  37681  iblabsnc  37685  iblmulc2nc  37686  itgmulc2nc  37689  ftc1anclem3  37696  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  dvasin  37705  cntotbnd  37797  rmxluc  42932  rmyluc  42933  jm2.17a  42956  jm2.18  42984  jm3.1lem1  43013  jm3.1lem2  43014  proot1ex  43192  lhe4.4ex1a  44325  expgrowthi  44329  expgrowth  44331  binomcxplemnotnn0  44352  dvsinax  45918  dvasinbx  45925  dvcosax  45931  stoweidlem10  46015  wallispi2lem1  46076  wallispi2  46078  fouriersw  46236  m1modmmod  47363  dfodd6  47642  opoeALTV  47688  opeoALTV  47689  2zrngnmrid  48248  sinh-conventional  49732  amgmwlem  49795