Theorem mulcld 8178

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 8137	. 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 6007   CCcc 8008   x. cmul 8015

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

This theorem is referenced by:  kcnktkm1cn  8540  rereim  8744  cru  8760  apreim  8761  mulreim  8762  apadd1  8766  apneg  8769  mulext1  8770  mulext  8772  aprcl  8804  aptap  8808  mulap0  8812  receuap  8827  mul0eqap  8828  divrecap  8846  divcanap3  8856  muldivdirap  8865  divdivdivap  8871  divsubdivap  8886  apmul1  8946  apdivmuld  8971  ofnegsub  9120  qapne  9846  cnref1o  9858  mul2lt0rlt0  9967  lincmb01cmp  10211  iccf1o  10212  qbtwnrelemcalc  10487  flqpmodeq  10561  modq0  10563  modqdiffl  10569  modqvalp1  10577  modqcyc  10593  modqcyc2  10594  modqadd1  10595  mulqaddmodid  10598  modqmuladdnn0  10602  qnegmod  10603  modqmul1  10611  mulexpzap  10813  expmulzap  10819  binom2  10885  binom3  10891  bernneq  10894  mulsubdivbinom2ap  10945  nn0opthd  10956  bcval5  10997  remullem  11398  cjreim2  11431  cnrecnv  11437  absval  11528  resqrexlemover  11537  resqrexlemcalc1  11541  resqrexlemnm  11545  absimle  11611  abstri  11631  bdtrilem  11766  mulcn2  11839  reccn2ap  11840  climcvg1nlem  11876  isummulc2  11953  fsummulc2  11975  fsumparts  11997  binomlem  12010  binom1dif  12014  trireciplem  12027  mertenslemi1  12062  mertensabs  12064  ntrivcvgap  12075  fprodmul  12118  efaddlem  12201  sinval  12229  cosval  12230  sinadd  12263  cosadd  12264  tanaddaplem  12265  tanaddap  12266  addsin  12269  sincossq  12275  sin2t  12276  cos12dec  12295  eirraplem  12304  dvdscmulr  12347  dvdsmulcr  12348  dvds2ln  12351  oddm1even  12402  divalglemnn  12445  divalglemnqt  12447  flodddiv4  12463  gcdaddm  12521  bezoutlemnewy  12533  bezoutlema  12536  bezoutlemb  12537  lcmgcdlem  12615  oddpwdc  12712  phiprmpw  12760  eulerthlema  12768  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem16  12818  pcpremul  12832  pcaddlem  12878  fldivp1  12887  mul4sqlem  12932  4sqlem14  12943  oddennn  12979  cnfldui  14569  expghmap  14587  znunit  14639  expcn  15259  mulc1cncf  15279  mulcncf  15298  dvmulxxbr  15392  dvimulf  15396  dvexp  15401  dvmptmulx  15410  dvmptcmulcn  15411  plyf  15427  ply1termlem  15432  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  plycolemc  15448  plycjlemc  15450  plyrecj  15453  dvply1  15455  dvply2g  15456  sin0pilem1  15471  rpcxpef  15584  rpcncxpcl  15592  cxpap0  15594  rpcxpadd  15595  rpmulcxp  15599  cxpmul  15602  rpcxpmul2  15603  abscxp  15605  rpabscxpbnd  15630  binom4  15669  mpodvdsmulf1o  15680  fsumdvdsmul  15681  perfectlem2  15690  lgsquad2lem1  15776  2lgslem3b  15789  2lgslem3c  15790  2lgslem3d  15791  2sqlem3  15812  qdencn  16483  cvgcmp2nlemabs  16488