Theorem mulcli 8332

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 8307	. 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 6085   CCcc 8178   x. cmul 8185

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

This theorem is used by:  ixi  8914  2mulicn  9532  numma  9830  nummac  9831  9t11e99  9916  decbin2  9927  irec  11091  binom2i  11100  3dec  11168  rei  11681  imi  11682  3dvdsdec  12651  3dvds2dec  12652  odd2np1  12659  3lcm2e6woprm  12883  6lcm4e12  12884  modxai  13218  mod2xnegi  13221  karatsuba  13233  ballotfilemth  13333  sinhalfpilem  15984  ef2pi  15998  ef2kpi  15999  efper  16000  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  sin2pim  16006  cos2pim  16007  sincos4thpi  16033  sincos6thpi  16035  abssinper  16039  cosq34lt1  16044  root1idef  16050  efnthr  16142  log2ublem2  16188  log2ublem3  16189  log2ublog2  16190  bclbnd  16273  bposlem8  16284  bposlem9  16285  lgsdir2lem5  16322  2lgsoddprmlem3c  16399  2lgsoddprmlem3d  16400