Theorem mulcld 7940

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   · cmul 7779

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

This theorem is referenced by:  kcnktkm1cn  8302  rereim  8505  cru  8521  apreim  8522  mulreim  8523  apadd1  8527  apneg  8530  mulext1  8531  mulext  8533  aprcl  8565  mulap0  8572  receuap  8587  mul0eqap  8588  divrecap  8605  divcanap3  8615  muldivdirap  8624  divdivdivap  8630  divsubdivap  8645  apmul1  8705  apdivmuld  8730  qapne  9598  cnref1o  9609  mul2lt0rlt0  9716  lincmb01cmp  9960  iccf1o  9961  qbtwnrelemcalc  10212  flqpmodeq  10283  modq0  10285  modqdiffl  10291  modqvalp1  10299  modqcyc  10315  modqcyc2  10316  modqadd1  10317  mulqaddmodid  10320  modqmuladdnn0  10324  qnegmod  10325  modqmul1  10333  mulexpzap  10516  expmulzap  10522  binom2  10587  binom3  10593  bernneq  10596  nn0opthd  10656  bcval5  10697  remullem  10835  cjreim2  10868  cnrecnv  10874  absval  10965  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemnm  10982  absimle  11048  abstri  11068  bdtrilem  11202  mulcn2  11275  reccn2ap  11276  climcvg1nlem  11312  isummulc2  11389  fsummulc2  11411  fsumparts  11433  binomlem  11446  binom1dif  11450  trireciplem  11463  mertenslemi1  11498  mertensabs  11500  ntrivcvgap  11511  fprodmul  11554  efaddlem  11637  sinval  11665  cosval  11666  sinadd  11699  cosadd  11700  tanaddaplem  11701  tanaddap  11702  addsin  11705  sincossq  11711  sin2t  11712  cos12dec  11730  eirraplem  11739  dvdscmulr  11782  dvdsmulcr  11783  dvds2ln  11786  oddm1even  11834  divalglemnn  11877  divalglemnqt  11879  flodddiv4  11893  gcdaddm  11939  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  lcmgcdlem  12031  oddpwdc  12128  phiprmpw  12176  eulerthlema  12184  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  pcpremul  12247  pcaddlem  12292  fldivp1  12300  mul4sqlem  12345  oddennn  12347  mulc1cncf  13370  mulcncf  13385  dvmulxxbr  13460  dvimulf  13464  dvexp  13469  dvmptmulx  13476  dvmptcmulcn  13477  sin0pilem1  13496  rpcxpef  13609  rpcncxpcl  13617  cxpap0  13619  rpcxpadd  13620  rpmulcxp  13624  cxpmul  13627  abscxp  13629  rpabscxpbnd  13653  binom4  13691  2sqlem3  13747  qdencn  14059  cvgcmp2nlemabs  14064