Theorem mulcl 11233

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099  (class class class)co 7416  ℂcc 11147   · cmul 11154

This theorem was proved from axioms:  ax-mulcl 11211

This theorem is referenced by:  mpomulf  11244  0cn  11247  mulrid  11253  mulcli  11262  mulcld  11275  mul31  11422  mul4  11423  mul02  11433  cnegex2  11437  muladd11r  11468  muladd  11687  subdi  11688  submul2  11695  mulsub  11698  recextlem1  11885  recex  11887  muleqadd  11899  mulnzcnf  11901  mulcan1g  11908  divass  11932  divmulass  11937  divmuldiv  11959  divmuleq  11964  divadddiv  11974  conjmul  11976  cju  12254  zneo  12691  cnref1o  13015  modcyc2  13921  muladdmodid  13925  negmod  13930  modaddmulmod  13952  expcl  14093  expclzlem  14097  mulexp  14115  sqcl  14131  subsq  14222  subsq2  14223  binom2sub  14232  mulbinom2  14235  binom3  14236  zesq  14238  bernneq  14241  bernneq2  14242  mulsubdivbinom2  14274  bcval5  14330  reim  15109  imcl  15111  crre  15114  crim  15115  remim  15117  mulre  15121  cjreb  15123  recj  15124  reneg  15125  readd  15126  remullem  15128  remul2  15130  imcj  15132  imneg  15133  imadd  15134  immul2  15137  cjadd  15141  ipcnval  15143  cjmulrcl  15144  cjneg  15147  imval2  15151  cjreim  15160  rennim  15239  cnpart  15240  sqrtneg  15267  sqabsadd  15282  sqabssub  15283  absreimsq  15292  absreim  15293  absmul  15294  sqreulem  15359  sqreu  15360  mulcn2  15593  o1mul  15612  climmul  15630  iseraltlem2  15682  prodf  15886  clim2div  15888  prodfmul  15889  prodfn0  15893  prodfrec  15894  prodfdiv  15895  prodmolem3  15930  prodmolem2a  15931  fprodcl  15949  fprodclf  15989  risefaccl  16012  fallfaccl  16013  bpoly3  16055  fsumcube  16057  efexp  16098  sinf  16121  cosf  16122  tanval2  16130  tanval3  16131  resinval  16132  recosval  16133  efi4p  16134  resin4p  16135  recos4p  16136  resincl  16137  recoscl  16138  sinneg  16143  cosneg  16144  efival  16149  efmival  16150  sinhval  16151  coshval  16152  retanhcl  16156  tanhlt1  16157  tanhbnd  16158  efeul  16159  sinadd  16161  cosadd  16162  sinsub  16165  cossub  16166  subsin  16168  sinmul  16169  cosmul  16170  addcos  16171  subcos  16172  cos2tsin  16176  ef01bndlem  16181  sin01bnd  16182  cos01bnd  16183  absef  16194  absefib  16195  efieq1re  16196  demoivre  16197  demoivreALT  16198  dvdscmulr  16282  dvdsmulcr  16283  odd2np1lem  16337  odd2np1  16338  opoe  16360  omoe  16361  opeo  16362  omeo  16363  gcdaddm  16520  modgcd  16528  bezoutlem1  16535  qredeq  16653  eulerthlem2  16779  modprm0  16802  pythagtriplem1  16813  pythagtriplem12  16823  pythagtriplem14  16825  iserodd  16832  gzmulcl  16935  4sqlem11  16952  4sqlem17  16958  cncrng  21376  cncrngOLD  21377  cnfldmulg  21391  cnsubrg  21420  mpomulcn  24873  mulc1cncf  24913  icccvx  24963  pcorevlem  25041  cnlmod  25155  cnstrcvs  25156  cncvs  25160  itgcnlem  25807  itgneg  25821  itgconst  25836  itgadd  25842  iblabs  25846  itgmulc2  25851  dvmulbr  25957  dvmulbrOLD  25958  dvmulf  25962  dvsincos  26001  plymullem1  26238  plymulcl  26245  plysubcl  26246  dgrcolem1  26298  dgrcolem2  26299  plydivlem4  26321  quotlem  26325  quotcl2  26327  quotdgr  26328  aaliou3lem3  26369  efper  26504  sinperlem  26505  sin2kpi  26508  cos2kpi  26509  efimpi  26516  sincosq1eq  26537  pige3ALT  26544  abssinper  26545  sinkpi  26546  coskpi  26547  sineq0  26548  coseq1  26549  tanregt0  26563  efif1olem4  26569  efifo  26571  eff1olem  26572  lognegb  26614  eflogeq  26626  efiarg  26631  tanarg  26643  logf1o2  26674  cxpcl  26698  cxpne0  26701  cxpsqrtlem  26726  cxpsqrt  26727  dvcxp1  26764  dvcncxp1  26767  root1eq1  26780  cxpeq  26782  relogbmul  26802  quad2  26864  quad  26865  dcubic2  26869  dcubic1  26870  dcubic  26871  mcubic  26872  cubic2  26873  cubic  26874  binom4  26875  dquartlem1  26876  dquartlem2  26877  dquart  26878  quart1cl  26879  quart1lem  26880  quart1  26881  quartlem1  26882  quartlem2  26883  quartlem3  26884  quart  26886  asinlem  26893  asinlem2  26894  asinlem3a  26895  asinlem3  26896  asinf  26897  atandm2  26902  atanf  26905  asinneg  26911  efiasin  26913  sinasin  26914  asinsinlem  26916  asinsin  26917  asinbnd  26924  cosasin  26929  atanneg  26932  atancj  26935  efiatan  26937  atanlogaddlem  26938  atanlogadd  26939  atanlogsublem  26940  atanlogsub  26941  efiatan2  26942  2efiatan  26943  tanatan  26944  cosatan  26946  atantan  26948  atanbndlem  26950  atans2  26956  dvatan  26960  atantayl  26962  atantayl2  26963  leibpilem2  26966  efrlim  26994  efrlimOLD  26995  zetacvg  27040  ftalem7  27104  basellem3  27108  basellem7  27112  basellem8  27113  basellem9  27114  ppiub  27230  dchrmulcl  27275  bposlem9  27318  lgsdir  27358  lgsdilem2  27359  lgsdi  27360  lgsne0  27361  lgsquadlem1  27406  2sqlem2  27444  rpvmasum2  27538  dchrisum0lem1  27542  dchrisum0lem2  27544  mulogsumlem  27557  mulog2sumlem3  27562  log2sumbnd  27570  selberglem1  27571  selberglem2  27572  selberg2  27577  pntlemk  27632  colinearalglem1  28837  colinearalglem2  28838  ax5seglem1  28859  axcontlem2  28896  axcontlem8  28902  numclwwlk3lem1  30312  smcnlem  30627  ipval2  30637  4ipval2  30638  ipidsq  30640  dipcj  30644  cncph  30749  ipasslem2  30762  ipasslem4  30764  ipasslem9  30768  ipasslem11  30770  hhssnv  31194  spansncol  31498  homulass  31732  lnfnmuli  31974  riesz3i  31992  circum  35515  faclim  35581  mpomulnzcnf  36024  sin2h  37324  cos2h  37325  itg2addnclem3  37387  itgaddnc  37394  iblabsnc  37398  iblmulc2nc  37399  itgmulc2nc  37402  ftc1anclem3  37409  ftc1anclem6  37412  ftc1anclem7  37413  ftc1anclem8  37414  ftc1anc  37415  dvasin  37418  cntotbnd  37510  fac2xp3  41947  rmxluc  42631  rmyluc  42632  jm2.17a  42655  jm2.18  42683  jm3.1lem1  42712  jm3.1lem2  42713  proot1ex  42898  lhe4.4ex1a  44040  expgrowthi  44044  expgrowth  44046  binomcxplemnotnn0  44067  dvsinax  45570  dvasinbx  45577  dvcosax  45583  stoweidlem10  45667  wallispi2lem1  45728  wallispi2  45730  fouriersw  45888  dfodd6  47245  opoeALTV  47291  opeoALTV  47292  2zrngnmrid  47669  m1modmmod  47945  sinh-conventional  48521  amgmwlem  48586