Theorem mulcld 7139

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

Syntax hints:   → wi 4   ∈ wcel 1433  (class class class)co 5532  ℂcc 6979   · cmul 6986

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

This theorem is referenced by:  kcnktkm1cn  7487  rereim  7686  cru  7702  apreim  7703  mulreim  7704  apadd1  7708  apneg  7711  mulext1  7712  mulext  7714  mulap0  7744  receuap  7759  divrecap  7776  divcanap3  7786  muldivdirap  7795  divdivdivap  7801  divsubdivap  7816  apmul1  7876  qapne  8724  cnref1o  8733  lincmb01cmp  9025  iccf1o  9026  qbtwnrelemcalc  9264  flqpmodeq  9329  modq0  9331  modqdiffl  9337  modqvalp1  9345  modqcyc  9361  modqcyc2  9362  modqadd1  9363  mulqaddmodid  9366  modqmuladdnn0  9370  qnegmod  9371  modqmul1  9379  mulexpzap  9516  expmulzap  9522  binom2  9585  binom3  9590  bernneq  9593  nn0opthd  9649  ibcval5  9690  remullem  9758  cjreim2  9791  cnrecnv  9797  absval  9887  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemnm  9904  absimle  9970  abstri  9990  mulcn2  10151  iisermulc2  10178  climcvg1nlem  10186  dvdscmulr  10224  dvdsmulcr  10225  dvds2ln  10228  oddm1even  10274  divalglemnn  10318  divalglemnqt  10320  flodddiv4  10334  gcdaddm  10375  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  lcmgcdlem  10459  oddpwdc  10552  qdencn  10785