Theorem mulcld 8199

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029   · cmul 8036

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

This theorem is referenced by:  kcnktkm1cn  8561  rereim  8765  cru  8781  apreim  8782  mulreim  8783  apadd1  8787  apneg  8790  mulext1  8791  mulext  8793  aprcl  8825  aptap  8829  mulap0  8833  receuap  8848  mul0eqap  8849  divrecap  8867  divcanap3  8877  muldivdirap  8886  divdivdivap  8892  divsubdivap  8907  apmul1  8967  apdivmuld  8992  ofnegsub  9141  qapne  9872  cnref1o  9884  mul2lt0rlt0  9993  lincmb01cmp  10237  iccf1o  10238  qbtwnrelemcalc  10514  flqpmodeq  10588  modq0  10590  modqdiffl  10596  modqvalp1  10604  modqcyc  10620  modqcyc2  10621  modqadd1  10622  mulqaddmodid  10625  modqmuladdnn0  10629  qnegmod  10630  modqmul1  10638  mulexpzap  10840  expmulzap  10846  binom2  10912  binom3  10918  bernneq  10921  mulsubdivbinom2ap  10972  nn0opthd  10983  bcval5  11024  remullem  11431  cjreim2  11464  cnrecnv  11470  absval  11561  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemnm  11578  absimle  11644  abstri  11664  bdtrilem  11799  mulcn2  11872  reccn2ap  11873  climcvg1nlem  11909  isummulc2  11986  fsummulc2  12008  fsumparts  12030  binomlem  12043  binom1dif  12047  trireciplem  12060  mertenslemi1  12095  mertensabs  12097  ntrivcvgap  12108  fprodmul  12151  efaddlem  12234  sinval  12262  cosval  12263  sinadd  12296  cosadd  12297  tanaddaplem  12298  tanaddap  12299  addsin  12302  sincossq  12308  sin2t  12309  cos12dec  12328  eirraplem  12337  dvdscmulr  12380  dvdsmulcr  12381  dvds2ln  12384  oddm1even  12435  divalglemnn  12478  divalglemnqt  12480  flodddiv4  12496  gcdaddm  12554  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  lcmgcdlem  12648  oddpwdc  12745  phiprmpw  12793  eulerthlema  12801  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pcpremul  12865  pcaddlem  12911  fldivp1  12920  mul4sqlem  12965  4sqlem14  12976  oddennn  13012  cnfldui  14602  expghmap  14620  znunit  14672  expcn  15292  mulc1cncf  15312  mulcncf  15331  dvmulxxbr  15425  dvimulf  15429  dvexp  15434  dvmptmulx  15443  dvmptcmulcn  15444  plyf  15460  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycolemc  15481  plycjlemc  15483  plyrecj  15486  dvply1  15488  dvply2g  15489  sin0pilem1  15504  rpcxpef  15617  rpcncxpcl  15625  cxpap0  15627  rpcxpadd  15628  rpmulcxp  15632  cxpmul  15635  rpcxpmul2  15636  abscxp  15638  rpabscxpbnd  15663  binom4  15702  mpodvdsmulf1o  15713  fsumdvdsmul  15714  perfectlem2  15723  lgsquad2lem1  15809  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2sqlem3  15845  qdencn  16631  cvgcmp2nlemabs  16636