Theorem mulcl 8087

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2178  (class class class)co 5967   CCcc 7958   x. cmul 7965

This theorem was proved from axioms:  ax-mulcl 8058

This theorem is referenced by:  mpomulf  8097  0cn  8099  mulrid  8104  mulcli  8112  mulcld  8128  mul31  8238  mul4  8239  muladd11r  8263  cnegexlem2  8283  cnegex  8285  muladd  8491  subdi  8492  mul02  8494  submul2  8506  mulsub  8508  recextlem1  8759  recexap  8761  muleqadd  8776  divassap  8798  divmulassap  8803  divmuldivap  8820  divmuleqap  8825  divadddivap  8835  conjmulap  8837  cju  9069  ofnegsub  9070  zneo  9509  exp3vallem  10722  exp3val  10723  exp1  10727  expp1  10728  expcl  10739  expclzaplem  10745  mulexp  10760  sqcl  10782  subsq  10828  subsq2  10829  binom2sub  10835  mulbinom2  10838  binom3  10839  zesq  10840  bernneq  10842  bernneq2  10843  mulsubdivbinom2ap  10893  facnn  10909  fac0  10910  fac1  10911  facp1  10912  bcval5  10945  bcn2  10946  reim  11278  imcl  11280  crre  11283  crim  11284  remim  11286  mulreap  11290  cjreb  11292  recj  11293  reneg  11294  readd  11295  remullem  11297  remul2  11299  imcj  11301  imneg  11302  imadd  11303  immul2  11306  cjadd  11310  ipcnval  11312  cjmulrcl  11313  cjneg  11316  imval2  11320  cjreim  11329  rennim  11428  sqabsadd  11481  sqabssub  11482  absreimsq  11493  absreim  11494  absmul  11495  mul0inf  11667  mulcn2  11738  climmul  11753  isermulc2  11766  fsummulc2  11874  prodf  11964  clim2prod  11965  clim2divap  11966  prod3fmul  11967  prodf1  11968  prodfap0  11971  prodfrecap  11972  prodrbdclem  11997  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prodsnf  12018  fprodcl  12033  fprodclf  12061  efexp  12108  sinf  12130  cosf  12131  tanval2ap  12139  tanval3ap  12140  resinval  12141  recosval  12142  efi4p  12143  resin4p  12144  recos4p  12145  resincl  12146  recoscl  12147  sinneg  12152  cosneg  12153  efival  12158  efmival  12159  efeul  12160  sinadd  12162  cosadd  12163  sinsub  12166  cossub  12167  subsin  12169  sinmul  12170  cosmul  12171  addcos  12172  subcos  12173  cos2tsin  12177  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  absef  12196  absefib  12197  efieq1re  12198  demoivre  12199  demoivreALT  12200  odd2np1lem  12298  odd2np1  12299  opoe  12321  omoe  12322  opeo  12323  omeo  12324  modgcd  12427  qredeq  12533  modprm0  12692  pythagtriplem1  12703  pythagtriplem12  12713  pythagtriplem14  12715  gzmulcl  12816  4sqlem11  12839  4sqlem17  12845  cncrng  14446  cnfldmulg  14453  mpomulcn  15153  mulc1cncf  15176  mulcncflem  15194  dvmulxxbr  15289  dvmulxx  15291  dvimulf  15293  plymullem1  15335  plymulcl  15342  plysubcl  15343  efper  15394  sinperlem  15395  sin2kpi  15398  cos2kpi  15399  efimpi  15406  sincosq1eq  15426  abssinper  15433  sinkpi  15434  coskpi  15435  binom4  15566  fsumdvdsmul  15578  lgsdilem2  15628  lgsne0  15630  lgsquadlem1  15669  2sqlem2  15707