Theorem mulcld 8200

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 8159	. 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 2202  (class class class)co 6018   CCcc 8030   x. cmul 8037

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

This theorem is referenced by:  kcnktkm1cn  8562  rereim  8766  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  mulext1  8792  mulext  8794  aprcl  8826  aptap  8830  mulap0  8834  receuap  8849  mul0eqap  8850  divrecap  8868  divcanap3  8878  muldivdirap  8887  divdivdivap  8893  divsubdivap  8908  apmul1  8968  apdivmuld  8993  ofnegsub  9142  qapne  9873  cnref1o  9885  mul2lt0rlt0  9994  lincmb01cmp  10238  iccf1o  10239  qbtwnrelemcalc  10516  flqpmodeq  10590  modq0  10592  modqdiffl  10598  modqvalp1  10606  modqcyc  10622  modqcyc2  10623  modqadd1  10624  mulqaddmodid  10627  modqmuladdnn0  10631  qnegmod  10632  modqmul1  10640  mulexpzap  10842  expmulzap  10848  binom2  10914  binom3  10920  bernneq  10923  mulsubdivbinom2ap  10974  nn0opthd  10985  bcval5  11026  remullem  11449  cjreim2  11482  cnrecnv  11488  absval  11579  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemnm  11596  absimle  11662  abstri  11682  bdtrilem  11817  mulcn2  11890  reccn2ap  11891  climcvg1nlem  11927  isummulc2  12005  fsummulc2  12027  fsumparts  12049  binomlem  12062  binom1dif  12066  trireciplem  12079  mertenslemi1  12114  mertensabs  12116  ntrivcvgap  12127  fprodmul  12170  efaddlem  12253  sinval  12281  cosval  12282  sinadd  12315  cosadd  12316  tanaddaplem  12317  tanaddap  12318  addsin  12321  sincossq  12327  sin2t  12328  cos12dec  12347  eirraplem  12356  dvdscmulr  12399  dvdsmulcr  12400  dvds2ln  12403  oddm1even  12454  divalglemnn  12497  divalglemnqt  12499  flodddiv4  12515  gcdaddm  12573  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  lcmgcdlem  12667  oddpwdc  12764  phiprmpw  12812  eulerthlema  12820  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pcpremul  12884  pcaddlem  12930  fldivp1  12939  mul4sqlem  12984  4sqlem14  12995  oddennn  13031  cnfldui  14622  expghmap  14640  znunit  14692  expcn  15312  mulc1cncf  15332  mulcncf  15351  dvmulxxbr  15445  dvimulf  15449  dvexp  15454  dvmptmulx  15463  dvmptcmulcn  15464  plyf  15480  ply1termlem  15485  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  plycolemc  15501  plycjlemc  15503  plyrecj  15506  dvply1  15508  dvply2g  15509  sin0pilem1  15524  rpcxpef  15637  rpcncxpcl  15645  cxpap0  15647  rpcxpadd  15648  rpmulcxp  15652  cxpmul  15655  rpcxpmul2  15656  abscxp  15658  rpabscxpbnd  15683  binom4  15722  mpodvdsmulf1o  15733  fsumdvdsmul  15734  perfectlem2  15743  lgsquad2lem1  15829  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2sqlem3  15865  qdencn  16682  cvgcmp2nlemabs  16687  qdiff  16704