Theorem mulcl 11135

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  (class class class)co 7357  ℂcc 11049   · cmul 11056

This theorem was proved from axioms:  ax-mulcl 11113

This theorem is referenced by:  0cn  11147  mulid1  11153  mulcli  11162  mulcld  11175  mul31  11322  mul4  11323  mul02  11333  cnegex2  11337  muladd11r  11368  muladd  11587  subdi  11588  submul2  11595  mulsub  11598  recextlem1  11785  recex  11787  muleqadd  11799  mulnzcnopr  11801  mulcan1g  11808  divass  11831  divmulass  11836  divmuldiv  11855  divmuleq  11860  divadddiv  11870  conjmul  11872  cju  12149  zneo  12586  cnref1o  12910  modcyc2  13812  muladdmodid  13816  negmod  13821  modaddmulmod  13843  expcl  13985  expclzlem  13989  mulexp  14007  sqcl  14023  subsq  14114  subsq2  14115  binom2sub  14123  mulbinom2  14126  binom3  14127  zesq  14129  bernneq  14132  bernneq2  14133  mulsubdivbinom2  14162  bcval5  14218  reim  14994  imcl  14996  crre  14999  crim  15000  remim  15002  mulre  15006  cjreb  15008  recj  15009  reneg  15010  readd  15011  remullem  15013  remul2  15015  imcj  15017  imneg  15018  imadd  15019  immul2  15022  cjadd  15026  ipcnval  15028  cjmulrcl  15029  cjneg  15032  imval2  15036  cjreim  15045  rennim  15124  cnpart  15125  sqrtneg  15152  sqabsadd  15167  sqabssub  15168  absreimsq  15177  absreim  15178  absmul  15179  sqreulem  15244  sqreu  15245  mulcn2  15478  o1mul  15497  climmul  15515  iseraltlem2  15567  prodf  15772  clim2div  15774  prodfmul  15775  prodfn0  15779  prodfrec  15780  prodfdiv  15781  prodmolem3  15816  prodmolem2a  15817  fprodcl  15835  fprodclf  15875  risefaccl  15898  fallfaccl  15899  bpoly3  15941  fsumcube  15943  efexp  15983  sinf  16006  cosf  16007  tanval2  16015  tanval3  16016  resinval  16017  recosval  16018  efi4p  16019  resin4p  16020  recos4p  16021  resincl  16022  recoscl  16023  sinneg  16028  cosneg  16029  efival  16034  efmival  16035  sinhval  16036  coshval  16037  retanhcl  16041  tanhlt1  16042  tanhbnd  16043  efeul  16044  sinadd  16046  cosadd  16047  sinsub  16050  cossub  16051  subsin  16053  sinmul  16054  cosmul  16055  addcos  16056  subcos  16057  cos2tsin  16061  ef01bndlem  16066  sin01bnd  16067  cos01bnd  16068  absef  16079  absefib  16080  efieq1re  16081  demoivre  16082  demoivreALT  16083  dvdscmulr  16167  dvdsmulcr  16168  odd2np1lem  16222  odd2np1  16223  opoe  16245  omoe  16246  opeo  16247  omeo  16248  gcdaddm  16405  modgcd  16413  bezoutlem1  16420  qredeq  16533  eulerthlem2  16654  modprm0  16677  pythagtriplem1  16688  pythagtriplem12  16698  pythagtriplem14  16700  iserodd  16707  gzmulcl  16810  4sqlem11  16827  4sqlem17  16833  cncrng  20818  cnfldmulg  20829  cnsubrg  20857  mulc1cncf  24268  icccvx  24313  pcorevlem  24389  cnlmod  24503  cnstrcvs  24504  cncvs  24508  itgcnlem  25154  itgneg  25168  itgconst  25183  itgadd  25189  iblabs  25193  itgmulc2  25198  dvmulbr  25303  dvmulf  25307  dvsincos  25345  plymullem1  25575  plymulcl  25582  plysubcl  25583  dgrcolem1  25634  dgrcolem2  25635  plydivlem4  25656  quotlem  25660  quotcl2  25662  quotdgr  25663  aaliou3lem3  25704  efper  25836  sinperlem  25837  sin2kpi  25840  cos2kpi  25841  efimpi  25848  sincosq1eq  25869  pige3ALT  25876  abssinper  25877  sinkpi  25878  coskpi  25879  sineq0  25880  coseq1  25881  tanregt0  25895  efif1olem4  25901  efifo  25903  eff1olem  25904  lognegb  25945  eflogeq  25957  efiarg  25962  tanarg  25974  logf1o2  26005  cxpcl  26029  cxpne0  26032  cxpsqrtlem  26057  cxpsqrt  26058  dvcxp1  26093  dvcncxp1  26096  root1eq1  26108  cxpeq  26110  relogbmul  26127  quad2  26189  quad  26190  dcubic2  26194  dcubic1  26195  dcubic  26196  mcubic  26197  cubic2  26198  cubic  26199  binom4  26200  dquartlem1  26201  dquartlem2  26202  dquart  26203  quart1cl  26204  quart1lem  26205  quart1  26206  quartlem1  26207  quartlem2  26208  quartlem3  26209  quart  26211  asinlem  26218  asinlem2  26219  asinlem3a  26220  asinlem3  26221  asinf  26222  atandm2  26227  atanf  26230  asinneg  26236  efiasin  26238  sinasin  26239  asinsinlem  26241  asinsin  26242  asinbnd  26249  cosasin  26254  atanneg  26257  atancj  26260  efiatan  26262  atanlogaddlem  26263  atanlogadd  26264  atanlogsublem  26265  atanlogsub  26266  efiatan2  26267  2efiatan  26268  tanatan  26269  cosatan  26271  atantan  26273  atanbndlem  26275  atans2  26281  dvatan  26285  atantayl  26287  atantayl2  26288  leibpilem2  26291  efrlim  26319  zetacvg  26364  ftalem7  26428  basellem3  26432  basellem7  26436  basellem8  26437  basellem9  26438  ppiub  26552  dchrmulcl  26597  bposlem9  26640  lgsdir  26680  lgsdilem2  26681  lgsdi  26682  lgsne0  26683  lgsquadlem1  26728  2sqlem2  26766  rpvmasum2  26860  dchrisum0lem1  26864  dchrisum0lem2  26866  mulogsumlem  26879  mulog2sumlem3  26884  log2sumbnd  26892  selberglem1  26893  selberglem2  26894  selberg2  26899  pntlemk  26954  colinearalglem1  27855  colinearalglem2  27856  ax5seglem1  27877  axcontlem2  27914  axcontlem8  27920  numclwwlk3lem1  29326  smcnlem  29639  ipval2  29649  4ipval2  29650  ipidsq  29652  dipcj  29656  cncph  29761  ipasslem2  29774  ipasslem4  29776  ipasslem9  29780  ipasslem11  29782  hhssnv  30206  spansncol  30510  homulass  30744  lnfnmuli  30986  riesz3i  31004  circum  34262  faclim  34319  sin2h  36068  cos2h  36069  itg2addnclem3  36131  itgaddnc  36138  iblabsnc  36142  iblmulc2nc  36143  itgmulc2nc  36146  ftc1anclem3  36153  ftc1anclem6  36156  ftc1anclem7  36157  ftc1anclem8  36158  ftc1anc  36159  dvasin  36162  cntotbnd  36255  fac2xp3  40612  rmxluc  41246  rmyluc  41247  jm2.17a  41270  jm2.18  41298  jm3.1lem1  41327  jm3.1lem2  41328  proot1ex  41514  lhe4.4ex1a  42599  expgrowthi  42603  expgrowth  42605  binomcxplemnotnn0  42626  dvsinax  44144  dvasinbx  44151  dvcosax  44157  stoweidlem10  44241  wallispi2lem1  44302  wallispi2  44304  fouriersw  44462  dfodd6  45819  opoeALTV  45865  opeoALTV  45866  2zrngnmrid  46238  m1modmmod  46597  sinh-conventional  47174  amgmwlem  47239