Theorem mulcld 8310

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

Syntax hints:   → wi 4   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

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

This theorem is referenced by:  kcnktkm1cn  8673  rereim  8877  cru  8893  apreim  8894  mulreim  8895  apadd1  8899  apneg  8902  mulext1  8903  mulext  8905  aprcl  8937  aptap  8941  mulap0  8945  receuap  8960  mul0eqap  8961  divrecap  8979  divcanap3  8989  muldivdirap  8998  divdivdivap  9004  divsubdivap  9019  apmul1  9079  apdivmuld  9104  ofnegsub  9253  qapne  9989  cnref1o  10001  mul2lt0rlt0  10110  lincmb01cmp  10355  iccf1o  10357  qbtwnrelemcalc  10639  flqpmodeq  10713  modq0  10715  modqdiffl  10721  modqvalp1  10729  modqcyc  10745  modqcyc2  10746  modqadd1  10747  mulqaddmodid  10750  modqmuladdnn0  10754  qnegmod  10755  modqmul1  10763  mulexpzap  10965  expmulzap  10971  binom2  11037  binom3  11043  resq01  11044  bernneq  11047  mulsubdivbinom2ap  11098  nn0opthd  11109  bcval5  11150  remullem  11581  cjreim2  11614  cnrecnv  11620  absval  11711  resqrexlemover  11720  resqrexlemcalc1  11724  resqrexlemnm  11728  absimle  11794  abstri  11814  bdtrilem  11949  mulcn2  12022  reccn2ap  12023  climcvg1nlem  12059  isummulc2  12137  fsummulc2  12159  fsumparts  12181  binomlem  12194  binom1dif  12198  trireciplem  12211  mertenslemi1  12246  mertensabs  12248  ntrivcvgap  12259  fprodmul  12302  efaddlem  12385  sinval  12413  cosval  12414  sinadd  12447  cosadd  12448  tanaddaplem  12449  tanaddap  12450  addsin  12453  sincossq  12459  sin2t  12460  cos12dec  12479  eirraplem  12488  dvdscmulr  12531  dvdsmulcr  12532  dvds2ln  12535  oddm1even  12586  divalglemnn  12629  divalglemnqt  12631  flodddiv4  12647  gcdaddm  12705  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  lcmgcdlem  12799  oddpwdc  12896  phiprmpw  12944  eulerthlema  12952  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pcpremul  13016  pcaddlem  13062  fldivp1  13071  mul4sqlem  13116  4sqlem14  13127  oddennn  13227  cnfldui  14863  expghmap  14881  znunit  14933  expcn  15560  mulc1cncf  15580  mulcncf  15599  dvmulxxbr  15693  dvimulf  15697  dvexp  15702  dvmptmulx  15711  dvmptcmulcn  15712  plyf  15728  ply1termlem  15733  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plycolemc  15749  plycjlemc  15751  plyrecj  15754  dvply1  15756  dvply2g  15757  sin0pilem1  15772  rpcxpef  15885  rpcncxpcl  15893  cxpap0  15895  rpcxpadd  15896  rpmulcxp  15900  cxpmul  15903  rpcxpmul2  15904  abscxp  15906  rpabscxpbnd  15931  binom4  15970  pellexlem1  15971  pellexlem2  15972  mpodvdsmulf1o  15984  fsumdvdsmul  15985  perfectlem2  15994  lgsquad2lem1  16080  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2sqlem3  16116  qdencn  16933  cvgcmp2nlemabs  16942  qdiff  16959  trimul0or  16971