Theorem mulcld 8346

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   CCcc 8177   x. cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8277

This theorem is used by:  kcnktkm1cn  8710  rereim  8914  cru  8930  apreim  8931  mulreim  8932  apadd1  8936  apneg  8939  mulext1  8940  mulext  8942  aprcl  8974  aptap  8978  mulap0  8982  msq0  8997  receuap  8999  mul0eqap  9000  divrecap  9018  divcanap3  9028  muldivdirap  9037  divdivdivap  9043  divsubdivap  9058  apmul1  9118  apdivmuld  9143  ofnegsub  9292  qapne  10039  cnref1o  10051  mul2lt0rlt0  10160  lincmb01cmp  10405  iccf1o  10407  qbtwnrelemcalc  10690  flqpmodeq  10764  modq0  10766  modqdiffl  10772  modqvalp1  10780  modqcyc  10796  modqcyc2  10797  modqadd1  10798  mulqaddmodid  10801  modqmuladdnn0  10805  qnegmod  10806  modqmul1  10814  mulexpzap  11016  expmulzap  11022  binom2  11088  binom3  11094  resq01  11095  bernneq  11098  mulsubdivbinom2ap  11149  nn0opthd  11160  bcval5  11201  remullem  11636  sq01  11660  cjreim2  11670  cnrecnv  11676  absval  11767  resqrexlemover  11776  resqrexlemcalc1  11780  resqrexlemnm  11784  absimle  11850  abstri  11870  bdtrilem  12005  mulcn2  12078  reccn2ap  12079  climcvg1nlem  12115  isummulc2  12193  fsummulc2  12215  fsumparts  12237  binomlem  12250  binom1dif  12254  trireciplem  12267  mertenslemi1  12302  mertensabs  12304  ntrivcvgap  12315  fprodmul  12358  efaddlem  12441  sinval  12469  cosval  12470  sinadd  12503  cosadd  12504  tanaddaplem  12505  tanaddap  12506  addsin  12509  sincossq  12515  sin2t  12516  cos12dec  12535  eirraplem  12544  dvdscmulr  12587  dvdsmulcr  12588  dvds2ln  12591  oddm1even  12642  divalglemnn  12685  divalglemnqt  12687  flodddiv4  12703  gcdaddm  12761  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  lcmgcdlem  12855  oddpwdc  12952  phiprmpw  13000  eulerthlema  13008  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pcpremul  13072  pcaddlem  13118  fldivp1  13127  mul4sqlem  13172  4sqlem14  13183  oddennn  13283  cnfldui  14924  expghmap  14942  znunit  14994  expcn  15670  mulc1cncf  15690  mulcncf  15709  dvmulxxbr  15803  dvimulf  15807  dvexp  15812  dvmptmulx  15821  dvmptcmulcn  15822  plyf  15838  ply1termlem  15843  plyaddlem1  15848  plymullem1  15849  plycoeid3  15858  plycolemc  15859  plycjlemc  15861  plyrecj  15864  dvply1  15866  dvply2g  15867  sin0pilem1  15882  rpcxpef  15996  rpcncxpcl  16004  cxpap0  16006  rpcxpadd  16007  rpmulcxp  16011  cxpmul  16014  rpcxpmul2  16015  abscxp  16017  rpabscxpbnd  16042  binom4  16081  birthdaylem2  16088  pellexlem1  16091  pellexlem2  16092  mpodvdsmulf1o  16104  fsumdvdsmul  16105  perfectlem2  16114  lgsquad2lem1  16200  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2sqlem3  16236  qdencn  17072  cvgcmp2nlemabs  17081  qdiff  17098