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  15992  ef2pi  16006  ef2kpi  16007  efper  16008  sinperlem  16009  sin2kpi  16012  cos2kpi  16013  sin2pim  16014  cos2pim  16015  sincos4thpi  16041  sincos6thpi  16043  abssinper  16047  cosq34lt1  16052  root1idef  16058  efnthr  16150  log2ublem2  16196  log2ublem3  16197  log2ublog2  16198  bclbnd  16281  bposlem8  16292  bposlem9  16293  lgsdir2lem5  16330  2lgsoddprmlem3c  16407  2lgsoddprmlem3d  16408