Theorem mulcld 7881

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

Syntax hints:   → wi 4   ∈ wcel 2128  (class class class)co 5818  ℂcc 7713   · cmul 7720

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

This theorem is referenced by:  kcnktkm1cn  8241  rereim  8444  cru  8460  apreim  8461  mulreim  8462  apadd1  8466  apneg  8469  mulext1  8470  mulext  8472  aprcl  8504  mulap0  8511  receuap  8526  mul0eqap  8527  divrecap  8544  divcanap3  8554  muldivdirap  8563  divdivdivap  8569  divsubdivap  8584  apmul1  8644  apdivmuld  8669  qapne  9530  cnref1o  9541  mul2lt0rlt0  9648  lincmb01cmp  9889  iccf1o  9890  qbtwnrelemcalc  10137  flqpmodeq  10208  modq0  10210  modqdiffl  10216  modqvalp1  10224  modqcyc  10240  modqcyc2  10241  modqadd1  10242  mulqaddmodid  10245  modqmuladdnn0  10249  qnegmod  10250  modqmul1  10258  mulexpzap  10441  expmulzap  10447  binom2  10511  binom3  10517  bernneq  10520  nn0opthd  10578  bcval5  10619  remullem  10753  cjreim2  10786  cnrecnv  10792  absval  10883  resqrexlemover  10892  resqrexlemcalc1  10896  resqrexlemnm  10900  absimle  10966  abstri  10986  bdtrilem  11120  mulcn2  11191  reccn2ap  11192  climcvg1nlem  11228  isummulc2  11305  fsummulc2  11327  fsumparts  11349  binomlem  11362  binom1dif  11366  trireciplem  11379  mertenslemi1  11414  mertensabs  11416  ntrivcvgap  11427  fprodmul  11470  efaddlem  11553  sinval  11581  cosval  11582  sinadd  11615  cosadd  11616  tanaddaplem  11617  tanaddap  11618  addsin  11621  sincossq  11627  sin2t  11628  cos12dec  11646  eirraplem  11655  dvdscmulr  11697  dvdsmulcr  11698  dvds2ln  11701  oddm1even  11747  divalglemnn  11790  divalglemnqt  11792  flodddiv4  11806  gcdaddm  11848  bezoutlemnewy  11860  bezoutlema  11863  bezoutlemb  11864  lcmgcdlem  11934  oddpwdc  12028  phiprmpw  12074  eulerthlema  12082  oddennn  12093  mulc1cncf  12936  mulcncf  12951  dvmulxxbr  13026  dvimulf  13030  dvexp  13035  dvmptmulx  13042  dvmptcmulcn  13043  sin0pilem1  13062  rpcxpef  13175  rpcncxpcl  13183  cxpap0  13185  rpcxpadd  13186  rpmulcxp  13190  cxpmul  13193  abscxp  13195  rpabscxpbnd  13219  binom4  13256  qdencn  13561  cvgcmp2nlemabs  13566