Theorem mulcld 8066

Description: Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
mulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcld

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		mulcl 8025	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   · cmul 7903

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

This theorem is referenced by:  kcnktkm1cn  8428  rereim  8632  cru  8648  apreim  8649  mulreim  8650  apadd1  8654  apneg  8657  mulext1  8658  mulext  8660  aprcl  8692  aptap  8696  mulap0  8700  receuap  8715  mul0eqap  8716  divrecap  8734  divcanap3  8744  muldivdirap  8753  divdivdivap  8759  divsubdivap  8774  apmul1  8834  apdivmuld  8859  ofnegsub  9008  qapne  9732  cnref1o  9744  mul2lt0rlt0  9853  lincmb01cmp  10097  iccf1o  10098  qbtwnrelemcalc  10364  flqpmodeq  10438  modq0  10440  modqdiffl  10446  modqvalp1  10454  modqcyc  10470  modqcyc2  10471  modqadd1  10472  mulqaddmodid  10475  modqmuladdnn0  10479  qnegmod  10480  modqmul1  10488  mulexpzap  10690  expmulzap  10696  binom2  10762  binom3  10768  bernneq  10771  mulsubdivbinom2ap  10822  nn0opthd  10833  bcval5  10874  remullem  11055  cjreim2  11088  cnrecnv  11094  absval  11185  resqrexlemover  11194  resqrexlemcalc1  11198  resqrexlemnm  11202  absimle  11268  abstri  11288  bdtrilem  11423  mulcn2  11496  reccn2ap  11497  climcvg1nlem  11533  isummulc2  11610  fsummulc2  11632  fsumparts  11654  binomlem  11667  binom1dif  11671  trireciplem  11684  mertenslemi1  11719  mertensabs  11721  ntrivcvgap  11732  fprodmul  11775  efaddlem  11858  sinval  11886  cosval  11887  sinadd  11920  cosadd  11921  tanaddaplem  11922  tanaddap  11923  addsin  11926  sincossq  11932  sin2t  11933  cos12dec  11952  eirraplem  11961  dvdscmulr  12004  dvdsmulcr  12005  dvds2ln  12008  oddm1even  12059  divalglemnn  12102  divalglemnqt  12104  flodddiv4  12120  gcdaddm  12178  bezoutlemnewy  12190  bezoutlema  12193  bezoutlemb  12194  lcmgcdlem  12272  oddpwdc  12369  phiprmpw  12417  eulerthlema  12425  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  pcpremul  12489  pcaddlem  12535  fldivp1  12544  mul4sqlem  12589  4sqlem14  12600  oddennn  12636  cnfldui  14223  expghmap  14241  znunit  14293  expcn  14913  mulc1cncf  14933  mulcncf  14952  dvmulxxbr  15046  dvimulf  15050  dvexp  15055  dvmptmulx  15064  dvmptcmulcn  15065  plyf  15081  ply1termlem  15086  plyaddlem1  15091  plymullem1  15092  plycoeid3  15101  plycolemc  15102  plycjlemc  15104  plyrecj  15107  dvply1  15109  dvply2g  15110  sin0pilem1  15125  rpcxpef  15238  rpcncxpcl  15246  cxpap0  15248  rpcxpadd  15249  rpmulcxp  15253  cxpmul  15256  rpcxpmul2  15257  abscxp  15259  rpabscxpbnd  15284  binom4  15323  mpodvdsmulf1o  15334  fsumdvdsmul  15335  perfectlem2  15344  lgsquad2lem1  15430  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2sqlem3  15466  qdencn  15784  cvgcmp2nlemabs  15789