Theorem mulcli 8331

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   · cmul 8184

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

This theorem is used by:  ixi  8913  2mulicn  9531  numma  9829  nummac  9830  9t11e99  9915  decbin2  9926  irec  11089  binom2i  11098  3dec  11166  rei  11679  imi  11680  3dvdsdec  12648  3dvds2dec  12649  odd2np1  12656  3lcm2e6woprm  12880  6lcm4e12  12881  modxai  13215  mod2xnegi  13218  karatsuba  13230  ballotfilemth  13330  sinhalfpilem  15942  ef2pi  15956  ef2kpi  15957  efper  15958  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  sin2pim  15964  cos2pim  15965  sincos4thpi  15991  sincos6thpi  15993  abssinper  15997  cosq34lt1  16001  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  bclbnd  16205  lgsdir2lem5  16249  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327