Theorem mulcld 8123

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

Syntax hints:   → wi 4   ∈ wcel 2177  (class class class)co 5962  ℂcc 7953   · cmul 7960

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

This theorem is referenced by:  kcnktkm1cn  8485  rereim  8689  cru  8705  apreim  8706  mulreim  8707  apadd1  8711  apneg  8714  mulext1  8715  mulext  8717  aprcl  8749  aptap  8753  mulap0  8757  receuap  8772  mul0eqap  8773  divrecap  8791  divcanap3  8801  muldivdirap  8810  divdivdivap  8816  divsubdivap  8831  apmul1  8891  apdivmuld  8916  ofnegsub  9065  qapne  9790  cnref1o  9802  mul2lt0rlt0  9911  lincmb01cmp  10155  iccf1o  10156  qbtwnrelemcalc  10430  flqpmodeq  10504  modq0  10506  modqdiffl  10512  modqvalp1  10520  modqcyc  10536  modqcyc2  10537  modqadd1  10538  mulqaddmodid  10541  modqmuladdnn0  10545  qnegmod  10546  modqmul1  10554  mulexpzap  10756  expmulzap  10762  binom2  10828  binom3  10834  bernneq  10837  mulsubdivbinom2ap  10888  nn0opthd  10899  bcval5  10940  remullem  11267  cjreim2  11300  cnrecnv  11306  absval  11397  resqrexlemover  11406  resqrexlemcalc1  11410  resqrexlemnm  11414  absimle  11480  abstri  11500  bdtrilem  11635  mulcn2  11708  reccn2ap  11709  climcvg1nlem  11745  isummulc2  11822  fsummulc2  11844  fsumparts  11866  binomlem  11879  binom1dif  11883  trireciplem  11896  mertenslemi1  11931  mertensabs  11933  ntrivcvgap  11944  fprodmul  11987  efaddlem  12070  sinval  12098  cosval  12099  sinadd  12132  cosadd  12133  tanaddaplem  12134  tanaddap  12135  addsin  12138  sincossq  12144  sin2t  12145  cos12dec  12164  eirraplem  12173  dvdscmulr  12216  dvdsmulcr  12217  dvds2ln  12220  oddm1even  12271  divalglemnn  12314  divalglemnqt  12316  flodddiv4  12332  gcdaddm  12390  bezoutlemnewy  12402  bezoutlema  12405  bezoutlemb  12406  lcmgcdlem  12484  oddpwdc  12581  phiprmpw  12629  eulerthlema  12637  pythagtriplem12  12683  pythagtriplem14  12685  pythagtriplem16  12687  pcpremul  12701  pcaddlem  12747  fldivp1  12756  mul4sqlem  12801  4sqlem14  12812  oddennn  12848  cnfldui  14436  expghmap  14454  znunit  14506  expcn  15126  mulc1cncf  15146  mulcncf  15165  dvmulxxbr  15259  dvimulf  15263  dvexp  15268  dvmptmulx  15277  dvmptcmulcn  15278  plyf  15294  ply1termlem  15299  plyaddlem1  15304  plymullem1  15305  plycoeid3  15314  plycolemc  15315  plycjlemc  15317  plyrecj  15320  dvply1  15322  dvply2g  15323  sin0pilem1  15338  rpcxpef  15451  rpcncxpcl  15459  cxpap0  15461  rpcxpadd  15462  rpmulcxp  15466  cxpmul  15469  rpcxpmul2  15470  abscxp  15472  rpabscxpbnd  15497  binom4  15536  mpodvdsmulf1o  15547  fsumdvdsmul  15548  perfectlem2  15557  lgsquad2lem1  15643  2lgslem3b  15656  2lgslem3c  15657  2lgslem3d  15658  2sqlem3  15679  qdencn  16138  cvgcmp2nlemabs  16143