Theorem remulcli 8059

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	|- A e. RR
axri.2	|- B e. RR

Assertion

Ref	Expression
remulcli	|- ( A x. B ) e. RR

Proof of Theorem remulcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 |- A e. RR
2		axri.2	. 2 |- B e. RR
3		remulcl 8026	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	mp2an 426	1 |- ( A x. B ) e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5925   RRcr 7897   x. cmul 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 7997

This theorem is referenced by:  addltmul  9247  nn0lele2xi  9319  numltc  9501  ef01bndlem  11940  cos2bnd  11944  sin4lt0  11951  sincosq3sgn  15150  sincosq4sgn  15151  cosq23lt0  15155  coseq0q4123  15156  coseq00topi  15157  coseq0negpitopi  15158  sincos4thpi  15162  cosq34lt1  15172  cos02pilt1  15173  cos0pilt1  15174  taupi  15808