Theorem remulcli 8035

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 8002	. 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 2164  (class class class)co 5919   RRcr 7873   x. cmul 7879

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

This theorem is referenced by:  addltmul  9222  nn0lele2xi  9294  numltc  9476  ef01bndlem  11902  cos2bnd  11906  sin4lt0  11913  sincosq3sgn  15004  sincosq4sgn  15005  cosq23lt0  15009  coseq0q4123  15010  coseq00topi  15011  coseq0negpitopi  15012  sincos4thpi  15016  cosq34lt1  15026  cos02pilt1  15027  cos0pilt1  15028  taupi  15633