Theorem mulcld 7786

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 7747	. 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 5774   CCcc 7618   x. cmul 7625

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

This theorem is referenced by:  kcnktkm1cn  8145  rereim  8348  cru  8364  apreim  8365  mulreim  8366  apadd1  8370  apneg  8373  mulext1  8374  mulext  8376  aprcl  8408  mulap0  8415  receuap  8430  mul0eqap  8431  divrecap  8448  divcanap3  8458  muldivdirap  8467  divdivdivap  8473  divsubdivap  8488  apmul1  8548  apdivmuld  8573  qapne  9431  cnref1o  9440  mul2lt0rlt0  9546  lincmb01cmp  9786  iccf1o  9787  qbtwnrelemcalc  10033  flqpmodeq  10100  modq0  10102  modqdiffl  10108  modqvalp1  10116  modqcyc  10132  modqcyc2  10133  modqadd1  10134  mulqaddmodid  10137  modqmuladdnn0  10141  qnegmod  10142  modqmul1  10150  mulexpzap  10333  expmulzap  10339  binom2  10403  binom3  10409  bernneq  10412  nn0opthd  10468  bcval5  10509  remullem  10643  cjreim2  10676  cnrecnv  10682  absval  10773  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemnm  10790  absimle  10856  abstri  10876  bdtrilem  11010  mulcn2  11081  reccn2ap  11082  climcvg1nlem  11118  isummulc2  11195  fsummulc2  11217  fsumparts  11239  binomlem  11252  binom1dif  11256  trireciplem  11269  mertenslemi1  11304  mertensabs  11306  ntrivcvgap  11317  efaddlem  11380  sinval  11409  cosval  11410  sinadd  11443  cosadd  11444  tanaddaplem  11445  tanaddap  11446  addsin  11449  sincossq  11455  sin2t  11456  cos12dec  11474  eirraplem  11483  dvdscmulr  11522  dvdsmulcr  11523  dvds2ln  11526  oddm1even  11572  divalglemnn  11615  divalglemnqt  11617  flodddiv4  11631  gcdaddm  11672  bezoutlemnewy  11684  bezoutlema  11687  bezoutlemb  11688  lcmgcdlem  11758  oddpwdc  11852  phiprmpw  11898  oddennn  11905  mulc1cncf  12745  mulcncf  12760  dvmulxxbr  12835  dvimulf  12839  dvexp  12844  dvmptmulx  12851  dvmptcmulcn  12852  sin0pilem1  12862  qdencn  13222  cvgcmp2nlemabs  13227