Theorem mulcld 8190

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020   · cmul 8027

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

This theorem is referenced by:  kcnktkm1cn  8552  rereim  8756  cru  8772  apreim  8773  mulreim  8774  apadd1  8778  apneg  8781  mulext1  8782  mulext  8784  aprcl  8816  aptap  8820  mulap0  8824  receuap  8839  mul0eqap  8840  divrecap  8858  divcanap3  8868  muldivdirap  8877  divdivdivap  8883  divsubdivap  8898  apmul1  8958  apdivmuld  8983  ofnegsub  9132  qapne  9863  cnref1o  9875  mul2lt0rlt0  9984  lincmb01cmp  10228  iccf1o  10229  qbtwnrelemcalc  10505  flqpmodeq  10579  modq0  10581  modqdiffl  10587  modqvalp1  10595  modqcyc  10611  modqcyc2  10612  modqadd1  10613  mulqaddmodid  10616  modqmuladdnn0  10620  qnegmod  10621  modqmul1  10629  mulexpzap  10831  expmulzap  10837  binom2  10903  binom3  10909  bernneq  10912  mulsubdivbinom2ap  10963  nn0opthd  10974  bcval5  11015  remullem  11422  cjreim2  11455  cnrecnv  11461  absval  11552  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemnm  11569  absimle  11635  abstri  11655  bdtrilem  11790  mulcn2  11863  reccn2ap  11864  climcvg1nlem  11900  isummulc2  11977  fsummulc2  11999  fsumparts  12021  binomlem  12034  binom1dif  12038  trireciplem  12051  mertenslemi1  12086  mertensabs  12088  ntrivcvgap  12099  fprodmul  12142  efaddlem  12225  sinval  12253  cosval  12254  sinadd  12287  cosadd  12288  tanaddaplem  12289  tanaddap  12290  addsin  12293  sincossq  12299  sin2t  12300  cos12dec  12319  eirraplem  12328  dvdscmulr  12371  dvdsmulcr  12372  dvds2ln  12375  oddm1even  12426  divalglemnn  12469  divalglemnqt  12471  flodddiv4  12487  gcdaddm  12545  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  lcmgcdlem  12639  oddpwdc  12736  phiprmpw  12784  eulerthlema  12792  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pcpremul  12856  pcaddlem  12902  fldivp1  12911  mul4sqlem  12956  4sqlem14  12967  oddennn  13003  cnfldui  14593  expghmap  14611  znunit  14663  expcn  15283  mulc1cncf  15303  mulcncf  15322  dvmulxxbr  15416  dvimulf  15420  dvexp  15425  dvmptmulx  15434  dvmptcmulcn  15435  plyf  15451  ply1termlem  15456  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  plycolemc  15472  plycjlemc  15474  plyrecj  15477  dvply1  15479  dvply2g  15480  sin0pilem1  15495  rpcxpef  15608  rpcncxpcl  15616  cxpap0  15618  rpcxpadd  15619  rpmulcxp  15623  cxpmul  15626  rpcxpmul2  15627  abscxp  15629  rpabscxpbnd  15654  binom4  15693  mpodvdsmulf1o  15704  fsumdvdsmul  15705  perfectlem2  15714  lgsquad2lem1  15800  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2sqlem3  15836  qdencn  16567  cvgcmp2nlemabs  16572