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  8711  rereim  8916  cru  8932  apreim  8933  mulreim  8934  apadd1  8938  apneg  8941  mulext1  8942  mulext  8944  aprcl  8976  aptap  8980  mulap0  8984  msq0  8999  receuap  9001  mul0eqap  9002  divrecap  9020  divcanap3  9030  muldivdirap  9039  divdivdivap  9045  divsubdivap  9060  apmul1  9120  apdivmuld  9145  ofnegsub  9294  qapne  10048  cnref1o  10061  mul2lt0rlt0  10170  lincmb01cmp  10415  iccf1o  10417  qbtwnrelemcalc  10700  flqpmodeq  10777  modq0  10779  modqdiffl  10785  modqvalp1  10793  modqcyc  10809  modqcyc2  10810  modqadd1  10811  mulqaddmodid  10814  modqmuladdnn0  10818  qnegmod  10819  modqmul1  10827  mulexpzap  11029  expmulzap  11035  binom2  11101  binom3  11107  resq01  11108  bernneq  11111  mulsubdivbinom2ap  11163  nn0opthd  11174  bcval5  11215  remullem  11650  sq01  11674  cjreim2  11684  cnrecnv  11690  absval  11781  resqrexlemover  11790  resqrexlemcalc1  11794  resqrexlemnm  11798  absimle  11865  abstri  11885  bdtrilem  12021  mulcn2  12094  reccn2ap  12095  climcvg1nlem  12131  isummulc2  12209  fsummulc2  12231  fsumparts  12253  binomlem  12266  binom1dif  12270  trireciplem  12283  mertenslemi1  12318  mertensabs  12320  ntrivcvgap  12331  fprodmul  12374  efaddlem  12457  sinval  12485  cosval  12486  sinadd  12519  cosadd  12520  tanaddaplem  12521  tanaddap  12522  addsin  12525  sincossq  12531  sin2t  12532  cos12dec  12551  eirraplem  12560  dvdscmulr  12603  dvdsmulcr  12604  dvds2ln  12607  oddm1even  12658  divalglemnn  12701  divalglemnqt  12703  flodddiv4  12719  gcdaddm  12777  bezoutlemnewy  12789  bezoutlema  12792  bezoutlemb  12793  lcmgcdlem  12871  nnmaxpw  12969  phiprmpw  13020  eulerthlema  13028  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  pcpremul  13092  pcaddlem  13138  fldivp1  13147  mul4sqlem  13192  4sqlem14  13203  oddennn  13332  cnfldui  14973  expghmap  14991  znunit  15043  expcn  15719  mulc1cncf  15739  mulcncf  15758  dvmulxxbr  15852  dvimulf  15856  dvexp  15861  dvmptmulx  15870  dvmptcmulcn  15871  plyf  15887  ply1termlem  15892  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  plycolemc  15908  plycjlemc  15910  plyrecj  15913  dvply1  15915  dvply2g  15916  sin0pilem1  15932  rpcxpef  16049  rpcncxpcl  16057  cxpap0  16059  rpcxpadd  16060  rpmulcxp  16064  cxpmul  16067  rpcxpmul2  16068  abscxp  16070  rpabscxpbnd  16095  binom4  16138  birthdaylem2  16145  pellexlem1  16148  pellexlem2  16149  mpodvdsmulf1o  16185  fsumdvdsmul  16186  perfectlem2  16198  lgsquad2lem1  16298  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2sqlem3  16334  qdencn  17170  cvgcmp2nlemabs  17179  qdiff  17196