Theorem mulcli 8337

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 8312	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 430	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  ℂcc 8183   · cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcl 8283

This theorem is used by:  ixi  8919  2mulicn  9538  numma  9836  nummac  9837  9t11e99  9922  decbin2  9933  irec  11097  binom2i  11106  3dec  11174  rei  11687  imi  11688  3dvdsdec  12657  3dvds2dec  12658  odd2np1  12665  3lcm2e6woprm  12889  6lcm4e12  12890  modxai  13224  mod2xnegi  13227  karatsuba  13239  ballotfilemth  13339  sinhalfpilem  16018  ef2pi  16032  ef2kpi  16033  efper  16034  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  sin2pim  16040  cos2pim  16041  sincos4thpi  16067  sincos6thpi  16069  abssinper  16073  cosq34lt1  16078  root1idef  16084  efnthr  16176  log2ublem2  16222  log2ublem3  16223  log2ublog2  16224  bclbnd  16307  bposlem8  16318  bposlem9  16319  lgsdir2lem5  16356  2lgsoddprmlem3c  16433  2lgsoddprmlem3d  16434