Theorem mulcld 8178

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6007  ℂcc 8008   · cmul 8015

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

This theorem is referenced by:  kcnktkm1cn  8540  rereim  8744  cru  8760  apreim  8761  mulreim  8762  apadd1  8766  apneg  8769  mulext1  8770  mulext  8772  aprcl  8804  aptap  8808  mulap0  8812  receuap  8827  mul0eqap  8828  divrecap  8846  divcanap3  8856  muldivdirap  8865  divdivdivap  8871  divsubdivap  8886  apmul1  8946  apdivmuld  8971  ofnegsub  9120  qapne  9846  cnref1o  9858  mul2lt0rlt0  9967  lincmb01cmp  10211  iccf1o  10212  qbtwnrelemcalc  10487  flqpmodeq  10561  modq0  10563  modqdiffl  10569  modqvalp1  10577  modqcyc  10593  modqcyc2  10594  modqadd1  10595  mulqaddmodid  10598  modqmuladdnn0  10602  qnegmod  10603  modqmul1  10611  mulexpzap  10813  expmulzap  10819  binom2  10885  binom3  10891  bernneq  10894  mulsubdivbinom2ap  10945  nn0opthd  10956  bcval5  10997  remullem  11397  cjreim2  11430  cnrecnv  11436  absval  11527  resqrexlemover  11536  resqrexlemcalc1  11540  resqrexlemnm  11544  absimle  11610  abstri  11630  bdtrilem  11765  mulcn2  11838  reccn2ap  11839  climcvg1nlem  11875  isummulc2  11952  fsummulc2  11974  fsumparts  11996  binomlem  12009  binom1dif  12013  trireciplem  12026  mertenslemi1  12061  mertensabs  12063  ntrivcvgap  12074  fprodmul  12117  efaddlem  12200  sinval  12228  cosval  12229  sinadd  12262  cosadd  12263  tanaddaplem  12264  tanaddap  12265  addsin  12268  sincossq  12274  sin2t  12275  cos12dec  12294  eirraplem  12303  dvdscmulr  12346  dvdsmulcr  12347  dvds2ln  12350  oddm1even  12401  divalglemnn  12444  divalglemnqt  12446  flodddiv4  12462  gcdaddm  12520  bezoutlemnewy  12532  bezoutlema  12535  bezoutlemb  12536  lcmgcdlem  12614  oddpwdc  12711  phiprmpw  12759  eulerthlema  12767  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pcpremul  12831  pcaddlem  12877  fldivp1  12886  mul4sqlem  12931  4sqlem14  12942  oddennn  12978  cnfldui  14568  expghmap  14586  znunit  14638  expcn  15258  mulc1cncf  15278  mulcncf  15297  dvmulxxbr  15391  dvimulf  15395  dvexp  15400  dvmptmulx  15409  dvmptcmulcn  15410  plyf  15426  ply1termlem  15431  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  plycolemc  15447  plycjlemc  15449  plyrecj  15452  dvply1  15454  dvply2g  15455  sin0pilem1  15470  rpcxpef  15583  rpcncxpcl  15591  cxpap0  15593  rpcxpadd  15594  rpmulcxp  15598  cxpmul  15601  rpcxpmul2  15602  abscxp  15604  rpabscxpbnd  15629  binom4  15668  mpodvdsmulf1o  15679  fsumdvdsmul  15680  perfectlem2  15689  lgsquad2lem1  15775  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2sqlem3  15811  qdencn  16455  cvgcmp2nlemabs  16460