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  11090  binom2i  11099  3dec  11167  rei  11680  imi  11681  3dvdsdec  12650  3dvds2dec  12651  odd2np1  12658  3lcm2e6woprm  12882  6lcm4e12  12883  modxai  13217  mod2xnegi  13220  karatsuba  13232  ballotfilemth  13332  sinhalfpilem  15945  ef2pi  15959  ef2kpi  15960  efper  15961  sinperlem  15962  sin2kpi  15965  cos2kpi  15966  sin2pim  15967  cos2pim  15968  sincos4thpi  15994  sincos6thpi  15996  abssinper  16000  cosq34lt1  16004  log2ublem2  16144  log2ublem3  16145  log2ublog2  16146  bclbnd  16229  lgsdir2lem5  16273  2lgsoddprmlem3c  16350  2lgsoddprmlem3d  16351