Theorem mulcld 8042

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

Syntax hints:   → wi 4   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   · cmul 7879

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

This theorem is referenced by:  kcnktkm1cn  8404  rereim  8607  cru  8623  apreim  8624  mulreim  8625  apadd1  8629  apneg  8632  mulext1  8633  mulext  8635  aprcl  8667  aptap  8671  mulap0  8675  receuap  8690  mul0eqap  8691  divrecap  8709  divcanap3  8719  muldivdirap  8728  divdivdivap  8734  divsubdivap  8749  apmul1  8809  apdivmuld  8834  ofnegsub  8983  qapne  9707  cnref1o  9719  mul2lt0rlt0  9828  lincmb01cmp  10072  iccf1o  10073  qbtwnrelemcalc  10327  flqpmodeq  10401  modq0  10403  modqdiffl  10409  modqvalp1  10417  modqcyc  10433  modqcyc2  10434  modqadd1  10435  mulqaddmodid  10438  modqmuladdnn0  10442  qnegmod  10443  modqmul1  10451  mulexpzap  10653  expmulzap  10659  binom2  10725  binom3  10731  bernneq  10734  mulsubdivbinom2ap  10785  nn0opthd  10796  bcval5  10837  remullem  11018  cjreim2  11051  cnrecnv  11057  absval  11148  resqrexlemover  11157  resqrexlemcalc1  11161  resqrexlemnm  11165  absimle  11231  abstri  11251  bdtrilem  11385  mulcn2  11458  reccn2ap  11459  climcvg1nlem  11495  isummulc2  11572  fsummulc2  11594  fsumparts  11616  binomlem  11629  binom1dif  11633  trireciplem  11646  mertenslemi1  11681  mertensabs  11683  ntrivcvgap  11694  fprodmul  11737  efaddlem  11820  sinval  11848  cosval  11849  sinadd  11882  cosadd  11883  tanaddaplem  11884  tanaddap  11885  addsin  11888  sincossq  11894  sin2t  11895  cos12dec  11914  eirraplem  11923  dvdscmulr  11966  dvdsmulcr  11967  dvds2ln  11970  oddm1even  12019  divalglemnn  12062  divalglemnqt  12064  flodddiv4  12078  gcdaddm  12124  bezoutlemnewy  12136  bezoutlema  12139  bezoutlemb  12140  lcmgcdlem  12218  oddpwdc  12315  phiprmpw  12363  eulerthlema  12371  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pcpremul  12434  pcaddlem  12480  fldivp1  12489  mul4sqlem  12534  4sqlem14  12545  oddennn  12552  cnfldui  14088  expghmap  14106  znunit  14158  expcn  14748  mulc1cncf  14768  mulcncf  14787  dvmulxxbr  14881  dvimulf  14885  dvexp  14890  dvmptmulx  14899  dvmptcmulcn  14900  plyf  14916  ply1termlem  14921  plyaddlem1  14926  plymullem1  14927  plycolemc  14936  plycjlemc  14938  plyrecj  14941  dvply1  14943  sin0pilem1  14957  rpcxpef  15070  rpcncxpcl  15078  cxpap0  15080  rpcxpadd  15081  rpmulcxp  15085  cxpmul  15088  abscxp  15090  rpabscxpbnd  15114  binom4  15152  lgsquad2lem1  15238  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2sqlem3  15274  qdencn  15587  cvgcmp2nlemabs  15592