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  8911  2mulicn  9527  numma  9820  nummac  9821  9t11e99  9906  decbin2  9917  irec  11076  binom2i  11085  3dec  11152  rei  11665  imi  11666  3dvdsdec  12632  3dvds2dec  12633  odd2np1  12640  3lcm2e6woprm  12864  6lcm4e12  12865  modxai  13195  karatsuba  13209  ballotfilemth  13281  sinhalfpilem  15892  ef2pi  15906  ef2kpi  15907  efper  15908  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  sin2pim  15914  cos2pim  15915  sincos4thpi  15941  sincos6thpi  15943  abssinper  15947  cosq34lt1  15951  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  lgsdir2lem5  16151  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229