Theorem mulcld 8128

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

Syntax hints:   → wi 4   ∈ wcel 2178  (class class class)co 5967  ℂcc 7958   · cmul 7965

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

This theorem is referenced by:  kcnktkm1cn  8490  rereim  8694  cru  8710  apreim  8711  mulreim  8712  apadd1  8716  apneg  8719  mulext1  8720  mulext  8722  aprcl  8754  aptap  8758  mulap0  8762  receuap  8777  mul0eqap  8778  divrecap  8796  divcanap3  8806  muldivdirap  8815  divdivdivap  8821  divsubdivap  8836  apmul1  8896  apdivmuld  8921  ofnegsub  9070  qapne  9795  cnref1o  9807  mul2lt0rlt0  9916  lincmb01cmp  10160  iccf1o  10161  qbtwnrelemcalc  10435  flqpmodeq  10509  modq0  10511  modqdiffl  10517  modqvalp1  10525  modqcyc  10541  modqcyc2  10542  modqadd1  10543  mulqaddmodid  10546  modqmuladdnn0  10550  qnegmod  10551  modqmul1  10559  mulexpzap  10761  expmulzap  10767  binom2  10833  binom3  10839  bernneq  10842  mulsubdivbinom2ap  10893  nn0opthd  10904  bcval5  10945  remullem  11297  cjreim2  11330  cnrecnv  11336  absval  11427  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemnm  11444  absimle  11510  abstri  11530  bdtrilem  11665  mulcn2  11738  reccn2ap  11739  climcvg1nlem  11775  isummulc2  11852  fsummulc2  11874  fsumparts  11896  binomlem  11909  binom1dif  11913  trireciplem  11926  mertenslemi1  11961  mertensabs  11963  ntrivcvgap  11974  fprodmul  12017  efaddlem  12100  sinval  12128  cosval  12129  sinadd  12162  cosadd  12163  tanaddaplem  12164  tanaddap  12165  addsin  12168  sincossq  12174  sin2t  12175  cos12dec  12194  eirraplem  12203  dvdscmulr  12246  dvdsmulcr  12247  dvds2ln  12250  oddm1even  12301  divalglemnn  12344  divalglemnqt  12346  flodddiv4  12362  gcdaddm  12420  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  lcmgcdlem  12514  oddpwdc  12611  phiprmpw  12659  eulerthlema  12667  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  pcpremul  12731  pcaddlem  12777  fldivp1  12786  mul4sqlem  12831  4sqlem14  12842  oddennn  12878  cnfldui  14466  expghmap  14484  znunit  14536  expcn  15156  mulc1cncf  15176  mulcncf  15195  dvmulxxbr  15289  dvimulf  15293  dvexp  15298  dvmptmulx  15307  dvmptcmulcn  15308  plyf  15324  ply1termlem  15329  plyaddlem1  15334  plymullem1  15335  plycoeid3  15344  plycolemc  15345  plycjlemc  15347  plyrecj  15350  dvply1  15352  dvply2g  15353  sin0pilem1  15368  rpcxpef  15481  rpcncxpcl  15489  cxpap0  15491  rpcxpadd  15492  rpmulcxp  15496  cxpmul  15499  rpcxpmul2  15500  abscxp  15502  rpabscxpbnd  15527  binom4  15566  mpodvdsmulf1o  15577  fsumdvdsmul  15578  perfectlem2  15587  lgsquad2lem1  15673  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2sqlem3  15709  qdencn  16168  cvgcmp2nlemabs  16173