Theorem remulcli 8099

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 8066	. 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 2177  (class class class)co 5954   RRcr 7937   x. cmul 7943

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

This theorem is referenced by:  addltmul  9287  nn0lele2xi  9359  numltc  9542  ef01bndlem  12117  cos2bnd  12121  sin4lt0  12128  sincosq3sgn  15350  sincosq4sgn  15351  cosq23lt0  15355  coseq0q4123  15356  coseq00topi  15357  coseq0negpitopi  15358  sincos4thpi  15362  cosq34lt1  15372  cos02pilt1  15373  cos0pilt1  15374  taupi  16127