Theorem mulcl 8159

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6018   CCcc 8030   x. cmul 8037

This theorem was proved from axioms:  ax-mulcl 8130

This theorem is referenced by:  mpomulf  8169  0cn  8171  mulrid  8176  mulcli  8184  mulcld  8200  mul31  8310  mul4  8311  muladd11r  8335  cnegexlem2  8355  cnegex  8357  muladd  8563  subdi  8564  mul02  8566  submul2  8578  mulsub  8580  recextlem1  8831  recexap  8833  muleqadd  8848  divassap  8870  divmulassap  8875  divmuldivap  8892  divmuleqap  8897  divadddivap  8907  conjmulap  8909  cju  9141  ofnegsub  9142  zneo  9581  exp3vallem  10803  exp3val  10804  exp1  10808  expp1  10809  expcl  10820  expclzaplem  10826  mulexp  10841  sqcl  10863  subsq  10909  subsq2  10910  binom2sub  10916  mulbinom2  10919  binom3  10920  zesq  10921  bernneq  10923  bernneq2  10924  mulsubdivbinom2ap  10974  facnn  10990  fac0  10991  fac1  10992  facp1  10993  bcval5  11026  bcn2  11027  reim  11430  imcl  11432  crre  11435  crim  11436  remim  11438  mulreap  11442  cjreb  11444  recj  11445  reneg  11446  readd  11447  remullem  11449  remul2  11451  imcj  11453  imneg  11454  imadd  11455  immul2  11458  cjadd  11462  ipcnval  11464  cjmulrcl  11465  cjneg  11468  imval2  11472  cjreim  11481  rennim  11580  sqabsadd  11633  sqabssub  11634  absreimsq  11645  absreim  11646  absmul  11647  mul0inf  11819  mulcn2  11890  climmul  11905  isermulc2  11918  fsummulc2  12027  prodf  12117  clim2prod  12118  clim2divap  12119  prod3fmul  12120  prodf1  12121  prodfap0  12124  prodfrecap  12125  prodrbdclem  12150  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodntrivap  12163  prodsnf  12171  fprodcl  12186  fprodclf  12214  efexp  12261  sinf  12283  cosf  12284  tanval2ap  12292  tanval3ap  12293  resinval  12294  recosval  12295  efi4p  12296  resin4p  12297  recos4p  12298  resincl  12299  recoscl  12300  sinneg  12305  cosneg  12306  efival  12311  efmival  12312  efeul  12313  sinadd  12315  cosadd  12316  sinsub  12319  cossub  12320  subsin  12322  sinmul  12323  cosmul  12324  addcos  12325  subcos  12326  cos2tsin  12330  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  absef  12349  absefib  12350  efieq1re  12351  demoivre  12352  demoivreALT  12353  odd2np1lem  12451  odd2np1  12452  opoe  12474  omoe  12475  opeo  12476  omeo  12477  modgcd  12580  qredeq  12686  modprm0  12845  pythagtriplem1  12856  pythagtriplem12  12866  pythagtriplem14  12868  gzmulcl  12969  4sqlem11  12992  4sqlem17  12998  cncrng  14602  cnfldmulg  14609  mpomulcn  15309  mulc1cncf  15332  mulcncflem  15350  dvmulxxbr  15445  dvmulxx  15447  dvimulf  15449  plymullem1  15491  plymulcl  15498  plysubcl  15499  efper  15550  sinperlem  15551  sin2kpi  15554  cos2kpi  15555  efimpi  15562  sincosq1eq  15582  abssinper  15589  sinkpi  15590  coskpi  15591  binom4  15722  fsumdvdsmul  15734  lgsdilem2  15784  lgsne0  15786  lgsquadlem1  15825  2sqlem2  15863