Theorem mulcl 9030

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

Assertion

Ref	Expression
mulcl	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 9008	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721  (class class class)co 6040   CCcc 8944   x. cmul 8951

This theorem is referenced by:  0cn  9040  mulid1  9044  mulcli  9051  mulcld  9064  mul31  9190  mul4  9191  mul02  9200  cnegex2  9204  muladd  9422  subdi  9423  submul2  9430  mulsub  9432  recextlem1  9608  recex  9610  muleqadd  9622  mulnzcnopr  9624  divass  9652  divmuldiv  9670  divmuleq  9675  divadddiv  9685  conjmul  9687  cju  9952  zneo  10308  cnref1o  10563  modcyc2  11232  expcl  11354  expclzlem  11360  mulexp  11374  sqcl  11399  subsq  11443  subsq2  11444  binom2sub  11453  binom3  11455  zesq  11457  bernneq  11460  bernneq2  11461  bcval5  11564  reim  11869  imcl  11871  crre  11874  crim  11875  remim  11877  mulre  11881  cjreb  11883  recj  11884  reneg  11885  readd  11886  remullem  11888  remul2  11890  imcj  11892  imneg  11893  imadd  11894  immul2  11897  cjadd  11901  ipcnval  11903  cjmulrcl  11904  cjneg  11907  imval2  11911  cjreim  11920  rennim  11999  cnpart  12000  sqrneg  12028  sqabsadd  12042  sqabssub  12043  absreimsq  12052  absreim  12053  absmul  12054  sqreulem  12118  sqreu  12119  mulcn2  12344  o1mul  12363  climmul  12381  iseraltlem2  12431  efexp  12657  sinf  12680  cosf  12681  tanval2  12689  tanval3  12690  resinval  12691  recosval  12692  efi4p  12693  resin4p  12694  recos4p  12695  resincl  12696  recoscl  12697  sinneg  12702  cosneg  12703  efival  12708  efmival  12709  sinhval  12710  coshval  12711  retanhcl  12715  tanhlt1  12716  tanhbnd  12717  efeul  12718  sinadd  12720  cosadd  12721  sinsub  12724  cossub  12725  subsin  12727  sinmul  12728  cosmul  12729  addcos  12730  subcos  12731  cos2tsin  12735  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  absef  12753  absefib  12754  efieq1re  12755  demoivre  12756  demoivreALT  12757  dvdscmulr  12833  dvdsmulcr  12834  odd2np1lem  12862  odd2np1  12863  gcdaddm  12984  modgcd  12991  bezoutlem1  12993  qredeq  13061  eulerthlem2  13126  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pythagtriplem1  13145  pythagtriplem12  13155  pythagtriplem14  13157  iserodd  13164  gzmulcl  13261  4sqlem11  13278  4sqlem17  13284  cncrng  16677  cnfldmulg  16688  cnsubrg  16714  mulc1cncf  18888  icccvx  18928  pcorevlem  19004  itgcnlem  19634  itgneg  19648  itgconst  19663  itgadd  19669  iblabs  19673  itgmulc2  19678  dvmulbr  19778  dvmulf  19782  dvsincos  19818  plymullem1  20086  plymulcl  20093  plysubcl  20094  dgrcolem1  20144  dgrcolem2  20145  plydivlem4  20166  quotlem  20170  quotcl2  20172  quotdgr  20173  aaliou3lem3  20214  efper  20340  sinperlem  20341  sin2kpi  20344  cos2kpi  20345  efimpi  20352  sincosq1eq  20373  pige3  20378  abssinper  20379  sinkpi  20380  coskpi  20381  sineq0  20382  coseq1  20383  tanregt0  20394  efgh  20396  efif1olem4  20400  efifo  20402  eff1olem  20403  lognegb  20437  eflogeq  20449  efiarg  20455  tanarg  20467  logf1o2  20494  cxpcl  20518  cxpne0  20521  cxpsqrlem  20546  cxpsqr  20547  dvcxp1  20579  root1eq1  20592  cxpeq  20594  quad2  20632  quad  20633  dcubic2  20637  dcubic1  20638  dcubic  20639  mcubic  20640  cubic2  20641  cubic  20642  binom4  20643  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1cl  20647  quart1lem  20648  quart1  20649  quartlem1  20650  quartlem2  20651  quartlem3  20652  quart  20654  asinlem  20661  asinlem2  20662  asinlem3a  20663  asinlem3  20664  asinf  20665  atandm2  20670  atanf  20673  asinneg  20679  efiasin  20681  sinasin  20682  asinsinlem  20684  asinsin  20685  asinbnd  20692  cosasin  20697  atanneg  20700  atancj  20703  efiatan  20705  atanlogaddlem  20706  atanlogadd  20707  atanlogsublem  20708  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  cosatan  20714  atantan  20716  atanbndlem  20718  atans2  20724  dvatan  20728  atantayl  20730  atantayl2  20731  leibpilem1  20733  leibpilem2  20734  efrlim  20761  ftalem7  20814  basellem3  20818  basellem7  20822  basellem8  20823  basellem9  20824  ppiub  20941  dchrmulcl  20986  bposlem9  21029  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgsquadlem1  21091  2sqlem2  21101  rpvmasum2  21159  dchrisum0lem1  21163  dchrisum0lem2  21165  mulogsumlem  21178  mulog2sumlem3  21183  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  selberg2  21198  pntlemk  21253  ablomul  21896  efghgrp  21914  smcnlem  22146  ipval2  22156  4ipval2  22157  4ipval3  22161  ipidsq  22162  dipcj  22166  cncph  22273  ipasslem2  22286  ipasslem4  22288  ipasslem9  22292  ipasslem11  22294  hhssnv  22717  spansncol  23023  homulass  23258  lnfnmuli  23500  riesz3i  23518  zetacvg  24752  circum  25064  mulcan1g  25142  prodf  25168  clim2div  25170  prodfmul  25171  prodfn0  25175  prodfrec  25176  prodfdiv  25177  prodmolem3  25212  prodmolem2a  25213  fprodcl  25231  risefaccl  25283  fallfaccl  25284  faclim  25313  colinearalglem1  25749  colinearalglem2  25750  ax5seglem1  25771  axcontlem2  25808  axcontlem8  25814  bpoly3  26008  fsumcube  26010  itg2addnclem3  26157  itgaddnc  26164  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nc  26172  cntotbnd  26395  rmxluc  26889  rmyluc  26890  jm2.17a  26915  jm2.18  26949  jm3.1lem1  26978  jm3.1lem2  26979  proot1ex  27388  lhe4.4ex1a  27414  expgrowthi  27418  expgrowth  27420  stoweidlem10  27626  wallispi2lem1  27687  wallispi2  27689  sinh-conventional  28196  dpfrac1  28229

This theorem was proved from axioms:  ax-mulcl 9008