Theorem mulcl 9505

Description: Alias for ax-mulcl 9483, for naming consistency with mulcli 9530. (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 9483	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 367   e. wcel 1836  (class class class)co 6214   CCcc 9419   x. cmul 9426

This theorem was proved from axioms:  ax-mulcl 9483

This theorem is referenced by:  0cn  9517  mulid1  9522  mulcli  9530  mulcld  9545  mul31  9677  mul4  9678  mul02  9687  cnegex2  9691  muladd  9925  subdi  9926  submul2  9933  mulsub  9935  recextlem1  10114  recex  10116  muleqadd  10128  mulnzcnopr  10130  mulcan1g  10137  divass  10160  divmuldiv  10179  divmuleq  10184  divadddiv  10194  conjmul  10196  cju  10466  zneo  10880  cnref1o  11152  modcyc2  11952  muladdmodid  11956  negmod  11957  modaddmulmod  11975  expcl  12106  expclzlem  12112  mulexp  12127  sqcl  12152  subsq  12197  subsq2  12198  binom2sub  12206  binom3  12208  zesq  12210  bernneq  12213  bernneq2  12214  bcval5  12317  reim  12963  imcl  12965  crre  12968  crim  12969  remim  12971  mulre  12975  cjreb  12977  recj  12978  reneg  12979  readd  12980  remullem  12982  remul2  12984  imcj  12986  imneg  12987  imadd  12988  immul2  12991  cjadd  12995  ipcnval  12997  cjmulrcl  12998  cjneg  13001  imval2  13005  cjreim  13014  rennim  13093  cnpart  13094  sqrtneg  13122  sqabsadd  13136  sqabssub  13137  absreimsq  13146  absreim  13147  absmul  13148  sqreulem  13213  sqreu  13214  mulcn2  13439  o1mul  13458  climmul  13476  iseraltlem2  13526  prodf  13717  clim2div  13719  prodfmul  13720  prodfn0  13724  prodfrec  13725  prodfdiv  13726  prodmolem3  13761  prodmolem2a  13762  fprodcl  13780  efexp  13857  sinf  13880  cosf  13881  tanval2  13889  tanval3  13890  resinval  13891  recosval  13892  efi4p  13893  resin4p  13894  recos4p  13895  resincl  13896  recoscl  13897  sinneg  13902  cosneg  13903  efival  13908  efmival  13909  sinhval  13910  coshval  13911  retanhcl  13915  tanhlt1  13916  tanhbnd  13917  efeul  13918  sinadd  13920  cosadd  13921  sinsub  13924  cossub  13925  subsin  13927  sinmul  13928  cosmul  13929  addcos  13930  subcos  13931  cos2tsin  13935  ef01bndlem  13940  sin01bnd  13941  cos01bnd  13942  absef  13953  absefib  13954  efieq1re  13955  demoivre  13956  demoivreALT  13957  dvdscmulr  14033  dvdsmulcr  14034  odd2np1lem  14066  odd2np1  14067  gcdaddm  14188  modgcd  14195  bezoutlem1  14197  qredeq  14268  eulerthlem2  14333  modprm0  14351  opoe  14356  omoe  14357  opeo  14358  omeo  14359  pythagtriplem1  14361  pythagtriplem12  14371  pythagtriplem14  14373  iserodd  14380  gzmulcl  14477  4sqlem11  14494  4sqlem17  14500  cncrng  18571  cnfldmulg  18582  cnsubrg  18610  mulc1cncf  21513  icccvx  21554  pcorevlem  21630  itgcnlem  22300  itgneg  22314  itgconst  22329  itgadd  22335  iblabs  22339  itgmulc2  22344  dvmulbr  22446  dvmulf  22450  dvsincos  22486  plymullem1  22715  plymulcl  22722  plysubcl  22723  dgrcolem1  22774  dgrcolem2  22775  plydivlem4  22796  quotlem  22800  quotcl2  22802  quotdgr  22803  aaliou3lem3  22844  efper  22976  sinperlem  22977  sin2kpi  22980  cos2kpi  22981  efimpi  22988  sincosq1eq  23009  pige3  23014  abssinper  23015  sinkpi  23016  coskpi  23017  sineq0  23018  coseq1  23019  tanregt0  23030  efif1olem4  23036  efifo  23038  eff1olem  23039  lognegb  23081  eflogeq  23093  efiarg  23098  tanarg  23110  logf1o2  23137  cxpcl  23161  cxpne0  23164  cxpsqrtlem  23189  cxpsqrt  23190  dvcxp1  23222  root1eq1  23235  cxpeq  23237  relogbmul  23254  quad2  23305  quad  23306  dcubic2  23310  dcubic1  23311  dcubic  23312  mcubic  23313  cubic2  23314  cubic  23315  binom4  23316  dquartlem1  23317  dquartlem2  23318  dquart  23319  quart1cl  23320  quart1lem  23321  quart1  23322  quartlem1  23323  quartlem2  23324  quartlem3  23325  quart  23327  asinlem  23334  asinlem2  23335  asinlem3a  23336  asinlem3  23337  asinf  23338  atandm2  23343  atanf  23346  asinneg  23352  efiasin  23354  sinasin  23355  asinsinlem  23357  asinsin  23358  asinbnd  23365  cosasin  23370  atanneg  23373  atancj  23376  efiatan  23378  atanlogaddlem  23379  atanlogadd  23380  atanlogsublem  23381  atanlogsub  23382  efiatan2  23383  2efiatan  23384  tanatan  23385  cosatan  23387  atantan  23389  atanbndlem  23391  atans2  23397  dvatan  23401  atantayl  23403  atantayl2  23404  leibpilem1  23406  leibpilem2  23407  efrlim  23435  ftalem7  23488  basellem3  23492  basellem7  23496  basellem8  23497  basellem9  23498  ppiub  23615  dchrmulcl  23660  bposlem9  23703  lgsdir  23741  lgsdilem2  23742  lgsdi  23743  lgsne0  23744  lgsquadlem1  23765  2sqlem2  23775  rpvmasum2  23833  dchrisum0lem1  23837  dchrisum0lem2  23839  mulogsumlem  23852  mulog2sumlem3  23857  log2sumbnd  23865  selberglem1  23866  selberglem2  23867  selberg2  23872  pntlemk  23927  colinearalglem1  24351  colinearalglem2  24352  ax5seglem1  24373  axcontlem2  24410  axcontlem8  24416  numclwlk3lem3  25215  ablomul  25495  efghgrpOLD  25513  smcnlem  25745  ipval2  25755  4ipval2  25756  4ipval3  25760  ipidsq  25761  dipcj  25765  cncph  25872  ipasslem2  25885  ipasslem4  25887  ipasslem9  25891  ipasslem11  25893  hhssnv  26318  spansncol  26624  homulass  26858  lnfnmuli  27100  riesz3i  27118  zetacvg  28782  circum  29265  risefaccl  29339  fallfaccl  29340  faclim  29373  bpoly3  30009  fsumcube  30011  sin2h  30246  cos2h  30247  dvtanlemOLD  30266  itg2addnclem3  30270  itgaddnc  30277  iblabsnc  30281  iblmulc2nc  30282  itgmulc2nc  30285  ftc1anclem3  30294  ftc1anclem6  30297  ftc1anclem7  30298  ftc1anclem8  30299  ftc1anc  30300  dvcncxp1  30302  dvasin  30305  cntotbnd  30494  rmxluc  31073  rmyluc  31074  jm2.17a  31099  jm2.18  31132  jm3.1lem1  31161  jm3.1lem2  31162  proot1ex  31365  lhe4.4ex1a  31438  expgrowthi  31442  expgrowth  31444  binomcxplemnotnn0  31465  fprodclf  31796  dvsinax  31909  dvasinbx  31918  dvcosax  31924  stoweidlem10  31993  wallispi2lem1  32054  wallispi2  32056  fouriersw  32215  dfodd6  32515  opoeALTV  32560  opeoALTV  32561  2zrngnmrid  32991  m1modmmod  33369  sinh-conventional  33504  dpfrac1  33537