Theorem mulcld 8352

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 8312	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6088  ℂcc 8183   · cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8283

This theorem is used by:  kcnktkm1cn  8717  rereim  8922  cru  8938  apreim  8939  mulreim  8940  apadd1  8944  apneg  8947  mulext1  8948  mulext  8950  aprcl  8982  aptap  8986  mulap0  8990  msq0  9005  receuap  9007  mul0eqap  9008  divrecap  9026  divcanap3  9036  muldivdirap  9045  divdivdivap  9051  divsubdivap  9066  apmul1  9126  apdivmuld  9151  ofnegsub  9301  qapne  10054  cnref1o  10067  mul2lt0rlt0  10176  lincmb01cmp  10421  iccf1o  10423  qbtwnrelemcalc  10706  flqpmodeq  10784  modq0  10786  modqdiffl  10792  modqvalp1  10800  modqcyc  10816  modqcyc2  10817  modqadd1  10818  mulqaddmodid  10821  modqmuladdnn0  10825  qnegmod  10826  modqmul1  10834  mulexpzap  11036  expmulzap  11042  binom2  11108  binom3  11114  resq01  11115  bernneq  11118  mulsubdivbinom2ap  11170  nn0opthd  11181  bcval5  11222  remullem  11657  sq01  11681  cjreim2  11691  cnrecnv  11697  absval  11788  resqrexlemover  11797  resqrexlemcalc1  11801  resqrexlemnm  11805  absimle  11872  abstri  11892  bdtrilem  12029  mulcn2  12102  reccn2ap  12103  climcvg1nlem  12139  isummulc2  12217  fsummulc2  12239  fsumparts  12261  binomlem  12274  binom1dif  12278  trireciplem  12291  mertenslemi1  12326  mertensabs  12328  ntrivcvgap  12339  fprodmul  12382  efaddlem  12465  sinval  12493  cosval  12494  sinadd  12527  cosadd  12528  tanaddaplem  12529  tanaddap  12530  addsin  12533  sincossq  12539  sin2t  12540  cos12dec  12559  eirraplem  12568  dvdscmulr  12611  dvdsmulcr  12612  dvds2ln  12615  oddm1even  12666  divalglemnn  12709  divalglemnqt  12711  flodddiv4  12727  gcdaddm  12785  bezoutlemnewy  12797  bezoutlema  12800  bezoutlemb  12801  lcmgcdlem  12879  nnmaxpw  12977  phiprmpw  13028  eulerthlema  13036  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  pcpremul  13100  pcaddlem  13146  fldivp1  13155  mul4sqlem  13200  4sqlem14  13211  oddennn  13340  cnfldui  15032  expghmap  15050  znunit  15102  expcn  15812  mulc1cncf  15832  mulcncf  15851  dvmulxxbr  15945  dvimulf  15949  dvexp  15954  dvmptmulx  15963  dvmptcmulcn  15964  plyf  15980  ply1termlem  15985  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  plycolemc  16001  plycjlemc  16003  plyrecj  16006  dvply1  16008  dvply2g  16009  sin0pilem1  16025  rpcxpef  16144  rpcncxpcl  16152  cxpap0  16154  rpcxpadd  16155  rpmulcxp  16159  cxpmul  16162  rpcxpmul2  16163  rpcxpmul2z  16165  abscxp  16167  rpabscxpbnd  16192  binom4  16236  birthdaylem2  16243  pellexlem1  16246  pellexlem2  16247  mpodvdsmulf1o  16301  fsumdvdsmul  16302  perfectlem2  16317  bposlem9  16336  lgsquad2lem1  16422  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2sqlem3  16458  qdencn  17295  cvgcmp2nlemabs  17304  qdiff  17322