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  9835  nummac  9836  9t11e99  9921  decbin2  9932  irec  11096  binom2i  11105  3dec  11173  rei  11686  imi  11687  3dvdsdec  12656  3dvds2dec  12657  odd2np1  12664  3lcm2e6woprm  12888  6lcm4e12  12889  modxai  13223  mod2xnegi  13226  karatsuba  13238  ballotfilemth  13338  sinhalfpilem  16035  ef2pi  16049  ef2kpi  16050  efper  16051  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  sin2pim  16057  cos2pim  16058  sincos4thpi  16084  sincos6thpi  16086  abssinper  16090  cosq34lt1  16095  root1idef  16101  efnthr  16193  log2ublem2  16239  log2ublem3  16240  log2ublog2  16241  bclbnd  16324  bposlem8  16335  bposlem9  16336  lgsdir2lem5  16373  2lgsoddprmlem3c  16450  2lgsoddprmlem3d  16451