Theorem mulcli 8338

Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC

Assertion

Ref	Expression
mulcli	|- ( A x. B ) e. CC

Proof of Theorem mulcli

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		mulcl 8313	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
4	1, 2, 3	mp2an 430	1 |- ( A x. B ) e. CC

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6088   CCcc 8184   x. cmul 8191

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

This theorem is used by:  ixi  8920  2mulicn  9539  numma  9837  nummac  9838  9t11e99  9923  decbin2  9934  irec  11098  binom2i  11107  3dec  11175  rei  11688  imi  11689  3dvdsdec  12658  3dvds2dec  12659  odd2np1  12666  3lcm2e6woprm  12890  6lcm4e12  12891  modxai  13225  mod2xnegi  13228  karatsuba  13240  ballotfilemth  13340  sinhalfpilem  16030  ef2pi  16044  ef2kpi  16045  efper  16046  sinperlem  16047  sin2kpi  16050  cos2kpi  16051  sin2pim  16052  cos2pim  16053  sincos4thpi  16079  sincos6thpi  16081  abssinper  16085  cosq34lt1  16090  root1idef  16096  efnthr  16188  log2ublem2  16234  log2ublem3  16235  log2ublog2  16236  bclbnd  16319  bposlem8  16330  bposlem9  16331  lgsdir2lem5  16368  2lgsoddprmlem3c  16445  2lgsoddprmlem3d  16446