Theorem mulcl 10472

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2081  (class class class)co 7021  ℂcc 10386   · cmul 10393

This theorem was proved from axioms:  ax-mulcl 10450

This theorem is referenced by:  0cn  10484  mulid1  10490  mulcli  10499  mulcld  10512  mul31  10659  mul4  10660  mul02  10670  cnegex2  10674  muladd11r  10705  muladd  10925  subdi  10926  submul2  10933  mulsub  10936  recextlem1  11123  recex  11125  muleqadd  11137  mulnzcnopr  11139  mulcan1g  11146  divass  11169  divmulass  11174  divmuldiv  11193  divmuleq  11198  divadddiv  11208  conjmul  11210  cju  11487  zneo  11919  cnref1o  12239  modcyc2  13130  muladdmodid  13134  negmod  13139  modaddmulmod  13161  expcl  13302  expclzlem  13308  mulexp  13323  sqcl  13339  subsq  13427  subsq2  13428  binom2sub  13436  mulbinom2  13439  binom3  13440  zesq  13442  bernneq  13445  bernneq2  13446  mulsubdivbinom2  13477  bcval5  13533  reim  14307  imcl  14309  crre  14312  crim  14313  remim  14315  mulre  14319  cjreb  14321  recj  14322  reneg  14323  readd  14324  remullem  14326  remul2  14328  imcj  14330  imneg  14331  imadd  14332  immul2  14335  cjadd  14339  ipcnval  14341  cjmulrcl  14342  cjneg  14345  imval2  14349  cjreim  14358  rennim  14437  cnpart  14438  sqrtneg  14466  sqabsadd  14481  sqabssub  14482  absreimsq  14491  absreim  14492  absmul  14493  sqreulem  14558  sqreu  14559  mulcn2  14791  o1mul  14810  climmul  14828  iseraltlem2  14878  prodf  15081  clim2div  15083  prodfmul  15084  prodfn0  15088  prodfrec  15089  prodfdiv  15090  prodmolem3  15125  prodmolem2a  15126  fprodcl  15144  fprodclf  15184  risefaccl  15207  fallfaccl  15208  bpoly3  15250  fsumcube  15252  efexp  15292  sinf  15315  cosf  15316  tanval2  15324  tanval3  15325  resinval  15326  recosval  15327  efi4p  15328  resin4p  15329  recos4p  15330  resincl  15331  recoscl  15332  sinneg  15337  cosneg  15338  efival  15343  efmival  15344  sinhval  15345  coshval  15346  retanhcl  15350  tanhlt1  15351  tanhbnd  15352  efeul  15353  sinadd  15355  cosadd  15356  sinsub  15359  cossub  15360  subsin  15362  sinmul  15363  cosmul  15364  addcos  15365  subcos  15366  cos2tsin  15370  ef01bndlem  15375  sin01bnd  15376  cos01bnd  15377  absef  15388  absefib  15389  efieq1re  15390  demoivre  15391  demoivreALT  15392  dvdscmulr  15476  dvdsmulcr  15477  odd2np1lem  15527  odd2np1  15528  opoe  15550  omoe  15551  opeo  15552  omeo  15553  gcdaddm  15711  modgcd  15718  bezoutlem1  15721  qredeq  15835  eulerthlem2  15953  modprm0  15976  pythagtriplem1  15987  pythagtriplem12  15997  pythagtriplem14  15999  iserodd  16006  gzmulcl  16108  4sqlem11  16125  4sqlem17  16131  cncrng  20253  cnfldmulg  20264  cnsubrg  20292  mulc1cncf  23201  icccvx  23242  pcorevlem  23318  cnlmod  23432  cnstrcvs  23433  cncvs  23437  itgcnlem  24078  itgneg  24092  itgconst  24107  itgadd  24113  iblabs  24117  itgmulc2  24122  dvmulbr  24224  dvmulf  24228  dvsincos  24266  plymullem1  24492  plymulcl  24499  plysubcl  24500  dgrcolem1  24551  dgrcolem2  24552  plydivlem4  24573  quotlem  24577  quotcl2  24579  quotdgr  24580  aaliou3lem3  24621  efper  24753  sinperlem  24754  sin2kpi  24757  cos2kpi  24758  efimpi  24765  sincosq1eq  24786  pige3ALT  24793  abssinper  24794  sinkpi  24795  coskpi  24796  sineq0  24797  coseq1  24798  tanregt0  24809  efif1olem4  24815  efifo  24817  eff1olem  24818  lognegb  24859  eflogeq  24871  efiarg  24876  tanarg  24888  logf1o2  24919  cxpcl  24943  cxpne0  24946  cxpsqrtlem  24971  cxpsqrt  24972  dvcxp1  25007  dvcncxp1  25010  root1eq1  25022  cxpeq  25024  relogbmul  25041  quad2  25103  quad  25104  dcubic2  25108  dcubic1  25109  dcubic  25110  mcubic  25111  cubic2  25112  cubic  25113  binom4  25114  dquartlem1  25115  dquartlem2  25116  dquart  25117  quart1cl  25118  quart1lem  25119  quart1  25120  quartlem1  25121  quartlem2  25122  quartlem3  25123  quart  25125  asinlem  25132  asinlem2  25133  asinlem3a  25134  asinlem3  25135  asinf  25136  atandm2  25141  atanf  25144  asinneg  25150  efiasin  25152  sinasin  25153  asinsinlem  25155  asinsin  25156  asinbnd  25163  cosasin  25168  atanneg  25171  atancj  25174  efiatan  25176  atanlogaddlem  25177  atanlogadd  25178  atanlogsublem  25179  atanlogsub  25180  efiatan2  25181  2efiatan  25182  tanatan  25183  cosatan  25185  atantan  25187  atanbndlem  25189  atans2  25195  dvatan  25199  atantayl  25201  atantayl2  25202  leibpilem1OLD  25205  leibpilem2  25206  efrlim  25234  zetacvg  25279  ftalem7  25343  basellem3  25347  basellem7  25351  basellem8  25352  basellem9  25353  ppiub  25467  dchrmulcl  25512  bposlem9  25555  lgsdir  25595  lgsdilem2  25596  lgsdi  25597  lgsne0  25598  lgsquadlem1  25643  2sqlem2  25681  rpvmasum2  25775  dchrisum0lem1  25779  dchrisum0lem2  25781  mulogsumlem  25794  mulog2sumlem3  25799  log2sumbnd  25807  selberglem1  25808  selberglem2  25809  selberg2  25814  pntlemk  25869  colinearalglem1  26380  colinearalglem2  26381  ax5seglem1  26402  axcontlem2  26439  axcontlem8  26445  numclwwlk3lem1  27858  smcnlem  28170  ipval2  28180  4ipval2  28181  ipidsq  28183  dipcj  28187  cncph  28292  ipasslem2  28305  ipasslem4  28307  ipasslem9  28311  ipasslem11  28313  hhssnv  28737  spansncol  29041  homulass  29275  lnfnmuli  29517  riesz3i  29535  circum  32532  faclim  32593  sin2h  34439  cos2h  34440  itg2addnclem3  34502  itgaddnc  34509  iblabsnc  34513  iblmulc2nc  34514  itgmulc2nc  34517  ftc1anclem3  34526  ftc1anclem6  34529  ftc1anclem7  34530  ftc1anclem8  34531  ftc1anc  34532  dvasin  34535  cntotbnd  34632  rmxluc  39044  rmyluc  39045  jm2.17a  39068  jm2.18  39096  jm3.1lem1  39125  jm3.1lem2  39126  proot1ex  39312  lhe4.4ex1a  40225  expgrowthi  40229  expgrowth  40231  binomcxplemnotnn0  40252  dvsinax  41765  dvasinbx  41773  dvcosax  41779  stoweidlem10  41864  wallispi2lem1  41925  wallispi2  41927  fouriersw  42085  dfodd6  43311  opoeALTV  43357  opeoALTV  43358  2zrngnmrid  43726  m1modmmod  44089  sinh-conventional  44345  amgmwlem  44410