Theorem mulcld 8064

Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
mulcld	|- ( ph -> ( A x. B ) e. CC )

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		mulcl 8023	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 2167  (class class class)co 5925   CCcc 7894   x. cmul 7901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 7994

This theorem is referenced by:  kcnktkm1cn  8426  rereim  8630  cru  8646  apreim  8647  mulreim  8648  apadd1  8652  apneg  8655  mulext1  8656  mulext  8658  aprcl  8690  aptap  8694  mulap0  8698  receuap  8713  mul0eqap  8714  divrecap  8732  divcanap3  8742  muldivdirap  8751  divdivdivap  8757  divsubdivap  8772  apmul1  8832  apdivmuld  8857  ofnegsub  9006  qapne  9730  cnref1o  9742  mul2lt0rlt0  9851  lincmb01cmp  10095  iccf1o  10096  qbtwnrelemcalc  10362  flqpmodeq  10436  modq0  10438  modqdiffl  10444  modqvalp1  10452  modqcyc  10468  modqcyc2  10469  modqadd1  10470  mulqaddmodid  10473  modqmuladdnn0  10477  qnegmod  10478  modqmul1  10486  mulexpzap  10688  expmulzap  10694  binom2  10760  binom3  10766  bernneq  10769  mulsubdivbinom2ap  10820  nn0opthd  10831  bcval5  10872  remullem  11053  cjreim2  11086  cnrecnv  11092  absval  11183  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemnm  11200  absimle  11266  abstri  11286  bdtrilem  11421  mulcn2  11494  reccn2ap  11495  climcvg1nlem  11531  isummulc2  11608  fsummulc2  11630  fsumparts  11652  binomlem  11665  binom1dif  11669  trireciplem  11682  mertenslemi1  11717  mertensabs  11719  ntrivcvgap  11730  fprodmul  11773  efaddlem  11856  sinval  11884  cosval  11885  sinadd  11918  cosadd  11919  tanaddaplem  11920  tanaddap  11921  addsin  11924  sincossq  11930  sin2t  11931  cos12dec  11950  eirraplem  11959  dvdscmulr  12002  dvdsmulcr  12003  dvds2ln  12006  oddm1even  12057  divalglemnn  12100  divalglemnqt  12102  flodddiv4  12118  gcdaddm  12176  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  lcmgcdlem  12270  oddpwdc  12367  phiprmpw  12415  eulerthlema  12423  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  pcpremul  12487  pcaddlem  12533  fldivp1  12542  mul4sqlem  12587  4sqlem14  12598  oddennn  12634  cnfldui  14221  expghmap  14239  znunit  14291  expcn  14889  mulc1cncf  14909  mulcncf  14928  dvmulxxbr  15022  dvimulf  15026  dvexp  15031  dvmptmulx  15040  dvmptcmulcn  15041  plyf  15057  ply1termlem  15062  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  plycolemc  15078  plycjlemc  15080  plyrecj  15083  dvply1  15085  dvply2g  15086  sin0pilem1  15101  rpcxpef  15214  rpcncxpcl  15222  cxpap0  15224  rpcxpadd  15225  rpmulcxp  15229  cxpmul  15232  rpcxpmul2  15233  abscxp  15235  rpabscxpbnd  15260  binom4  15299  mpodvdsmulf1o  15310  fsumdvdsmul  15311  perfectlem2  15320  lgsquad2lem1  15406  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2sqlem3  15442  qdencn  15758  cvgcmp2nlemabs  15763