Theorem mulcli 8174

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

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020   · cmul 8027

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

This theorem is referenced by:  ixi  8753  2mulicn  9356  numma  9644  nummac  9645  9t11e99  9730  decbin2  9741  irec  10891  binom2i  10900  3dec  10966  rei  11450  imi  11451  3dvdsdec  12416  3dvds2dec  12417  odd2np1  12424  3lcm2e6woprm  12648  6lcm4e12  12649  modxai  12979  karatsuba  12993  sinhalfpilem  15505  ef2pi  15519  ef2kpi  15520  efper  15521  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  sin2pim  15527  cos2pim  15528  sincos4thpi  15554  sincos6thpi  15556  abssinper  15560  cosq34lt1  15564  lgsdir2lem5  15751  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829