Theorem remulcli 8042

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 8009	. 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 5923   RRcr 7880   x. cmul 7886

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

This theorem is referenced by:  addltmul  9230  nn0lele2xi  9302  numltc  9484  ef01bndlem  11923  cos2bnd  11927  sin4lt0  11934  sincosq3sgn  15074  sincosq4sgn  15075  cosq23lt0  15079  coseq0q4123  15080  coseq00topi  15081  coseq0negpitopi  15082  sincos4thpi  15086  cosq34lt1  15096  cos02pilt1  15097  cos0pilt1  15098  taupi  15727