Theorem mulcli 8147

Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
mulcli	⊢ (𝐴 · 𝐵) ∈ ℂ

Proof of Theorem mulcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcl 8122	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 426	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ 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:  ixi  8726  2mulicn  9329  numma  9617  nummac  9618  9t11e99  9703  decbin2  9714  irec  10856  binom2i  10865  3dec  10931  rei  11405  imi  11406  3dvdsdec  12371  3dvds2dec  12372  odd2np1  12379  3lcm2e6woprm  12603  6lcm4e12  12604  modxai  12934  karatsuba  12948  sinhalfpilem  15459  ef2pi  15473  ef2kpi  15474  efper  15475  sinperlem  15476  sin2kpi  15479  cos2kpi  15480  sin2pim  15481  cos2pim  15482  sincos4thpi  15508  sincos6thpi  15510  abssinper  15514  cosq34lt1  15518  lgsdir2lem5  15705  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783