Theorem mulcld 8336

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

Syntax hints:   → wi 4   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   · cmul 8174

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

This theorem is referenced by:  kcnktkm1cn  8700  rereim  8904  cru  8920  apreim  8921  mulreim  8922  apadd1  8926  apneg  8929  mulext1  8930  mulext  8932  aprcl  8964  aptap  8968  mulap0  8972  msq0  8987  receuap  8989  mul0eqap  8990  divrecap  9008  divcanap3  9018  muldivdirap  9027  divdivdivap  9033  divsubdivap  9048  apmul1  9108  apdivmuld  9133  ofnegsub  9282  qapne  10018  cnref1o  10030  mul2lt0rlt0  10139  lincmb01cmp  10384  iccf1o  10386  qbtwnrelemcalc  10668  flqpmodeq  10742  modq0  10744  modqdiffl  10750  modqvalp1  10758  modqcyc  10774  modqcyc2  10775  modqadd1  10776  mulqaddmodid  10779  modqmuladdnn0  10783  qnegmod  10784  modqmul1  10792  mulexpzap  10994  expmulzap  11000  binom2  11066  binom3  11072  resq01  11073  bernneq  11076  mulsubdivbinom2ap  11127  nn0opthd  11138  bcval5  11179  remullem  11614  sq01  11638  cjreim2  11648  cnrecnv  11654  absval  11745  resqrexlemover  11754  resqrexlemcalc1  11758  resqrexlemnm  11762  absimle  11828  abstri  11848  bdtrilem  11983  mulcn2  12056  reccn2ap  12057  climcvg1nlem  12093  isummulc2  12171  fsummulc2  12193  fsumparts  12215  binomlem  12228  binom1dif  12232  trireciplem  12245  mertenslemi1  12280  mertensabs  12282  ntrivcvgap  12293  fprodmul  12336  efaddlem  12419  sinval  12447  cosval  12448  sinadd  12481  cosadd  12482  tanaddaplem  12483  tanaddap  12484  addsin  12487  sincossq  12493  sin2t  12494  cos12dec  12513  eirraplem  12522  dvdscmulr  12565  dvdsmulcr  12566  dvds2ln  12569  oddm1even  12620  divalglemnn  12663  divalglemnqt  12665  flodddiv4  12681  gcdaddm  12739  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  lcmgcdlem  12833  oddpwdc  12930  phiprmpw  12978  eulerthlema  12986  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  pcpremul  13050  pcaddlem  13096  fldivp1  13105  mul4sqlem  13150  4sqlem14  13161  oddennn  13261  cnfldui  14896  expghmap  14914  znunit  14966  expcn  15593  mulc1cncf  15613  mulcncf  15632  dvmulxxbr  15726  dvimulf  15730  dvexp  15735  dvmptmulx  15744  dvmptcmulcn  15745  plyf  15761  ply1termlem  15766  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plycolemc  15782  plycjlemc  15784  plyrecj  15787  dvply1  15789  dvply2g  15790  sin0pilem1  15805  rpcxpef  15919  rpcncxpcl  15927  cxpap0  15929  rpcxpadd  15930  rpmulcxp  15934  cxpmul  15937  rpcxpmul2  15938  abscxp  15940  rpabscxpbnd  15965  binom4  16004  pellexlem1  16005  pellexlem2  16006  mpodvdsmulf1o  16018  fsumdvdsmul  16019  perfectlem2  16028  lgsquad2lem1  16114  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2sqlem3  16150  qdencn  16977  cvgcmp2nlemabs  16986  qdiff  17003