Theorem mulcli 8331

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 8306	. 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 8177   x. 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  8912  2mulicn  9529  numma  9822  nummac  9823  9t11e99  9908  decbin2  9919  irec  11078  binom2i  11087  3dec  11154  rei  11667  imi  11668  3dvdsdec  12634  3dvds2dec  12635  odd2np1  12642  3lcm2e6woprm  12866  6lcm4e12  12867  modxai  13197  karatsuba  13211  ballotfilemth  13283  sinhalfpilem  15895  ef2pi  15909  ef2kpi  15910  efper  15911  sinperlem  15912  sin2kpi  15915  cos2kpi  15916  sin2pim  15917  cos2pim  15918  sincos4thpi  15944  sincos6thpi  15946  abssinper  15950  cosq34lt1  15954  log2ublem2  16090  log2ublem3  16091  log2ublog2  16092  bclbnd  16127  lgsdir2lem5  16163  2lgsoddprmlem3c  16240  2lgsoddprmlem3d  16241