Theorem mulcli 8183

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

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029   · cmul 8036

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

This theorem is referenced by:  ixi  8762  2mulicn  9365  numma  9653  nummac  9654  9t11e99  9739  decbin2  9750  irec  10900  binom2i  10909  3dec  10975  rei  11459  imi  11460  3dvdsdec  12425  3dvds2dec  12426  odd2np1  12433  3lcm2e6woprm  12657  6lcm4e12  12658  modxai  12988  karatsuba  13002  sinhalfpilem  15514  ef2pi  15528  ef2kpi  15529  efper  15530  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  sin2pim  15536  cos2pim  15537  sincos4thpi  15563  sincos6thpi  15565  abssinper  15569  cosq34lt1  15573  lgsdir2lem5  15760  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838