Theorem mulcld 8200

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

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

This theorem is referenced by:  kcnktkm1cn  8562  rereim  8766  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  mulext1  8792  mulext  8794  aprcl  8826  aptap  8830  mulap0  8834  receuap  8849  mul0eqap  8850  divrecap  8868  divcanap3  8878  muldivdirap  8887  divdivdivap  8893  divsubdivap  8908  apmul1  8968  apdivmuld  8993  ofnegsub  9142  qapne  9873  cnref1o  9885  mul2lt0rlt0  9994  lincmb01cmp  10238  iccf1o  10239  qbtwnrelemcalc  10516  flqpmodeq  10590  modq0  10592  modqdiffl  10598  modqvalp1  10606  modqcyc  10622  modqcyc2  10623  modqadd1  10624  mulqaddmodid  10627  modqmuladdnn0  10631  qnegmod  10632  modqmul1  10640  mulexpzap  10842  expmulzap  10848  binom2  10914  binom3  10920  bernneq  10923  mulsubdivbinom2ap  10974  nn0opthd  10985  bcval5  11026  remullem  11436  cjreim2  11469  cnrecnv  11475  absval  11566  resqrexlemover  11575  resqrexlemcalc1  11579  resqrexlemnm  11583  absimle  11649  abstri  11669  bdtrilem  11804  mulcn2  11877  reccn2ap  11878  climcvg1nlem  11914  isummulc2  11992  fsummulc2  12014  fsumparts  12036  binomlem  12049  binom1dif  12053  trireciplem  12066  mertenslemi1  12101  mertensabs  12103  ntrivcvgap  12114  fprodmul  12157  efaddlem  12240  sinval  12268  cosval  12269  sinadd  12302  cosadd  12303  tanaddaplem  12304  tanaddap  12305  addsin  12308  sincossq  12314  sin2t  12315  cos12dec  12334  eirraplem  12343  dvdscmulr  12386  dvdsmulcr  12387  dvds2ln  12390  oddm1even  12441  divalglemnn  12484  divalglemnqt  12486  flodddiv4  12502  gcdaddm  12560  bezoutlemnewy  12572  bezoutlema  12575  bezoutlemb  12576  lcmgcdlem  12654  oddpwdc  12751  phiprmpw  12799  eulerthlema  12807  pythagtriplem12  12853  pythagtriplem14  12855  pythagtriplem16  12857  pcpremul  12871  pcaddlem  12917  fldivp1  12926  mul4sqlem  12971  4sqlem14  12982  oddennn  13018  cnfldui  14609  expghmap  14627  znunit  14679  expcn  15299  mulc1cncf  15319  mulcncf  15338  dvmulxxbr  15432  dvimulf  15436  dvexp  15441  dvmptmulx  15450  dvmptcmulcn  15451  plyf  15467  ply1termlem  15472  plyaddlem1  15477  plymullem1  15478  plycoeid3  15487  plycolemc  15488  plycjlemc  15490  plyrecj  15493  dvply1  15495  dvply2g  15496  sin0pilem1  15511  rpcxpef  15624  rpcncxpcl  15632  cxpap0  15634  rpcxpadd  15635  rpmulcxp  15639  cxpmul  15642  rpcxpmul2  15643  abscxp  15645  rpabscxpbnd  15670  binom4  15709  mpodvdsmulf1o  15720  fsumdvdsmul  15721  perfectlem2  15730  lgsquad2lem1  15816  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2sqlem3  15852  qdencn  16657  cvgcmp2nlemabs  16662  qdiff  16679