Theorem mulcld 7779

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 7740	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	syl2anc 408	1 |- ( ph -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1480  (class class class)co 5767   CCcc 7611   x. cmul 7618

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

This theorem is referenced by:  kcnktkm1cn  8138  rereim  8341  cru  8357  apreim  8358  mulreim  8359  apadd1  8363  apneg  8366  mulext1  8367  mulext  8369  aprcl  8401  mulap0  8408  receuap  8423  mul0eqap  8424  divrecap  8441  divcanap3  8451  muldivdirap  8460  divdivdivap  8466  divsubdivap  8481  apmul1  8541  apdivmuld  8566  qapne  9424  cnref1o  9433  mul2lt0rlt0  9539  lincmb01cmp  9779  iccf1o  9780  qbtwnrelemcalc  10026  flqpmodeq  10093  modq0  10095  modqdiffl  10101  modqvalp1  10109  modqcyc  10125  modqcyc2  10126  modqadd1  10127  mulqaddmodid  10130  modqmuladdnn0  10134  qnegmod  10135  modqmul1  10143  mulexpzap  10326  expmulzap  10332  binom2  10396  binom3  10402  bernneq  10405  nn0opthd  10461  bcval5  10502  remullem  10636  cjreim2  10669  cnrecnv  10675  absval  10766  resqrexlemover  10775  resqrexlemcalc1  10779  resqrexlemnm  10783  absimle  10849  abstri  10869  bdtrilem  11003  mulcn2  11074  reccn2ap  11075  climcvg1nlem  11111  isummulc2  11188  fsummulc2  11210  fsumparts  11232  binomlem  11245  binom1dif  11249  trireciplem  11262  mertenslemi1  11297  mertensabs  11299  ntrivcvgap  11310  efaddlem  11369  sinval  11398  cosval  11399  sinadd  11432  cosadd  11433  tanaddaplem  11434  tanaddap  11435  addsin  11438  sincossq  11444  sin2t  11445  cos12dec  11463  eirraplem  11472  dvdscmulr  11511  dvdsmulcr  11512  dvds2ln  11515  oddm1even  11561  divalglemnn  11604  divalglemnqt  11606  flodddiv4  11620  gcdaddm  11661  bezoutlemnewy  11673  bezoutlema  11676  bezoutlemb  11677  lcmgcdlem  11747  oddpwdc  11841  phiprmpw  11887  oddennn  11894  mulc1cncf  12734  mulcncf  12749  dvmulxxbr  12824  dvimulf  12828  dvexp  12833  dvmptmulx  12840  dvmptcmulcn  12841  sin0pilem1  12851  qdencn  13211  cvgcmp2nlemabs  13216