Theorem remulcli 8148

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 8115	. 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 5994   RRcr 7986   x. cmul 7992

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

This theorem is referenced by:  addltmul  9336  nn0lele2xi  9408  numltc  9591  ef01bndlem  12253  cos2bnd  12257  sin4lt0  12264  sincosq3sgn  15487  sincosq4sgn  15488  cosq23lt0  15492  coseq0q4123  15493  coseq00topi  15494  coseq0negpitopi  15495  sincos4thpi  15499  cosq34lt1  15509  cos02pilt1  15510  cos0pilt1  15511  taupi  16372