Theorem mulcld 7915

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

Syntax hints:   → wi 4   ∈ wcel 2136  (class class class)co 5841  ℂcc 7747   · cmul 7754

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

This theorem is referenced by:  kcnktkm1cn  8277  rereim  8480  cru  8496  apreim  8497  mulreim  8498  apadd1  8502  apneg  8505  mulext1  8506  mulext  8508  aprcl  8540  mulap0  8547  receuap  8562  mul0eqap  8563  divrecap  8580  divcanap3  8590  muldivdirap  8599  divdivdivap  8605  divsubdivap  8620  apmul1  8680  apdivmuld  8705  qapne  9573  cnref1o  9584  mul2lt0rlt0  9691  lincmb01cmp  9935  iccf1o  9936  qbtwnrelemcalc  10187  flqpmodeq  10258  modq0  10260  modqdiffl  10266  modqvalp1  10274  modqcyc  10290  modqcyc2  10291  modqadd1  10292  mulqaddmodid  10295  modqmuladdnn0  10299  qnegmod  10300  modqmul1  10308  mulexpzap  10491  expmulzap  10497  binom2  10562  binom3  10568  bernneq  10571  nn0opthd  10631  bcval5  10672  remullem  10809  cjreim2  10842  cnrecnv  10848  absval  10939  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemnm  10956  absimle  11022  abstri  11042  bdtrilem  11176  mulcn2  11249  reccn2ap  11250  climcvg1nlem  11286  isummulc2  11363  fsummulc2  11385  fsumparts  11407  binomlem  11420  binom1dif  11424  trireciplem  11437  mertenslemi1  11472  mertensabs  11474  ntrivcvgap  11485  fprodmul  11528  efaddlem  11611  sinval  11639  cosval  11640  sinadd  11673  cosadd  11674  tanaddaplem  11675  tanaddap  11676  addsin  11679  sincossq  11685  sin2t  11686  cos12dec  11704  eirraplem  11713  dvdscmulr  11756  dvdsmulcr  11757  dvds2ln  11760  oddm1even  11808  divalglemnn  11851  divalglemnqt  11853  flodddiv4  11867  gcdaddm  11913  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  lcmgcdlem  12005  oddpwdc  12102  phiprmpw  12150  eulerthlema  12158  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  pcpremul  12221  pcaddlem  12266  fldivp1  12274  mul4sqlem  12319  oddennn  12321  mulc1cncf  13176  mulcncf  13191  dvmulxxbr  13266  dvimulf  13270  dvexp  13275  dvmptmulx  13282  dvmptcmulcn  13283  sin0pilem1  13302  rpcxpef  13415  rpcncxpcl  13423  cxpap0  13425  rpcxpadd  13426  rpmulcxp  13430  cxpmul  13433  abscxp  13435  rpabscxpbnd  13459  binom4  13497  2sqlem3  13553  qdencn  13866  cvgcmp2nlemabs  13871