Theorem mulcld 7972

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 7933	. 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 2148  (class class class)co 5870   CCcc 7804   x. cmul 7811

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

This theorem is referenced by:  kcnktkm1cn  8334  rereim  8537  cru  8553  apreim  8554  mulreim  8555  apadd1  8559  apneg  8562  mulext1  8563  mulext  8565  aprcl  8597  aptap  8601  mulap0  8605  receuap  8620  mul0eqap  8621  divrecap  8639  divcanap3  8649  muldivdirap  8658  divdivdivap  8664  divsubdivap  8679  apmul1  8739  apdivmuld  8764  qapne  9633  cnref1o  9644  mul2lt0rlt0  9753  lincmb01cmp  9997  iccf1o  9998  qbtwnrelemcalc  10249  flqpmodeq  10320  modq0  10322  modqdiffl  10328  modqvalp1  10336  modqcyc  10352  modqcyc2  10353  modqadd1  10354  mulqaddmodid  10357  modqmuladdnn0  10361  qnegmod  10362  modqmul1  10370  mulexpzap  10553  expmulzap  10559  binom2  10624  binom3  10630  bernneq  10633  nn0opthd  10693  bcval5  10734  remullem  10871  cjreim2  10904  cnrecnv  10910  absval  11001  resqrexlemover  11010  resqrexlemcalc1  11014  resqrexlemnm  11018  absimle  11084  abstri  11104  bdtrilem  11238  mulcn2  11311  reccn2ap  11312  climcvg1nlem  11348  isummulc2  11425  fsummulc2  11447  fsumparts  11469  binomlem  11482  binom1dif  11486  trireciplem  11499  mertenslemi1  11534  mertensabs  11536  ntrivcvgap  11547  fprodmul  11590  efaddlem  11673  sinval  11701  cosval  11702  sinadd  11735  cosadd  11736  tanaddaplem  11737  tanaddap  11738  addsin  11741  sincossq  11747  sin2t  11748  cos12dec  11766  eirraplem  11775  dvdscmulr  11818  dvdsmulcr  11819  dvds2ln  11822  oddm1even  11870  divalglemnn  11913  divalglemnqt  11915  flodddiv4  11929  gcdaddm  11975  bezoutlemnewy  11987  bezoutlema  11990  bezoutlemb  11991  lcmgcdlem  12067  oddpwdc  12164  phiprmpw  12212  eulerthlema  12220  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  pcpremul  12283  pcaddlem  12328  fldivp1  12336  mul4sqlem  12381  oddennn  12383  mulc1cncf  13858  mulcncf  13873  dvmulxxbr  13948  dvimulf  13952  dvexp  13957  dvmptmulx  13964  dvmptcmulcn  13965  sin0pilem1  13984  rpcxpef  14097  rpcncxpcl  14105  cxpap0  14107  rpcxpadd  14108  rpmulcxp  14112  cxpmul  14115  abscxp  14117  rpabscxpbnd  14141  binom4  14179  2sqlem3  14235  qdencn  14546  cvgcmp2nlemabs  14551