Theorem mulcld 8092

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

Syntax hints:   → wi 4   ∈ wcel 2175  (class class class)co 5943  ℂcc 7922   · cmul 7929

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

This theorem is referenced by:  kcnktkm1cn  8454  rereim  8658  cru  8674  apreim  8675  mulreim  8676  apadd1  8680  apneg  8683  mulext1  8684  mulext  8686  aprcl  8718  aptap  8722  mulap0  8726  receuap  8741  mul0eqap  8742  divrecap  8760  divcanap3  8770  muldivdirap  8779  divdivdivap  8785  divsubdivap  8800  apmul1  8860  apdivmuld  8885  ofnegsub  9034  qapne  9759  cnref1o  9771  mul2lt0rlt0  9880  lincmb01cmp  10124  iccf1o  10125  qbtwnrelemcalc  10396  flqpmodeq  10470  modq0  10472  modqdiffl  10478  modqvalp1  10486  modqcyc  10502  modqcyc2  10503  modqadd1  10504  mulqaddmodid  10507  modqmuladdnn0  10511  qnegmod  10512  modqmul1  10520  mulexpzap  10722  expmulzap  10728  binom2  10794  binom3  10800  bernneq  10803  mulsubdivbinom2ap  10854  nn0opthd  10865  bcval5  10906  remullem  11153  cjreim2  11186  cnrecnv  11192  absval  11283  resqrexlemover  11292  resqrexlemcalc1  11296  resqrexlemnm  11300  absimle  11366  abstri  11386  bdtrilem  11521  mulcn2  11594  reccn2ap  11595  climcvg1nlem  11631  isummulc2  11708  fsummulc2  11730  fsumparts  11752  binomlem  11765  binom1dif  11769  trireciplem  11782  mertenslemi1  11817  mertensabs  11819  ntrivcvgap  11830  fprodmul  11873  efaddlem  11956  sinval  11984  cosval  11985  sinadd  12018  cosadd  12019  tanaddaplem  12020  tanaddap  12021  addsin  12024  sincossq  12030  sin2t  12031  cos12dec  12050  eirraplem  12059  dvdscmulr  12102  dvdsmulcr  12103  dvds2ln  12106  oddm1even  12157  divalglemnn  12200  divalglemnqt  12202  flodddiv4  12218  gcdaddm  12276  bezoutlemnewy  12288  bezoutlema  12291  bezoutlemb  12292  lcmgcdlem  12370  oddpwdc  12467  phiprmpw  12515  eulerthlema  12523  pythagtriplem12  12569  pythagtriplem14  12571  pythagtriplem16  12573  pcpremul  12587  pcaddlem  12633  fldivp1  12642  mul4sqlem  12687  4sqlem14  12698  oddennn  12734  cnfldui  14322  expghmap  14340  znunit  14392  expcn  15012  mulc1cncf  15032  mulcncf  15051  dvmulxxbr  15145  dvimulf  15149  dvexp  15154  dvmptmulx  15163  dvmptcmulcn  15164  plyf  15180  ply1termlem  15185  plyaddlem1  15190  plymullem1  15191  plycoeid3  15200  plycolemc  15201  plycjlemc  15203  plyrecj  15206  dvply1  15208  dvply2g  15209  sin0pilem1  15224  rpcxpef  15337  rpcncxpcl  15345  cxpap0  15347  rpcxpadd  15348  rpmulcxp  15352  cxpmul  15355  rpcxpmul2  15356  abscxp  15358  rpabscxpbnd  15383  binom4  15422  mpodvdsmulf1o  15433  fsumdvdsmul  15434  perfectlem2  15443  lgsquad2lem1  15529  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2sqlem3  15565  qdencn  15928  cvgcmp2nlemabs  15933