Theorem mulcld 8092

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

Syntax hints:   → wi 4   ∈ wcel 2175  (class class class)co 5943  ℂcc 7922   · cmul 7929

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

This theorem is referenced by:  kcnktkm1cn  8454  rereim  8658  cru  8674  apreim  8675  mulreim  8676  apadd1  8680  apneg  8683  mulext1  8684  mulext  8686  aprcl  8718  aptap  8722  mulap0  8726  receuap  8741  mul0eqap  8742  divrecap  8760  divcanap3  8770  muldivdirap  8779  divdivdivap  8785  divsubdivap  8800  apmul1  8860  apdivmuld  8885  ofnegsub  9034  qapne  9759  cnref1o  9771  mul2lt0rlt0  9880  lincmb01cmp  10124  iccf1o  10125  qbtwnrelemcalc  10396  flqpmodeq  10470  modq0  10472  modqdiffl  10478  modqvalp1  10486  modqcyc  10502  modqcyc2  10503  modqadd1  10504  mulqaddmodid  10507  modqmuladdnn0  10511  qnegmod  10512  modqmul1  10520  mulexpzap  10722  expmulzap  10728  binom2  10794  binom3  10800  bernneq  10803  mulsubdivbinom2ap  10854  nn0opthd  10865  bcval5  10906  remullem  11124  cjreim2  11157  cnrecnv  11163  absval  11254  resqrexlemover  11263  resqrexlemcalc1  11267  resqrexlemnm  11271  absimle  11337  abstri  11357  bdtrilem  11492  mulcn2  11565  reccn2ap  11566  climcvg1nlem  11602  isummulc2  11679  fsummulc2  11701  fsumparts  11723  binomlem  11736  binom1dif  11740  trireciplem  11753  mertenslemi1  11788  mertensabs  11790  ntrivcvgap  11801  fprodmul  11844  efaddlem  11927  sinval  11955  cosval  11956  sinadd  11989  cosadd  11990  tanaddaplem  11991  tanaddap  11992  addsin  11995  sincossq  12001  sin2t  12002  cos12dec  12021  eirraplem  12030  dvdscmulr  12073  dvdsmulcr  12074  dvds2ln  12077  oddm1even  12128  divalglemnn  12171  divalglemnqt  12173  flodddiv4  12189  gcdaddm  12247  bezoutlemnewy  12259  bezoutlema  12262  bezoutlemb  12263  lcmgcdlem  12341  oddpwdc  12438  phiprmpw  12486  eulerthlema  12494  pythagtriplem12  12540  pythagtriplem14  12542  pythagtriplem16  12544  pcpremul  12558  pcaddlem  12604  fldivp1  12613  mul4sqlem  12658  4sqlem14  12669  oddennn  12705  cnfldui  14293  expghmap  14311  znunit  14363  expcn  14983  mulc1cncf  15003  mulcncf  15022  dvmulxxbr  15116  dvimulf  15120  dvexp  15125  dvmptmulx  15134  dvmptcmulcn  15135  plyf  15151  ply1termlem  15156  plyaddlem1  15161  plymullem1  15162  plycoeid3  15171  plycolemc  15172  plycjlemc  15174  plyrecj  15177  dvply1  15179  dvply2g  15180  sin0pilem1  15195  rpcxpef  15308  rpcncxpcl  15316  cxpap0  15318  rpcxpadd  15319  rpmulcxp  15323  cxpmul  15326  rpcxpmul2  15327  abscxp  15329  rpabscxpbnd  15354  binom4  15393  mpodvdsmulf1o  15404  fsumdvdsmul  15405  perfectlem2  15414  lgsquad2lem1  15500  2lgslem3b  15513  2lgslem3c  15514  2lgslem3d  15515  2sqlem3  15536  qdencn  15899  cvgcmp2nlemabs  15904