Theorem mulcld 8047

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 8006	. 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 5922   CCcc 7877   x. cmul 7884

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

This theorem is referenced by:  kcnktkm1cn  8409  rereim  8613  cru  8629  apreim  8630  mulreim  8631  apadd1  8635  apneg  8638  mulext1  8639  mulext  8641  aprcl  8673  aptap  8677  mulap0  8681  receuap  8696  mul0eqap  8697  divrecap  8715  divcanap3  8725  muldivdirap  8734  divdivdivap  8740  divsubdivap  8755  apmul1  8815  apdivmuld  8840  ofnegsub  8989  qapne  9713  cnref1o  9725  mul2lt0rlt0  9834  lincmb01cmp  10078  iccf1o  10079  qbtwnrelemcalc  10345  flqpmodeq  10419  modq0  10421  modqdiffl  10427  modqvalp1  10435  modqcyc  10451  modqcyc2  10452  modqadd1  10453  mulqaddmodid  10456  modqmuladdnn0  10460  qnegmod  10461  modqmul1  10469  mulexpzap  10671  expmulzap  10677  binom2  10743  binom3  10749  bernneq  10752  mulsubdivbinom2ap  10803  nn0opthd  10814  bcval5  10855  remullem  11036  cjreim2  11069  cnrecnv  11075  absval  11166  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemnm  11183  absimle  11249  abstri  11269  bdtrilem  11404  mulcn2  11477  reccn2ap  11478  climcvg1nlem  11514  isummulc2  11591  fsummulc2  11613  fsumparts  11635  binomlem  11648  binom1dif  11652  trireciplem  11665  mertenslemi1  11700  mertensabs  11702  ntrivcvgap  11713  fprodmul  11756  efaddlem  11839  sinval  11867  cosval  11868  sinadd  11901  cosadd  11902  tanaddaplem  11903  tanaddap  11904  addsin  11907  sincossq  11913  sin2t  11914  cos12dec  11933  eirraplem  11942  dvdscmulr  11985  dvdsmulcr  11986  dvds2ln  11989  oddm1even  12040  divalglemnn  12083  divalglemnqt  12085  flodddiv4  12101  gcdaddm  12151  bezoutlemnewy  12163  bezoutlema  12166  bezoutlemb  12167  lcmgcdlem  12245  oddpwdc  12342  phiprmpw  12390  eulerthlema  12398  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  pcpremul  12462  pcaddlem  12508  fldivp1  12517  mul4sqlem  12562  4sqlem14  12573  oddennn  12609  cnfldui  14145  expghmap  14163  znunit  14215  expcn  14805  mulc1cncf  14825  mulcncf  14844  dvmulxxbr  14938  dvimulf  14942  dvexp  14947  dvmptmulx  14956  dvmptcmulcn  14957  plyf  14973  ply1termlem  14978  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  plycolemc  14994  plycjlemc  14996  plyrecj  14999  dvply1  15001  dvply2g  15002  sin0pilem1  15017  rpcxpef  15130  rpcncxpcl  15138  cxpap0  15140  rpcxpadd  15141  rpmulcxp  15145  cxpmul  15148  rpcxpmul2  15149  abscxp  15151  rpabscxpbnd  15176  binom4  15215  mpodvdsmulf1o  15226  fsumdvdsmul  15227  perfectlem2  15236  lgsquad2lem1  15322  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2sqlem3  15358  qdencn  15671  cvgcmp2nlemabs  15676