Theorem mulcld 8163

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6000  ℂcc 7993   · cmul 8000

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

This theorem is referenced by:  kcnktkm1cn  8525  rereim  8729  cru  8745  apreim  8746  mulreim  8747  apadd1  8751  apneg  8754  mulext1  8755  mulext  8757  aprcl  8789  aptap  8793  mulap0  8797  receuap  8812  mul0eqap  8813  divrecap  8831  divcanap3  8841  muldivdirap  8850  divdivdivap  8856  divsubdivap  8871  apmul1  8931  apdivmuld  8956  ofnegsub  9105  qapne  9830  cnref1o  9842  mul2lt0rlt0  9951  lincmb01cmp  10195  iccf1o  10196  qbtwnrelemcalc  10470  flqpmodeq  10544  modq0  10546  modqdiffl  10552  modqvalp1  10560  modqcyc  10576  modqcyc2  10577  modqadd1  10578  mulqaddmodid  10581  modqmuladdnn0  10585  qnegmod  10586  modqmul1  10594  mulexpzap  10796  expmulzap  10802  binom2  10868  binom3  10874  bernneq  10877  mulsubdivbinom2ap  10928  nn0opthd  10939  bcval5  10980  remullem  11377  cjreim2  11410  cnrecnv  11416  absval  11507  resqrexlemover  11516  resqrexlemcalc1  11520  resqrexlemnm  11524  absimle  11590  abstri  11610  bdtrilem  11745  mulcn2  11818  reccn2ap  11819  climcvg1nlem  11855  isummulc2  11932  fsummulc2  11954  fsumparts  11976  binomlem  11989  binom1dif  11993  trireciplem  12006  mertenslemi1  12041  mertensabs  12043  ntrivcvgap  12054  fprodmul  12097  efaddlem  12180  sinval  12208  cosval  12209  sinadd  12242  cosadd  12243  tanaddaplem  12244  tanaddap  12245  addsin  12248  sincossq  12254  sin2t  12255  cos12dec  12274  eirraplem  12283  dvdscmulr  12326  dvdsmulcr  12327  dvds2ln  12330  oddm1even  12381  divalglemnn  12424  divalglemnqt  12426  flodddiv4  12442  gcdaddm  12500  bezoutlemnewy  12512  bezoutlema  12515  bezoutlemb  12516  lcmgcdlem  12594  oddpwdc  12691  phiprmpw  12739  eulerthlema  12747  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pcpremul  12811  pcaddlem  12857  fldivp1  12866  mul4sqlem  12911  4sqlem14  12922  oddennn  12958  cnfldui  14547  expghmap  14565  znunit  14617  expcn  15237  mulc1cncf  15257  mulcncf  15276  dvmulxxbr  15370  dvimulf  15374  dvexp  15379  dvmptmulx  15388  dvmptcmulcn  15389  plyf  15405  ply1termlem  15410  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  plycolemc  15426  plycjlemc  15428  plyrecj  15431  dvply1  15433  dvply2g  15434  sin0pilem1  15449  rpcxpef  15562  rpcncxpcl  15570  cxpap0  15572  rpcxpadd  15573  rpmulcxp  15577  cxpmul  15580  rpcxpmul2  15581  abscxp  15583  rpabscxpbnd  15608  binom4  15647  mpodvdsmulf1o  15658  fsumdvdsmul  15659  perfectlem2  15668  lgsquad2lem1  15754  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2sqlem3  15790  qdencn  16354  cvgcmp2nlemabs  16359