Theorem mulcld 8167

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 8126	. 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 2200  (class class class)co 6001   CCcc 7997   x. cmul 8004

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

This theorem is referenced by:  kcnktkm1cn  8529  rereim  8733  cru  8749  apreim  8750  mulreim  8751  apadd1  8755  apneg  8758  mulext1  8759  mulext  8761  aprcl  8793  aptap  8797  mulap0  8801  receuap  8816  mul0eqap  8817  divrecap  8835  divcanap3  8845  muldivdirap  8854  divdivdivap  8860  divsubdivap  8875  apmul1  8935  apdivmuld  8960  ofnegsub  9109  qapne  9834  cnref1o  9846  mul2lt0rlt0  9955  lincmb01cmp  10199  iccf1o  10200  qbtwnrelemcalc  10475  flqpmodeq  10549  modq0  10551  modqdiffl  10557  modqvalp1  10565  modqcyc  10581  modqcyc2  10582  modqadd1  10583  mulqaddmodid  10586  modqmuladdnn0  10590  qnegmod  10591  modqmul1  10599  mulexpzap  10801  expmulzap  10807  binom2  10873  binom3  10879  bernneq  10882  mulsubdivbinom2ap  10933  nn0opthd  10944  bcval5  10985  remullem  11382  cjreim2  11415  cnrecnv  11421  absval  11512  resqrexlemover  11521  resqrexlemcalc1  11525  resqrexlemnm  11529  absimle  11595  abstri  11615  bdtrilem  11750  mulcn2  11823  reccn2ap  11824  climcvg1nlem  11860  isummulc2  11937  fsummulc2  11959  fsumparts  11981  binomlem  11994  binom1dif  11998  trireciplem  12011  mertenslemi1  12046  mertensabs  12048  ntrivcvgap  12059  fprodmul  12102  efaddlem  12185  sinval  12213  cosval  12214  sinadd  12247  cosadd  12248  tanaddaplem  12249  tanaddap  12250  addsin  12253  sincossq  12259  sin2t  12260  cos12dec  12279  eirraplem  12288  dvdscmulr  12331  dvdsmulcr  12332  dvds2ln  12335  oddm1even  12386  divalglemnn  12429  divalglemnqt  12431  flodddiv4  12447  gcdaddm  12505  bezoutlemnewy  12517  bezoutlema  12520  bezoutlemb  12521  lcmgcdlem  12599  oddpwdc  12696  phiprmpw  12744  eulerthlema  12752  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem16  12802  pcpremul  12816  pcaddlem  12862  fldivp1  12871  mul4sqlem  12916  4sqlem14  12927  oddennn  12963  cnfldui  14553  expghmap  14571  znunit  14623  expcn  15243  mulc1cncf  15263  mulcncf  15282  dvmulxxbr  15376  dvimulf  15380  dvexp  15385  dvmptmulx  15394  dvmptcmulcn  15395  plyf  15411  ply1termlem  15416  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  plycolemc  15432  plycjlemc  15434  plyrecj  15437  dvply1  15439  dvply2g  15440  sin0pilem1  15455  rpcxpef  15568  rpcncxpcl  15576  cxpap0  15578  rpcxpadd  15579  rpmulcxp  15583  cxpmul  15586  rpcxpmul2  15587  abscxp  15589  rpabscxpbnd  15614  binom4  15653  mpodvdsmulf1o  15664  fsumdvdsmul  15665  perfectlem2  15674  lgsquad2lem1  15760  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2sqlem3  15796  qdencn  16395  cvgcmp2nlemabs  16400