Theorem mulcld 8093

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

Syntax hints:   → wi 4   ∈ wcel 2176  (class class class)co 5944  ℂcc 7923   · cmul 7930

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

This theorem is referenced by:  kcnktkm1cn  8455  rereim  8659  cru  8675  apreim  8676  mulreim  8677  apadd1  8681  apneg  8684  mulext1  8685  mulext  8687  aprcl  8719  aptap  8723  mulap0  8727  receuap  8742  mul0eqap  8743  divrecap  8761  divcanap3  8771  muldivdirap  8780  divdivdivap  8786  divsubdivap  8801  apmul1  8861  apdivmuld  8886  ofnegsub  9035  qapne  9760  cnref1o  9772  mul2lt0rlt0  9881  lincmb01cmp  10125  iccf1o  10126  qbtwnrelemcalc  10398  flqpmodeq  10472  modq0  10474  modqdiffl  10480  modqvalp1  10488  modqcyc  10504  modqcyc2  10505  modqadd1  10506  mulqaddmodid  10509  modqmuladdnn0  10513  qnegmod  10514  modqmul1  10522  mulexpzap  10724  expmulzap  10730  binom2  10796  binom3  10802  bernneq  10805  mulsubdivbinom2ap  10856  nn0opthd  10867  bcval5  10908  remullem  11182  cjreim2  11215  cnrecnv  11221  absval  11312  resqrexlemover  11321  resqrexlemcalc1  11325  resqrexlemnm  11329  absimle  11395  abstri  11415  bdtrilem  11550  mulcn2  11623  reccn2ap  11624  climcvg1nlem  11660  isummulc2  11737  fsummulc2  11759  fsumparts  11781  binomlem  11794  binom1dif  11798  trireciplem  11811  mertenslemi1  11846  mertensabs  11848  ntrivcvgap  11859  fprodmul  11902  efaddlem  11985  sinval  12013  cosval  12014  sinadd  12047  cosadd  12048  tanaddaplem  12049  tanaddap  12050  addsin  12053  sincossq  12059  sin2t  12060  cos12dec  12079  eirraplem  12088  dvdscmulr  12131  dvdsmulcr  12132  dvds2ln  12135  oddm1even  12186  divalglemnn  12229  divalglemnqt  12231  flodddiv4  12247  gcdaddm  12305  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  lcmgcdlem  12399  oddpwdc  12496  phiprmpw  12544  eulerthlema  12552  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem16  12602  pcpremul  12616  pcaddlem  12662  fldivp1  12671  mul4sqlem  12716  4sqlem14  12727  oddennn  12763  cnfldui  14351  expghmap  14369  znunit  14421  expcn  15041  mulc1cncf  15061  mulcncf  15080  dvmulxxbr  15174  dvimulf  15178  dvexp  15183  dvmptmulx  15192  dvmptcmulcn  15193  plyf  15209  ply1termlem  15214  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  plycolemc  15230  plycjlemc  15232  plyrecj  15235  dvply1  15237  dvply2g  15238  sin0pilem1  15253  rpcxpef  15366  rpcncxpcl  15374  cxpap0  15376  rpcxpadd  15377  rpmulcxp  15381  cxpmul  15384  rpcxpmul2  15385  abscxp  15387  rpabscxpbnd  15412  binom4  15451  mpodvdsmulf1o  15462  fsumdvdsmul  15463  perfectlem2  15472  lgsquad2lem1  15558  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2sqlem3  15594  qdencn  15966  cvgcmp2nlemabs  15971