Theorem mulcl 9649

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

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898  (class class class)co 6315   CCcc 9563   x. cmul 9570

This theorem was proved from axioms:  ax-mulcl 9627

This theorem is referenced by:  0cn  9661  mulid1  9666  mulcli  9674  mulcld  9689  mul31  9827  mul4  9828  mul02  9837  cnegex2  9841  muladd  10079  subdi  10080  submul2  10087  mulsub  10089  recextlem1  10270  recex  10272  muleqadd  10284  mulnzcnopr  10286  mulcan1g  10293  divass  10316  divmuldiv  10335  divmuleq  10340  divadddiv  10350  conjmul  10352  cju  10633  zneo  11047  cnref1o  11326  modcyc2  12165  muladdmodid  12169  negmod  12170  modaddmulmod  12188  expcl  12322  expclzlem  12328  mulexp  12343  sqcl  12369  subsq  12414  subsq2  12415  binom2sub  12423  binom3  12425  zesq  12427  bernneq  12430  bernneq2  12431  bcval5  12535  reim  13221  imcl  13223  crre  13226  crim  13227  remim  13229  mulre  13233  cjreb  13235  recj  13236  reneg  13237  readd  13238  remullem  13240  remul2  13242  imcj  13244  imneg  13245  imadd  13246  immul2  13249  cjadd  13253  ipcnval  13255  cjmulrcl  13256  cjneg  13259  imval2  13263  cjreim  13272  rennim  13351  cnpart  13352  sqrtneg  13380  sqabsadd  13394  sqabssub  13395  absreimsq  13404  absreim  13405  absmul  13406  sqreulem  13471  sqreu  13472  mulcn2  13708  o1mul  13727  climmul  13745  iseraltlem2  13798  prodf  13992  clim2div  13994  prodfmul  13995  prodfn0  13999  prodfrec  14000  prodfdiv  14001  prodmolem3  14036  prodmolem2a  14037  fprodcl  14055  fprodclf  14095  risefaccl  14117  fallfaccl  14118  bpoly3  14160  fsumcube  14162  efexp  14204  sinf  14227  cosf  14228  tanval2  14236  tanval3  14237  resinval  14238  recosval  14239  efi4p  14240  resin4p  14241  recos4p  14242  resincl  14243  recoscl  14244  sinneg  14249  cosneg  14250  efival  14255  efmival  14256  sinhval  14257  coshval  14258  retanhcl  14262  tanhlt1  14263  tanhbnd  14264  efeul  14265  sinadd  14267  cosadd  14268  sinsub  14271  cossub  14272  subsin  14274  sinmul  14275  cosmul  14276  addcos  14277  subcos  14278  cos2tsin  14282  ef01bndlem  14287  sin01bnd  14288  cos01bnd  14289  absef  14300  absefib  14301  efieq1re  14302  demoivre  14303  demoivreALT  14304  dvdscmulr  14380  dvdsmulcr  14381  odd2np1lem  14413  odd2np1  14414  gcdaddm  14542  modgcd  14549  bezoutlem1  14552  qredeq  14712  eulerthlem2  14779  modprm0  14805  opoe  14810  omoe  14811  opeo  14812  omeo  14813  pythagtriplem1  14815  pythagtriplem12  14825  pythagtriplem14  14827  iserodd  14834  gzmulcl  14931  4sqlem11  14948  4sqlem17OLD  14954  4sqlem17  14960  cncrng  19038  cnfldmulg  19049  cnsubrg  19077  mulc1cncf  21986  icccvx  22027  pcorevlem  22106  itgcnlem  22796  itgneg  22810  itgconst  22825  itgadd  22831  iblabs  22835  itgmulc2  22840  dvmulbr  22942  dvmulf  22946  dvsincos  22982  plymullem1  23217  plymulcl  23224  plysubcl  23225  dgrcolem1  23276  dgrcolem2  23277  plydivlem4  23298  quotlem  23302  quotcl2  23304  quotdgr  23305  aaliou3lem3  23349  efper  23483  sinperlem  23484  sin2kpi  23487  cos2kpi  23488  efimpi  23495  sincosq1eq  23516  pige3  23521  abssinper  23522  sinkpi  23523  coskpi  23524  sineq0  23525  coseq1  23526  tanregt0  23537  efif1olem4  23543  efifo  23545  eff1olem  23546  lognegb  23588  eflogeq  23600  efiarg  23605  tanarg  23617  logf1o2  23644  cxpcl  23668  cxpne0  23671  cxpsqrtlem  23696  cxpsqrt  23697  dvcxp1  23729  dvcncxp1  23732  root1eq1  23744  cxpeq  23746  relogbmul  23763  quad2  23814  quad  23815  dcubic2  23819  dcubic1  23820  dcubic  23821  mcubic  23822  cubic2  23823  cubic  23824  binom4  23825  dquartlem1  23826  dquartlem2  23827  dquart  23828  quart1cl  23829  quart1lem  23830  quart1  23831  quartlem1  23832  quartlem2  23833  quartlem3  23834  quart  23836  asinlem  23843  asinlem2  23844  asinlem3a  23845  asinlem3  23846  asinf  23847  atandm2  23852  atanf  23855  asinneg  23861  efiasin  23863  sinasin  23864  asinsinlem  23866  asinsin  23867  asinbnd  23874  cosasin  23879  atanneg  23882  atancj  23885  efiatan  23887  atanlogaddlem  23888  atanlogadd  23889  atanlogsublem  23890  atanlogsub  23891  efiatan2  23892  2efiatan  23893  tanatan  23894  cosatan  23896  atantan  23898  atanbndlem  23900  atans2  23906  dvatan  23910  atantayl  23912  atantayl2  23913  leibpilem1  23915  leibpilem2  23916  efrlim  23944  zetacvg  23989  ftalem7  24054  basellem3  24058  basellem7  24062  basellem8  24063  basellem9  24064  ppiub  24181  dchrmulcl  24226  bposlem9  24269  lgsdir  24307  lgsdilem2  24308  lgsdi  24309  lgsne0  24310  lgsquadlem1  24331  2sqlem2  24341  rpvmasum2  24399  dchrisum0lem1  24403  dchrisum0lem2  24405  mulogsumlem  24418  mulog2sumlem3  24423  log2sumbnd  24431  selberglem1  24432  selberglem2  24433  selberg2  24438  pntlemk  24493  colinearalglem1  24985  colinearalglem2  24986  ax5seglem1  25007  axcontlem2  25044  axcontlem8  25050  numclwlk3lem3  25850  ablomul  26132  efghgrpOLD  26150  smcnlem  26382  ipval2  26392  4ipval2  26393  4ipval3  26397  ipidsq  26398  dipcj  26402  cncph  26509  ipasslem2  26522  ipasslem4  26524  ipasslem9  26528  ipasslem11  26530  hhssnv  26964  spansncol  27270  homulass  27504  lnfnmuli  27746  riesz3i  27764  circum  30367  faclim  30431  sin2h  31980  cos2h  31981  dvtanlemOLD  32036  itg2addnclem3  32040  itgaddnc  32047  iblabsnc  32051  iblmulc2nc  32052  itgmulc2nc  32055  ftc1anclem3  32064  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  dvasin  32073  cntotbnd  32173  rmxluc  35829  rmyluc  35830  jm2.17a  35855  jm2.18  35888  jm3.1lem1  35917  jm3.1lem2  35918  proot1ex  36123  lhe4.4ex1a  36722  expgrowthi  36726  expgrowth  36728  binomcxplemnotnn0  36749  dvsinax  37821  dvasinbx  37830  dvcosax  37836  stoweidlem10  37908  wallispi2lem1  37971  wallispi2  37973  fouriersw  38133  dfodd6  38805  opoeALTV  38850  opeoALTV  38851  2zrngnmrid  40223  m1modmmod  40597  sinh-conventional  40732  dpfrac1  40765