Theorem remulcli 8334

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 8301	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4	1, 2, 3	mp2an 430	1 |- ( A x. B ) e. RR

Syntax hints:   e. wcel 2209  (class class class)co 6079   RRcr 8172   x. cmul 8178

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

This theorem is referenced by:  addltmul  9525  nn0lele2xi  9597  numltc  9785  ef01bndlem  12506  cos2bnd  12510  sin4lt0  12517  sincosq3sgn  15912  sincosq4sgn  15913  cosq23lt0  15917  coseq0q4123  15918  coseq00topi  15919  coseq0negpitopi  15920  sincos4thpi  15924  cosq34lt1  15934  cos02pilt1  15935  cos0pilt1  15936  log2ublem1  16066  log2ublem2  16067  taupi  17097