Theorem mulcld 8040

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 7999	. 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 2164  (class class class)co 5918   CCcc 7870   x. cmul 7877

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

This theorem is referenced by:  kcnktkm1cn  8402  rereim  8605  cru  8621  apreim  8622  mulreim  8623  apadd1  8627  apneg  8630  mulext1  8631  mulext  8633  aprcl  8665  aptap  8669  mulap0  8673  receuap  8688  mul0eqap  8689  divrecap  8707  divcanap3  8717  muldivdirap  8726  divdivdivap  8732  divsubdivap  8747  apmul1  8807  apdivmuld  8832  ofnegsub  8981  qapne  9704  cnref1o  9716  mul2lt0rlt0  9825  lincmb01cmp  10069  iccf1o  10070  qbtwnrelemcalc  10324  flqpmodeq  10398  modq0  10400  modqdiffl  10406  modqvalp1  10414  modqcyc  10430  modqcyc2  10431  modqadd1  10432  mulqaddmodid  10435  modqmuladdnn0  10439  qnegmod  10440  modqmul1  10448  mulexpzap  10650  expmulzap  10656  binom2  10722  binom3  10728  bernneq  10731  mulsubdivbinom2ap  10782  nn0opthd  10793  bcval5  10834  remullem  11015  cjreim2  11048  cnrecnv  11054  absval  11145  resqrexlemover  11154  resqrexlemcalc1  11158  resqrexlemnm  11162  absimle  11228  abstri  11248  bdtrilem  11382  mulcn2  11455  reccn2ap  11456  climcvg1nlem  11492  isummulc2  11569  fsummulc2  11591  fsumparts  11613  binomlem  11626  binom1dif  11630  trireciplem  11643  mertenslemi1  11678  mertensabs  11680  ntrivcvgap  11691  fprodmul  11734  efaddlem  11817  sinval  11845  cosval  11846  sinadd  11879  cosadd  11880  tanaddaplem  11881  tanaddap  11882  addsin  11885  sincossq  11891  sin2t  11892  cos12dec  11911  eirraplem  11920  dvdscmulr  11963  dvdsmulcr  11964  dvds2ln  11967  oddm1even  12016  divalglemnn  12059  divalglemnqt  12061  flodddiv4  12075  gcdaddm  12121  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  lcmgcdlem  12215  oddpwdc  12312  phiprmpw  12360  eulerthlema  12368  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pcpremul  12431  pcaddlem  12477  fldivp1  12486  mul4sqlem  12531  4sqlem14  12542  oddennn  12549  cnfldui  14077  expghmap  14095  znunit  14147  mulc1cncf  14744  mulcncf  14762  dvmulxxbr  14851  dvimulf  14855  dvexp  14860  dvmptmulx  14867  dvmptcmulcn  14868  plyf  14883  ply1termlem  14888  plyaddlem1  14893  plymullem1  14894  sin0pilem1  14916  rpcxpef  15029  rpcncxpcl  15037  cxpap0  15039  rpcxpadd  15040  rpmulcxp  15044  cxpmul  15047  abscxp  15049  rpabscxpbnd  15073  binom4  15111  2sqlem3  15204  qdencn  15517  cvgcmp2nlemabs  15522