Theorem mulcld 7980

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

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811   · cmul 7818

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

This theorem is referenced by:  kcnktkm1cn  8342  rereim  8545  cru  8561  apreim  8562  mulreim  8563  apadd1  8567  apneg  8570  mulext1  8571  mulext  8573  aprcl  8605  aptap  8609  mulap0  8613  receuap  8628  mul0eqap  8629  divrecap  8647  divcanap3  8657  muldivdirap  8666  divdivdivap  8672  divsubdivap  8687  apmul1  8747  apdivmuld  8772  qapne  9641  cnref1o  9652  mul2lt0rlt0  9761  lincmb01cmp  10005  iccf1o  10006  qbtwnrelemcalc  10258  flqpmodeq  10329  modq0  10331  modqdiffl  10337  modqvalp1  10345  modqcyc  10361  modqcyc2  10362  modqadd1  10363  mulqaddmodid  10366  modqmuladdnn0  10370  qnegmod  10371  modqmul1  10379  mulexpzap  10562  expmulzap  10568  binom2  10634  binom3  10640  bernneq  10643  mulsubdivbinom2ap  10693  nn0opthd  10704  bcval5  10745  remullem  10882  cjreim2  10915  cnrecnv  10921  absval  11012  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemnm  11029  absimle  11095  abstri  11115  bdtrilem  11249  mulcn2  11322  reccn2ap  11323  climcvg1nlem  11359  isummulc2  11436  fsummulc2  11458  fsumparts  11480  binomlem  11493  binom1dif  11497  trireciplem  11510  mertenslemi1  11545  mertensabs  11547  ntrivcvgap  11558  fprodmul  11601  efaddlem  11684  sinval  11712  cosval  11713  sinadd  11746  cosadd  11747  tanaddaplem  11748  tanaddap  11749  addsin  11752  sincossq  11758  sin2t  11759  cos12dec  11777  eirraplem  11786  dvdscmulr  11829  dvdsmulcr  11830  dvds2ln  11833  oddm1even  11882  divalglemnn  11925  divalglemnqt  11927  flodddiv4  11941  gcdaddm  11987  bezoutlemnewy  11999  bezoutlema  12002  bezoutlemb  12003  lcmgcdlem  12079  oddpwdc  12176  phiprmpw  12224  eulerthlema  12232  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  pcpremul  12295  pcaddlem  12340  fldivp1  12348  mul4sqlem  12393  oddennn  12395  mulc1cncf  14115  mulcncf  14130  dvmulxxbr  14205  dvimulf  14209  dvexp  14214  dvmptmulx  14221  dvmptcmulcn  14222  sin0pilem1  14241  rpcxpef  14354  rpcncxpcl  14362  cxpap0  14364  rpcxpadd  14365  rpmulcxp  14369  cxpmul  14372  abscxp  14374  rpabscxpbnd  14398  binom4  14436  2sqlem3  14503  qdencn  14814  cvgcmp2nlemabs  14819