Theorem mulcld 8095

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 8054	. 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 2176  (class class class)co 5946   CCcc 7925   x. cmul 7932

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

This theorem is referenced by:  kcnktkm1cn  8457  rereim  8661  cru  8677  apreim  8678  mulreim  8679  apadd1  8683  apneg  8686  mulext1  8687  mulext  8689  aprcl  8721  aptap  8725  mulap0  8729  receuap  8744  mul0eqap  8745  divrecap  8763  divcanap3  8773  muldivdirap  8782  divdivdivap  8788  divsubdivap  8803  apmul1  8863  apdivmuld  8888  ofnegsub  9037  qapne  9762  cnref1o  9774  mul2lt0rlt0  9883  lincmb01cmp  10127  iccf1o  10128  qbtwnrelemcalc  10400  flqpmodeq  10474  modq0  10476  modqdiffl  10482  modqvalp1  10490  modqcyc  10506  modqcyc2  10507  modqadd1  10508  mulqaddmodid  10511  modqmuladdnn0  10515  qnegmod  10516  modqmul1  10524  mulexpzap  10726  expmulzap  10732  binom2  10798  binom3  10804  bernneq  10807  mulsubdivbinom2ap  10858  nn0opthd  10869  bcval5  10910  remullem  11215  cjreim2  11248  cnrecnv  11254  absval  11345  resqrexlemover  11354  resqrexlemcalc1  11358  resqrexlemnm  11362  absimle  11428  abstri  11448  bdtrilem  11583  mulcn2  11656  reccn2ap  11657  climcvg1nlem  11693  isummulc2  11770  fsummulc2  11792  fsumparts  11814  binomlem  11827  binom1dif  11831  trireciplem  11844  mertenslemi1  11879  mertensabs  11881  ntrivcvgap  11892  fprodmul  11935  efaddlem  12018  sinval  12046  cosval  12047  sinadd  12080  cosadd  12081  tanaddaplem  12082  tanaddap  12083  addsin  12086  sincossq  12092  sin2t  12093  cos12dec  12112  eirraplem  12121  dvdscmulr  12164  dvdsmulcr  12165  dvds2ln  12168  oddm1even  12219  divalglemnn  12262  divalglemnqt  12264  flodddiv4  12280  gcdaddm  12338  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  lcmgcdlem  12432  oddpwdc  12529  phiprmpw  12577  eulerthlema  12585  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem16  12635  pcpremul  12649  pcaddlem  12695  fldivp1  12704  mul4sqlem  12749  4sqlem14  12760  oddennn  12796  cnfldui  14384  expghmap  14402  znunit  14454  expcn  15074  mulc1cncf  15094  mulcncf  15113  dvmulxxbr  15207  dvimulf  15211  dvexp  15216  dvmptmulx  15225  dvmptcmulcn  15226  plyf  15242  ply1termlem  15247  plyaddlem1  15252  plymullem1  15253  plycoeid3  15262  plycolemc  15263  plycjlemc  15265  plyrecj  15268  dvply1  15270  dvply2g  15271  sin0pilem1  15286  rpcxpef  15399  rpcncxpcl  15407  cxpap0  15409  rpcxpadd  15410  rpmulcxp  15414  cxpmul  15417  rpcxpmul2  15418  abscxp  15420  rpabscxpbnd  15445  binom4  15484  mpodvdsmulf1o  15495  fsumdvdsmul  15496  perfectlem2  15505  lgsquad2lem1  15591  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2sqlem3  15627  qdencn  16003  cvgcmp2nlemabs  16008