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  9836  nummac  9837  9t11e99  9922  decbin2  9933  irec  11097  binom2i  11106  3dec  11174  rei  11687  imi  11688  3dvdsdec  12657  3dvds2dec  12658  odd2np1  12665  3lcm2e6woprm  12889  6lcm4e12  12890  modxai  13224  mod2xnegi  13227  karatsuba  13239  ballotfilemth  13339  sinhalfpilem  16051  ef2pi  16065  ef2kpi  16066  efper  16067  sinperlem  16068  sin2kpi  16071  cos2kpi  16072  sin2pim  16073  cos2pim  16074  sincos4thpi  16100  sincos6thpi  16102  abssinper  16106  cosq34lt1  16111  root1idef  16117  efnthr  16209  log2ublem2  16255  log2ublem3  16256  log2ublog2  16257  bclbnd  16340  bposlem8  16351  bposlem9  16352  lgsdir2lem5  16389  2lgsoddprmlem3c  16466  2lgsoddprmlem3d  16467