Theorem mulcld 8259

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 8219	. 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 6028   CCcc 8090   x. cmul 8097

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

This theorem is referenced by:  kcnktkm1cn  8621  rereim  8825  cru  8841  apreim  8842  mulreim  8843  apadd1  8847  apneg  8850  mulext1  8851  mulext  8853  aprcl  8885  aptap  8889  mulap0  8893  receuap  8908  mul0eqap  8909  divrecap  8927  divcanap3  8937  muldivdirap  8946  divdivdivap  8952  divsubdivap  8967  apmul1  9027  apdivmuld  9052  ofnegsub  9201  qapne  9934  cnref1o  9946  mul2lt0rlt0  10055  lincmb01cmp  10299  iccf1o  10301  qbtwnrelemcalc  10578  flqpmodeq  10652  modq0  10654  modqdiffl  10660  modqvalp1  10668  modqcyc  10684  modqcyc2  10685  modqadd1  10686  mulqaddmodid  10689  modqmuladdnn0  10693  qnegmod  10694  modqmul1  10702  mulexpzap  10904  expmulzap  10910  binom2  10976  binom3  10982  bernneq  10985  mulsubdivbinom2ap  11036  nn0opthd  11047  bcval5  11088  remullem  11511  cjreim2  11544  cnrecnv  11550  absval  11641  resqrexlemover  11650  resqrexlemcalc1  11654  resqrexlemnm  11658  absimle  11724  abstri  11744  bdtrilem  11879  mulcn2  11952  reccn2ap  11953  climcvg1nlem  11989  isummulc2  12067  fsummulc2  12089  fsumparts  12111  binomlem  12124  binom1dif  12128  trireciplem  12141  mertenslemi1  12176  mertensabs  12178  ntrivcvgap  12189  fprodmul  12232  efaddlem  12315  sinval  12343  cosval  12344  sinadd  12377  cosadd  12378  tanaddaplem  12379  tanaddap  12380  addsin  12383  sincossq  12389  sin2t  12390  cos12dec  12409  eirraplem  12418  dvdscmulr  12461  dvdsmulcr  12462  dvds2ln  12465  oddm1even  12516  divalglemnn  12559  divalglemnqt  12561  flodddiv4  12577  gcdaddm  12635  bezoutlemnewy  12647  bezoutlema  12650  bezoutlemb  12651  lcmgcdlem  12729  oddpwdc  12826  phiprmpw  12874  eulerthlema  12882  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem16  12932  pcpremul  12946  pcaddlem  12992  fldivp1  13001  mul4sqlem  13046  4sqlem14  13057  oddennn  13093  cnfldui  14685  expghmap  14703  znunit  14755  expcn  15380  mulc1cncf  15400  mulcncf  15419  dvmulxxbr  15513  dvimulf  15517  dvexp  15522  dvmptmulx  15531  dvmptcmulcn  15532  plyf  15548  ply1termlem  15553  plyaddlem1  15558  plymullem1  15559  plycoeid3  15568  plycolemc  15569  plycjlemc  15571  plyrecj  15574  dvply1  15576  dvply2g  15577  sin0pilem1  15592  rpcxpef  15705  rpcncxpcl  15713  cxpap0  15715  rpcxpadd  15716  rpmulcxp  15720  cxpmul  15723  rpcxpmul2  15724  abscxp  15726  rpabscxpbnd  15751  binom4  15790  pellexlem1  15791  pellexlem2  15792  mpodvdsmulf1o  15804  fsumdvdsmul  15805  perfectlem2  15814  lgsquad2lem1  15900  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2sqlem3  15936  qdencn  16755  cvgcmp2nlemabs  16764  qdiff  16781