Theorem mulcl 11122

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

This theorem was proved from axioms:  ax-mulcl 11100

This theorem is referenced by:  mpomulf  11133  0cn  11136  mulrid  11142  mulcli  11151  mulcld  11164  mul31  11312  mul4  11313  mul02  11323  cnegex2  11327  muladd11r  11358  muladd  11581  subdi  11582  submul2  11589  mulsub  11592  recextlem1  11779  recex  11781  muleqadd  11793  mulnzcnf  11795  mulcan1g  11802  divass  11826  divmulass  11831  divmuldiv  11853  divmuleq  11858  divadddiv  11868  conjmul  11870  cju  12153  zneo  12587  cnref1o  12910  modcyc2  13839  muladdmodid  13845  negmod  13851  modaddmulmod  13873  expcl  14014  expclzlem  14018  mulexp  14036  sqcl  14053  subsq  14145  subsq2  14146  binom2sub  14155  mulbinom2  14158  binom3  14159  zesq  14161  bernneq  14164  bernneq2  14165  mulsubdivbinom2  14197  bcval5  14253  reim  15044  imcl  15046  crre  15049  crim  15050  remim  15052  mulre  15056  cjreb  15058  recj  15059  reneg  15060  readd  15061  remullem  15063  remul2  15065  imcj  15067  imneg  15068  imadd  15069  immul2  15072  cjadd  15076  ipcnval  15078  cjmulrcl  15079  cjneg  15082  imval2  15086  cjreim  15095  rennim  15174  cnpart  15175  sqrtneg  15202  sqabsadd  15217  sqabssub  15218  absreimsq  15227  absreim  15228  absmul  15229  sqreulem  15295  sqreu  15296  mulcn2  15531  o1mul  15550  climmul  15568  iseraltlem2  15618  prodf  15822  clim2div  15824  prodfmul  15825  prodfn0  15829  prodfrec  15830  prodfdiv  15831  prodmolem3  15868  prodmolem2a  15869  fprodcl  15887  fprodclf  15927  risefaccl  15950  fallfaccl  15951  bpoly3  15993  fsumcube  15995  efexp  16038  sinf  16061  cosf  16062  tanval2  16070  tanval3  16071  resinval  16072  recosval  16073  efi4p  16074  resin4p  16075  recos4p  16076  resincl  16077  recoscl  16078  sinneg  16083  cosneg  16084  efival  16089  efmival  16090  sinhval  16091  coshval  16092  retanhcl  16096  tanhlt1  16097  tanhbnd  16098  efeul  16099  sinadd  16101  cosadd  16102  sinsub  16105  cossub  16106  subsin  16108  sinmul  16109  cosmul  16110  addcos  16111  subcos  16112  cos2tsin  16116  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  absef  16134  absefib  16135  efieq1re  16136  demoivre  16137  demoivreALT  16138  dvdscmulr  16223  dvdsmulcr  16224  odd2np1lem  16279  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  gcdaddm  16464  modgcd  16471  bezoutlem1  16478  qredeq  16596  eulerthlem2  16721  modprm0  16745  pythagtriplem1  16756  pythagtriplem12  16766  pythagtriplem14  16768  iserodd  16775  gzmulcl  16878  4sqlem11  16895  4sqlem17  16901  cncrng  21355  cncrngOLD  21356  cnfldmulg  21370  cnsubrg  21394  mpomulcn  24826  mulc1cncf  24866  icccvx  24916  pcorevlem  24994  cnlmod  25108  cnstrcvs  25109  cncvs  25113  itgcnlem  25759  itgneg  25773  itgconst  25788  itgadd  25794  iblabs  25798  itgmulc2  25803  dvmulbr  25909  dvmulbrOLD  25910  dvmulf  25914  dvsincos  25953  plymullem1  26187  plymulcl  26194  plysubcl  26195  dgrcolem1  26247  dgrcolem2  26248  plydivlem4  26272  quotlem  26276  quotcl2  26278  quotdgr  26279  aaliou3lem3  26320  efper  26456  sinperlem  26457  sin2kpi  26460  cos2kpi  26461  efimpi  26468  sincosq1eq  26489  pige3ALT  26497  abssinper  26498  sinkpi  26499  coskpi  26500  sineq0  26501  coseq1  26502  tanregt0  26516  efif1olem4  26522  efifo  26524  eff1olem  26525  lognegb  26567  eflogeq  26579  efiarg  26584  tanarg  26596  logf1o2  26627  cxpcl  26651  cxpne0  26654  cxpsqrtlem  26679  cxpsqrt  26680  dvcxp1  26717  dvcncxp1  26720  root1eq1  26733  cxpeq  26735  relogbmul  26755  quad2  26817  quad  26818  dcubic2  26822  dcubic1  26823  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  binom4  26828  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem1  26835  quartlem2  26836  quartlem3  26837  quart  26839  asinlem  26846  asinlem2  26847  asinlem3a  26848  asinlem3  26849  asinf  26850  atandm2  26855  atanf  26858  asinneg  26864  efiasin  26866  sinasin  26867  asinsinlem  26869  asinsin  26870  asinbnd  26877  cosasin  26882  atanneg  26885  atancj  26888  efiatan  26890  atanlogaddlem  26891  atanlogadd  26892  atanlogsublem  26893  atanlogsub  26894  efiatan2  26895  2efiatan  26896  tanatan  26897  cosatan  26899  atantan  26901  atanbndlem  26903  atans2  26909  dvatan  26913  atantayl  26915  atantayl2  26916  leibpilem2  26919  efrlim  26947  efrlimOLD  26948  zetacvg  26993  ftalem7  27057  basellem3  27061  basellem7  27065  basellem8  27066  basellem9  27067  ppiub  27183  dchrmulcl  27228  bposlem9  27271  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  lgsquadlem1  27359  2sqlem2  27397  rpvmasum2  27491  dchrisum0lem1  27495  dchrisum0lem2  27497  mulogsumlem  27510  mulog2sumlem3  27515  log2sumbnd  27523  selberglem1  27524  selberglem2  27525  selberg2  27530  pntlemk  27585  colinearalglem1  28991  colinearalglem2  28992  ax5seglem1  29013  axcontlem2  29050  axcontlem8  29056  numclwwlk3lem1  30469  smcnlem  30784  ipval2  30794  4ipval2  30795  ipidsq  30797  dipcj  30801  cncph  30906  ipasslem2  30919  ipasslem4  30921  ipasslem9  30925  ipasslem11  30927  hhssnv  31351  spansncol  31655  homulass  31889  lnfnmuli  32131  riesz3i  32149  circum  35887  faclim  35959  mpomulnzcnf  36512  sin2h  37855  cos2h  37856  itg2addnclem3  37918  itgaddnc  37925  iblabsnc  37929  iblmulc2nc  37930  itgmulc2nc  37933  ftc1anclem3  37940  ftc1anclem6  37943  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  dvasin  37949  cntotbnd  38041  rmxluc  43287  rmyluc  43288  jm2.17a  43311  jm2.18  43339  jm3.1lem1  43368  jm3.1lem2  43369  proot1ex  43547  lhe4.4ex1a  44679  expgrowthi  44683  expgrowth  44685  binomcxplemnotnn0  44706  dvsinax  46265  dvasinbx  46272  dvcosax  46278  stoweidlem10  46362  wallispi2lem1  46423  wallispi2  46425  fouriersw  46583  sinnpoly  47245  m1modmmod  47712  dfodd6  47991  opoeALTV  48037  opeoALTV  48038  2zrngnmrid  48610  sinh-conventional  50092  amgmwlem  50155