Theorem mulcld 8242

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   · cmul 8080

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

This theorem is referenced by:  kcnktkm1cn  8604  rereim  8808  cru  8824  apreim  8825  mulreim  8826  apadd1  8830  apneg  8833  mulext1  8834  mulext  8836  aprcl  8868  aptap  8872  mulap0  8876  receuap  8891  mul0eqap  8892  divrecap  8910  divcanap3  8920  muldivdirap  8929  divdivdivap  8935  divsubdivap  8950  apmul1  9010  apdivmuld  9035  ofnegsub  9184  qapne  9917  cnref1o  9929  mul2lt0rlt0  10038  lincmb01cmp  10282  iccf1o  10284  qbtwnrelemcalc  10561  flqpmodeq  10635  modq0  10637  modqdiffl  10643  modqvalp1  10651  modqcyc  10667  modqcyc2  10668  modqadd1  10669  mulqaddmodid  10672  modqmuladdnn0  10676  qnegmod  10677  modqmul1  10685  mulexpzap  10887  expmulzap  10893  binom2  10959  binom3  10965  bernneq  10968  mulsubdivbinom2ap  11019  nn0opthd  11030  bcval5  11071  remullem  11494  cjreim2  11527  cnrecnv  11533  absval  11624  resqrexlemover  11633  resqrexlemcalc1  11637  resqrexlemnm  11641  absimle  11707  abstri  11727  bdtrilem  11862  mulcn2  11935  reccn2ap  11936  climcvg1nlem  11972  isummulc2  12050  fsummulc2  12072  fsumparts  12094  binomlem  12107  binom1dif  12111  trireciplem  12124  mertenslemi1  12159  mertensabs  12161  ntrivcvgap  12172  fprodmul  12215  efaddlem  12298  sinval  12326  cosval  12327  sinadd  12360  cosadd  12361  tanaddaplem  12362  tanaddap  12363  addsin  12366  sincossq  12372  sin2t  12373  cos12dec  12392  eirraplem  12401  dvdscmulr  12444  dvdsmulcr  12445  dvds2ln  12448  oddm1even  12499  divalglemnn  12542  divalglemnqt  12544  flodddiv4  12560  gcdaddm  12618  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  lcmgcdlem  12712  oddpwdc  12809  phiprmpw  12857  eulerthlema  12865  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  pcpremul  12929  pcaddlem  12975  fldivp1  12984  mul4sqlem  13029  4sqlem14  13040  oddennn  13076  cnfldui  14668  expghmap  14686  znunit  14738  expcn  15363  mulc1cncf  15383  mulcncf  15402  dvmulxxbr  15496  dvimulf  15500  dvexp  15505  dvmptmulx  15514  dvmptcmulcn  15515  plyf  15531  ply1termlem  15536  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  plycolemc  15552  plycjlemc  15554  plyrecj  15557  dvply1  15559  dvply2g  15560  sin0pilem1  15575  rpcxpef  15688  rpcncxpcl  15696  cxpap0  15698  rpcxpadd  15699  rpmulcxp  15703  cxpmul  15706  rpcxpmul2  15707  abscxp  15709  rpabscxpbnd  15734  binom4  15773  pellexlem1  15774  pellexlem2  15775  mpodvdsmulf1o  15787  fsumdvdsmul  15788  perfectlem2  15797  lgsquad2lem1  15883  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2sqlem3  15919  qdencn  16738  cvgcmp2nlemabs  16747  qdiff  16764