Theorem remulcli 8168

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 8135	. 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 2200  (class class class)co 6007   RRcr 8006   x. cmul 8012

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

This theorem is referenced by:  addltmul  9356  nn0lele2xi  9428  numltc  9611  ef01bndlem  12275  cos2bnd  12279  sin4lt0  12286  sincosq3sgn  15510  sincosq4sgn  15511  cosq23lt0  15515  coseq0q4123  15516  coseq00topi  15517  coseq0negpitopi  15518  sincos4thpi  15522  cosq34lt1  15532  cos02pilt1  15533  cos0pilt1  15534  taupi  16471